1(* Title: HOL/Auth/Kerberos_BAN_Gets.thy 2 Author: Giampaolo Bella, Catania University 3*) 4 5section\<open>The Kerberos Protocol, BAN Version, with Gets event\<close> 6 7theory Kerberos_BAN_Gets imports Public begin 8 9text\<open>From page 251 of 10 Burrows, Abadi and Needham (1989). A Logic of Authentication. 11 Proc. Royal Soc. 426 12 13 Confidentiality (secrecy) and authentication properties rely on 14 temporal checks: strong guarantees in a little abstracted - but 15 very realistic - model. 16\<close> 17 18(* Temporal modelization: session keys can be leaked 19 ONLY when they have expired *) 20 21consts 22 23 (*Duration of the session key*) 24 sesKlife :: nat 25 26 (*Duration of the authenticator*) 27 authlife :: nat 28 29text\<open>The ticket should remain fresh for two journeys on the network at least\<close> 30text\<open>The Gets event causes longer traces for the protocol to reach its end\<close> 31specification (sesKlife) 32 sesKlife_LB [iff]: "4 \<le> sesKlife" 33 by blast 34 35text\<open>The authenticator only for one journey\<close> 36text\<open>The Gets event causes longer traces for the protocol to reach its end\<close> 37specification (authlife) 38 authlife_LB [iff]: "2 \<le> authlife" 39 by blast 40 41 42abbreviation 43 CT :: "event list \<Rightarrow> nat" where 44 "CT == length" 45 46abbreviation 47 expiredK :: "[nat, event list] \<Rightarrow> bool" where 48 "expiredK T evs == sesKlife + T < CT evs" 49 50abbreviation 51 expiredA :: "[nat, event list] \<Rightarrow> bool" where 52 "expiredA T evs == authlife + T < CT evs" 53 54 55definition 56 (* Yields the subtrace of a given trace from its beginning to a given event *) 57 before :: "[event, event list] \<Rightarrow> event list" ("before _ on _") 58 where "before ev on evs = takeWhile (\<lambda>z. z \<noteq> ev) (rev evs)" 59 60definition 61 (* States than an event really appears only once on a trace *) 62 Unique :: "[event, event list] \<Rightarrow> bool" ("Unique _ on _") 63 where "Unique ev on evs = (ev \<notin> set (tl (dropWhile (\<lambda>z. z \<noteq> ev) evs)))" 64 65 66inductive_set bankerb_gets :: "event list set" 67 where 68 69 Nil: "[] \<in> bankerb_gets" 70 71 | Fake: "\<lbrakk> evsf \<in> bankerb_gets; X \<in> synth (analz (knows Spy evsf)) \<rbrakk> 72 \<Longrightarrow> Says Spy B X # evsf \<in> bankerb_gets" 73 74 | Reception: "\<lbrakk> evsr\<in> bankerb_gets; Says A B X \<in> set evsr \<rbrakk> 75 \<Longrightarrow> Gets B X # evsr \<in> bankerb_gets" 76 77 | BK1: "\<lbrakk> evs1 \<in> bankerb_gets \<rbrakk> 78 \<Longrightarrow> Says A Server \<lbrace>Agent A, Agent B\<rbrace> # evs1 79 \<in> bankerb_gets" 80 81 82 | BK2: "\<lbrakk> evs2 \<in> bankerb_gets; Key K \<notin> used evs2; K \<in> symKeys; 83 Gets Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs2 \<rbrakk> 84 \<Longrightarrow> Says Server A 85 (Crypt (shrK A) 86 \<lbrace>Number (CT evs2), Agent B, Key K, 87 (Crypt (shrK B) \<lbrace>Number (CT evs2), Agent A, Key K\<rbrace>)\<rbrace>) 88 # evs2 \<in> bankerb_gets" 89 90 91 | BK3: "\<lbrakk> evs3 \<in> bankerb_gets; 92 Gets A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) 93 \<in> set evs3; 94 Says A Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs3; 95 \<not> expiredK Tk evs3 \<rbrakk> 96 \<Longrightarrow> Says A B \<lbrace>Ticket, Crypt K \<lbrace>Agent A, Number (CT evs3)\<rbrace> \<rbrace> 97 # evs3 \<in> bankerb_gets" 98 99 100 | BK4: "\<lbrakk> evs4 \<in> bankerb_gets; 101 Gets B \<lbrace>(Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>), 102 (Crypt K \<lbrace>Agent A, Number Ta\<rbrace>) \<rbrace> \<in> set evs4; 103 \<not> expiredK Tk evs4; \<not> expiredA Ta evs4 \<rbrakk> 104 \<Longrightarrow> Says B A (Crypt K (Number Ta)) # evs4 105 \<in> bankerb_gets" 106 107 (*Old session keys may become compromised*) 108 | Oops: "\<lbrakk> evso \<in> bankerb_gets; 109 Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) 110 \<in> set evso; 111 expiredK Tk evso \<rbrakk> 112 \<Longrightarrow> Notes Spy \<lbrace>Number Tk, Key K\<rbrace> # evso \<in> bankerb_gets" 113 114 115declare Says_imp_knows_Spy [THEN parts.Inj, dest] 116declare parts.Body [dest] 117declare analz_into_parts [dest] 118declare Fake_parts_insert_in_Un [dest] 119declare knows_Spy_partsEs [elim] 120 121 122text\<open>A "possibility property": there are traces that reach the end.\<close> 123lemma "\<lbrakk>Key K \<notin> used []; K \<in> symKeys\<rbrakk> 124 \<Longrightarrow> \<exists>Timestamp. \<exists>evs \<in> bankerb_gets. 125 Says B A (Crypt K (Number Timestamp)) 126 \<in> set evs" 127apply (cut_tac sesKlife_LB) 128apply (cut_tac authlife_LB) 129apply (intro exI bexI) 130apply (rule_tac [2] 131 bankerb_gets.Nil [THEN bankerb_gets.BK1, THEN bankerb_gets.Reception, 132 THEN bankerb_gets.BK2, THEN bankerb_gets.Reception, 133 THEN bankerb_gets.BK3, THEN bankerb_gets.Reception, 134 THEN bankerb_gets.BK4]) 135apply (possibility, simp_all (no_asm_simp) add: used_Cons) 136done 137 138 139text\<open>Lemmas about reception invariant: if a message is received it certainly 140was sent\<close> 141lemma Gets_imp_Says : 142 "\<lbrakk> Gets B X \<in> set evs; evs \<in> bankerb_gets \<rbrakk> \<Longrightarrow> \<exists>A. Says A B X \<in> set evs" 143apply (erule rev_mp) 144apply (erule bankerb_gets.induct) 145apply auto 146done 147 148lemma Gets_imp_knows_Spy: 149 "\<lbrakk> Gets B X \<in> set evs; evs \<in> bankerb_gets \<rbrakk> \<Longrightarrow> X \<in> knows Spy evs" 150apply (blast dest!: Gets_imp_Says Says_imp_knows_Spy) 151done 152 153lemma Gets_imp_knows_Spy_parts[dest]: 154 "\<lbrakk> Gets B X \<in> set evs; evs \<in> bankerb_gets \<rbrakk> \<Longrightarrow> X \<in> parts (knows Spy evs)" 155apply (blast dest: Gets_imp_knows_Spy [THEN parts.Inj]) 156done 157 158lemma Gets_imp_knows: 159 "\<lbrakk> Gets B X \<in> set evs; evs \<in> bankerb_gets \<rbrakk> \<Longrightarrow> X \<in> knows B evs" 160by (metis Gets_imp_knows_Spy Gets_imp_knows_agents) 161 162lemma Gets_imp_knows_analz: 163 "\<lbrakk> Gets B X \<in> set evs; evs \<in> bankerb_gets \<rbrakk> \<Longrightarrow> X \<in> analz (knows B evs)" 164apply (blast dest: Gets_imp_knows [THEN analz.Inj]) 165done 166 167text\<open>Lemmas for reasoning about predicate "before"\<close> 168lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)" 169apply (induct_tac "evs") 170apply simp 171apply (rename_tac a b) 172apply (induct_tac "a") 173apply auto 174done 175 176lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)" 177apply (induct_tac "evs") 178apply simp 179apply (rename_tac a b) 180apply (induct_tac "a") 181apply auto 182done 183 184lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs" 185apply (induct_tac "evs") 186apply simp 187apply (rename_tac a b) 188apply (induct_tac "a") 189apply auto 190done 191 192lemma used_evs_rev: "used evs = used (rev evs)" 193apply (induct_tac "evs") 194apply simp 195apply (rename_tac a b) 196apply (induct_tac "a") 197apply (simp add: used_Says_rev) 198apply (simp add: used_Gets_rev) 199apply (simp add: used_Notes_rev) 200done 201 202lemma used_takeWhile_used [rule_format]: 203 "x \<in> used (takeWhile P X) \<longrightarrow> x \<in> used X" 204apply (induct_tac "X") 205apply simp 206apply (rename_tac a b) 207apply (induct_tac "a") 208apply (simp_all add: used_Nil) 209apply (blast dest!: initState_into_used)+ 210done 211 212lemma set_evs_rev: "set evs = set (rev evs)" 213apply auto 214done 215 216lemma takeWhile_void [rule_format]: 217 "x \<notin> set evs \<longrightarrow> takeWhile (\<lambda>z. z \<noteq> x) evs = evs" 218apply auto 219done 220 221(**** Inductive proofs about bankerb_gets ****) 222 223text\<open>Forwarding Lemma for reasoning about the encrypted portion of message BK3\<close> 224lemma BK3_msg_in_parts_knows_Spy: 225 "\<lbrakk>Gets A (Crypt KA \<lbrace>Timestamp, B, K, X\<rbrace>) \<in> set evs; evs \<in> bankerb_gets \<rbrakk> 226 \<Longrightarrow> X \<in> parts (knows Spy evs)" 227apply blast 228done 229 230lemma Oops_parts_knows_Spy: 231 "Says Server A (Crypt (shrK A) \<lbrace>Timestamp, B, K, X\<rbrace>) \<in> set evs 232 \<Longrightarrow> K \<in> parts (knows Spy evs)" 233apply blast 234done 235 236 237text\<open>Spy never sees another agent's shared key! (unless it's bad at start)\<close> 238lemma Spy_see_shrK [simp]: 239 "evs \<in> bankerb_gets \<Longrightarrow> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" 240apply (erule bankerb_gets.induct) 241apply (frule_tac [8] Oops_parts_knows_Spy) 242apply (frule_tac [6] BK3_msg_in_parts_knows_Spy, simp_all, blast+) 243done 244 245 246lemma Spy_analz_shrK [simp]: 247 "evs \<in> bankerb_gets \<Longrightarrow> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)" 248by auto 249 250lemma Spy_see_shrK_D [dest!]: 251 "\<lbrakk> Key (shrK A) \<in> parts (knows Spy evs); 252 evs \<in> bankerb_gets \<rbrakk> \<Longrightarrow> A\<in>bad" 253by (blast dest: Spy_see_shrK) 254 255lemmas Spy_analz_shrK_D = analz_subset_parts [THEN subsetD, THEN Spy_see_shrK_D, dest!] 256 257 258text\<open>Nobody can have used non-existent keys!\<close> 259lemma new_keys_not_used [simp]: 260 "\<lbrakk>Key K \<notin> used evs; K \<in> symKeys; evs \<in> bankerb_gets\<rbrakk> 261 \<Longrightarrow> K \<notin> keysFor (parts (knows Spy evs))" 262apply (erule rev_mp) 263apply (erule bankerb_gets.induct) 264apply (frule_tac [8] Oops_parts_knows_Spy) 265apply (frule_tac [6] BK3_msg_in_parts_knows_Spy, simp_all) 266txt\<open>Fake\<close> 267apply (force dest!: keysFor_parts_insert) 268txt\<open>BK2, BK3, BK4\<close> 269apply (force dest!: analz_shrK_Decrypt)+ 270done 271 272subsection\<open>Lemmas concerning the form of items passed in messages\<close> 273 274text\<open>Describes the form of K, X and K' when the Server sends this message.\<close> 275lemma Says_Server_message_form: 276 "\<lbrakk> Says Server A (Crypt K' \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) 277 \<in> set evs; evs \<in> bankerb_gets \<rbrakk> 278 \<Longrightarrow> K' = shrK A \<and> K \<notin> range shrK \<and> 279 Ticket = (Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>) \<and> 280 Key K \<notin> used(before 281 Says Server A (Crypt K' \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) 282 on evs) \<and> 283 Tk = CT(before 284 Says Server A (Crypt K' \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) 285 on evs)" 286apply (unfold before_def) 287apply (erule rev_mp) 288apply (erule bankerb_gets.induct, simp_all) 289txt\<open>We need this simplification only for Message 2\<close> 290apply (simp (no_asm) add: takeWhile_tail) 291apply auto 292txt\<open>Two subcases of Message 2. Subcase: used before\<close> 293apply (blast dest: used_evs_rev [THEN equalityD2, THEN contra_subsetD] 294 used_takeWhile_used) 295txt\<open>subcase: CT before\<close> 296apply (fastforce dest!: set_evs_rev [THEN equalityD2, THEN contra_subsetD, THEN takeWhile_void]) 297done 298 299 300text\<open>If the encrypted message appears then it originated with the Server 301 PROVIDED that A is NOT compromised! 302 This allows A to verify freshness of the session key. 303\<close> 304lemma Kab_authentic: 305 "\<lbrakk> Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace> 306 \<in> parts (knows Spy evs); 307 A \<notin> bad; evs \<in> bankerb_gets \<rbrakk> 308 \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>) 309 \<in> set evs" 310apply (erule rev_mp) 311apply (erule bankerb_gets.induct) 312apply (frule_tac [8] Oops_parts_knows_Spy) 313apply (frule_tac [6] BK3_msg_in_parts_knows_Spy, simp_all, blast) 314done 315 316 317text\<open>If the TICKET appears then it originated with the Server\<close> 318text\<open>FRESHNESS OF THE SESSION KEY to B\<close> 319lemma ticket_authentic: 320 "\<lbrakk> Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace> \<in> parts (knows Spy evs); 321 B \<notin> bad; evs \<in> bankerb_gets \<rbrakk> 322 \<Longrightarrow> Says Server A 323 (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, 324 Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>\<rbrace>) 325 \<in> set evs" 326apply (erule rev_mp) 327apply (erule bankerb_gets.induct) 328apply (frule_tac [8] Oops_parts_knows_Spy) 329apply (frule_tac [6] BK3_msg_in_parts_knows_Spy, simp_all, blast) 330done 331 332 333text\<open>EITHER describes the form of X when the following message is sent, 334 OR reduces it to the Fake case. 335 Use \<open>Says_Server_message_form\<close> if applicable.\<close> 336lemma Gets_Server_message_form: 337 "\<lbrakk> Gets A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>) 338 \<in> set evs; 339 evs \<in> bankerb_gets \<rbrakk> 340 \<Longrightarrow> (K \<notin> range shrK \<and> X = (Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>)) 341 | X \<in> analz (knows Spy evs)" 342apply (case_tac "A \<in> bad") 343apply (force dest!: Gets_imp_knows_Spy [THEN analz.Inj]) 344apply (blast dest!: Kab_authentic Says_Server_message_form) 345done 346 347 348text\<open>Reliability guarantees: honest agents act as we expect\<close> 349 350lemma BK3_imp_Gets: 351 "\<lbrakk> Says A B \<lbrace>Ticket, Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs; 352 A \<notin> bad; evs \<in> bankerb_gets \<rbrakk> 353 \<Longrightarrow> \<exists> Tk. Gets A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) 354 \<in> set evs" 355apply (erule rev_mp) 356apply (erule bankerb_gets.induct) 357apply auto 358done 359 360lemma BK4_imp_Gets: 361 "\<lbrakk> Says B A (Crypt K (Number Ta)) \<in> set evs; 362 B \<notin> bad; evs \<in> bankerb_gets \<rbrakk> 363 \<Longrightarrow> \<exists> Tk. Gets B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>, 364 Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs" 365apply (erule rev_mp) 366apply (erule bankerb_gets.induct) 367apply auto 368done 369 370lemma Gets_A_knows_K: 371 "\<lbrakk> Gets A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) \<in> set evs; 372 evs \<in> bankerb_gets \<rbrakk> 373 \<Longrightarrow> Key K \<in> analz (knows A evs)" 374apply (force dest: Gets_imp_knows_analz) 375done 376 377lemma Gets_B_knows_K: 378 "\<lbrakk> Gets B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>, 379 Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs; 380 evs \<in> bankerb_gets \<rbrakk> 381 \<Longrightarrow> Key K \<in> analz (knows B evs)" 382apply (force dest: Gets_imp_knows_analz) 383done 384 385 386(**** 387 The following is to prove theorems of the form 388 389 Key K \<in> analz (insert (Key KAB) (knows Spy evs)) \<Longrightarrow> 390 Key K \<in> analz (knows Spy evs) 391 392 A more general formula must be proved inductively. 393 394****) 395 396 397text\<open>Session keys are not used to encrypt other session keys\<close> 398lemma analz_image_freshK [rule_format (no_asm)]: 399 "evs \<in> bankerb_gets \<Longrightarrow> 400 \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow> 401 (Key K \<in> analz (Key`KK \<union> (knows Spy evs))) = 402 (K \<in> KK | Key K \<in> analz (knows Spy evs))" 403apply (erule bankerb_gets.induct) 404apply (drule_tac [8] Says_Server_message_form) 405apply (erule_tac [6] Gets_Server_message_form [THEN disjE], analz_freshK, spy_analz, auto) 406done 407 408 409lemma analz_insert_freshK: 410 "\<lbrakk> evs \<in> bankerb_gets; KAB \<notin> range shrK \<rbrakk> \<Longrightarrow> 411 (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = 412 (K = KAB | Key K \<in> analz (knows Spy evs))" 413by (simp only: analz_image_freshK analz_image_freshK_simps) 414 415 416text\<open>The session key K uniquely identifies the message\<close> 417lemma unique_session_keys: 418 "\<lbrakk> Says Server A 419 (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>) \<in> set evs; 420 Says Server A' 421 (Crypt (shrK A') \<lbrace>Number Tk', Agent B', Key K, X'\<rbrace>) \<in> set evs; 422 evs \<in> bankerb_gets \<rbrakk> \<Longrightarrow> A=A' \<and> Tk=Tk' \<and> B=B' \<and> X = X'" 423apply (erule rev_mp) 424apply (erule rev_mp) 425apply (erule bankerb_gets.induct) 426apply (frule_tac [8] Oops_parts_knows_Spy) 427apply (frule_tac [6] BK3_msg_in_parts_knows_Spy, simp_all) 428txt\<open>BK2: it can't be a new key\<close> 429apply blast 430done 431 432lemma unique_session_keys_Gets: 433 "\<lbrakk> Gets A 434 (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>) \<in> set evs; 435 Gets A 436 (Crypt (shrK A) \<lbrace>Number Tk', Agent B', Key K, X'\<rbrace>) \<in> set evs; 437 A \<notin> bad; evs \<in> bankerb_gets \<rbrakk> \<Longrightarrow> Tk=Tk' \<and> B=B' \<and> X = X'" 438apply (blast dest!: Kab_authentic unique_session_keys) 439done 440 441 442lemma Server_Unique: 443 "\<lbrakk> Says Server A 444 (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) \<in> set evs; 445 evs \<in> bankerb_gets \<rbrakk> \<Longrightarrow> 446 Unique Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) 447 on evs" 448apply (erule rev_mp, erule bankerb_gets.induct, simp_all add: Unique_def) 449apply blast 450done 451 452 453 454subsection\<open>Non-temporal guarantees, explicitly relying on non-occurrence of 455oops events - refined below by temporal guarantees\<close> 456 457text\<open>Non temporal treatment of confidentiality\<close> 458 459text\<open>Lemma: the session key sent in msg BK2 would be lost by oops 460 if the spy could see it!\<close> 461lemma lemma_conf [rule_format (no_asm)]: 462 "\<lbrakk> A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets \<rbrakk> 463 \<Longrightarrow> Says Server A 464 (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, 465 Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>\<rbrace>) 466 \<in> set evs \<longrightarrow> 467 Key K \<in> analz (knows Spy evs) \<longrightarrow> Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<in> set evs" 468apply (erule bankerb_gets.induct) 469apply (frule_tac [8] Says_Server_message_form) 470apply (frule_tac [6] Gets_Server_message_form [THEN disjE]) 471apply (simp_all (no_asm_simp) add: analz_insert_eq analz_insert_freshK pushes) 472txt\<open>Fake\<close> 473apply spy_analz 474txt\<open>BK2\<close> 475apply (blast intro: parts_insertI) 476txt\<open>BK3\<close> 477apply (case_tac "Aa \<in> bad") 478 prefer 2 apply (blast dest: Kab_authentic unique_session_keys) 479apply (blast dest: Gets_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad elim!: MPair_analz) 480txt\<open>Oops\<close> 481apply (blast dest: unique_session_keys) 482done 483 484 485text\<open>Confidentiality for the Server: Spy does not see the keys sent in msg BK2 486as long as they have not expired.\<close> 487lemma Confidentiality_S: 488 "\<lbrakk> Says Server A 489 (Crypt K' \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) \<in> set evs; 490 Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs; 491 A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets 492 \<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy evs)" 493apply (frule Says_Server_message_form, assumption) 494apply (blast intro: lemma_conf) 495done 496 497text\<open>Confidentiality for Alice\<close> 498lemma Confidentiality_A: 499 "\<lbrakk> Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace> \<in> parts (knows Spy evs); 500 Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs; 501 A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets 502 \<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy evs)" 503by (blast dest!: Kab_authentic Confidentiality_S) 504 505text\<open>Confidentiality for Bob\<close> 506lemma Confidentiality_B: 507 "\<lbrakk> Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace> 508 \<in> parts (knows Spy evs); 509 Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs; 510 A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets 511 \<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy evs)" 512by (blast dest!: ticket_authentic Confidentiality_S) 513 514 515text\<open>Non temporal treatment of authentication\<close> 516 517text\<open>Lemmas \<open>lemma_A\<close> and \<open>lemma_B\<close> in fact are common to both temporal and non-temporal treatments\<close> 518lemma lemma_A [rule_format]: 519 "\<lbrakk> A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets \<rbrakk> 520 \<Longrightarrow> 521 Key K \<notin> analz (knows Spy evs) \<longrightarrow> 522 Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>) 523 \<in> set evs \<longrightarrow> 524 Crypt K \<lbrace>Agent A, Number Ta\<rbrace> \<in> parts (knows Spy evs) \<longrightarrow> 525 Says A B \<lbrace>X, Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> 526 \<in> set evs" 527apply (erule bankerb_gets.induct) 528apply (frule_tac [8] Oops_parts_knows_Spy) 529apply (frule_tac [6] Gets_Server_message_form) 530apply (frule_tac [7] BK3_msg_in_parts_knows_Spy, analz_mono_contra) 531apply (simp_all (no_asm_simp) add: all_conj_distrib) 532txt\<open>Fake\<close> 533apply blast 534txt\<open>BK2\<close> 535apply (force dest: Crypt_imp_invKey_keysFor) 536txt\<open>BK3\<close> 537apply (blast dest: Kab_authentic unique_session_keys) 538done 539lemma lemma_B [rule_format]: 540 "\<lbrakk> B \<notin> bad; evs \<in> bankerb_gets \<rbrakk> 541 \<Longrightarrow> Key K \<notin> analz (knows Spy evs) \<longrightarrow> 542 Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>) 543 \<in> set evs \<longrightarrow> 544 Crypt K (Number Ta) \<in> parts (knows Spy evs) \<longrightarrow> 545 Says B A (Crypt K (Number Ta)) \<in> set evs" 546apply (erule bankerb_gets.induct) 547apply (frule_tac [8] Oops_parts_knows_Spy) 548apply (frule_tac [6] Gets_Server_message_form) 549apply (drule_tac [7] BK3_msg_in_parts_knows_Spy, analz_mono_contra) 550apply (simp_all (no_asm_simp) add: all_conj_distrib) 551txt\<open>Fake\<close> 552apply blast 553txt\<open>BK2\<close> 554apply (force dest: Crypt_imp_invKey_keysFor) 555txt\<open>BK4\<close> 556apply (blast dest: ticket_authentic unique_session_keys 557 Gets_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad) 558done 559 560 561text\<open>The "r" suffix indicates theorems where the confidentiality assumptions are relaxed by the corresponding arguments.\<close> 562 563text\<open>Authentication of A to B\<close> 564lemma B_authenticates_A_r: 565 "\<lbrakk> Crypt K \<lbrace>Agent A, Number Ta\<rbrace> \<in> parts (knows Spy evs); 566 Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace> \<in> parts (knows Spy evs); 567 Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs; 568 A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets \<rbrakk> 569 \<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>, 570 Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs" 571by (blast dest!: ticket_authentic 572 intro!: lemma_A 573 elim!: Confidentiality_S [THEN [2] rev_notE]) 574 575text\<open>Authentication of B to A\<close> 576lemma A_authenticates_B_r: 577 "\<lbrakk> Crypt K (Number Ta) \<in> parts (knows Spy evs); 578 Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace> \<in> parts (knows Spy evs); 579 Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs; 580 A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets \<rbrakk> 581 \<Longrightarrow> Says B A (Crypt K (Number Ta)) \<in> set evs" 582by (blast dest!: Kab_authentic 583 intro!: lemma_B elim!: Confidentiality_S [THEN [2] rev_notE]) 584 585lemma B_authenticates_A: 586 "\<lbrakk> Crypt K \<lbrace>Agent A, Number Ta\<rbrace> \<in> parts (spies evs); 587 Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace> \<in> parts (spies evs); 588 Key K \<notin> analz (spies evs); 589 A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets \<rbrakk> 590 \<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>, 591 Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs" 592apply (blast dest!: ticket_authentic intro!: lemma_A) 593done 594 595lemma A_authenticates_B: 596 "\<lbrakk> Crypt K (Number Ta) \<in> parts (spies evs); 597 Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace> \<in> parts (spies evs); 598 Key K \<notin> analz (spies evs); 599 A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets \<rbrakk> 600 \<Longrightarrow> Says B A (Crypt K (Number Ta)) \<in> set evs" 601apply (blast dest!: Kab_authentic intro!: lemma_B) 602done 603 604 605subsection\<open>Temporal guarantees, relying on a temporal check that insures that 606no oops event occurred. These are available in the sense of goal availability\<close> 607 608 609text\<open>Temporal treatment of confidentiality\<close> 610 611text\<open>Lemma: the session key sent in msg BK2 would be EXPIRED 612 if the spy could see it!\<close> 613lemma lemma_conf_temporal [rule_format (no_asm)]: 614 "\<lbrakk> A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets \<rbrakk> 615 \<Longrightarrow> Says Server A 616 (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, 617 Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>\<rbrace>) 618 \<in> set evs \<longrightarrow> 619 Key K \<in> analz (knows Spy evs) \<longrightarrow> expiredK Tk evs" 620apply (erule bankerb_gets.induct) 621apply (frule_tac [8] Says_Server_message_form) 622apply (frule_tac [6] Gets_Server_message_form [THEN disjE]) 623apply (simp_all (no_asm_simp) add: less_SucI analz_insert_eq analz_insert_freshK pushes) 624txt\<open>Fake\<close> 625apply spy_analz 626txt\<open>BK2\<close> 627apply (blast intro: parts_insertI less_SucI) 628txt\<open>BK3\<close> 629apply (case_tac "Aa \<in> bad") 630 prefer 2 apply (blast dest: Kab_authentic unique_session_keys) 631apply (blast dest: Gets_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad elim!: MPair_analz intro: less_SucI) 632txt\<open>Oops: PROOF FAILS if unsafe intro below\<close> 633apply (blast dest: unique_session_keys intro!: less_SucI) 634done 635 636 637text\<open>Confidentiality for the Server: Spy does not see the keys sent in msg BK2 638as long as they have not expired.\<close> 639lemma Confidentiality_S_temporal: 640 "\<lbrakk> Says Server A 641 (Crypt K' \<lbrace>Number T, Agent B, Key K, X\<rbrace>) \<in> set evs; 642 \<not> expiredK T evs; 643 A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets 644 \<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy evs)" 645apply (frule Says_Server_message_form, assumption) 646apply (blast intro: lemma_conf_temporal) 647done 648 649text\<open>Confidentiality for Alice\<close> 650lemma Confidentiality_A_temporal: 651 "\<lbrakk> Crypt (shrK A) \<lbrace>Number T, Agent B, Key K, X\<rbrace> \<in> parts (knows Spy evs); 652 \<not> expiredK T evs; 653 A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets 654 \<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy evs)" 655by (blast dest!: Kab_authentic Confidentiality_S_temporal) 656 657text\<open>Confidentiality for Bob\<close> 658lemma Confidentiality_B_temporal: 659 "\<lbrakk> Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace> 660 \<in> parts (knows Spy evs); 661 \<not> expiredK Tk evs; 662 A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets 663 \<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy evs)" 664by (blast dest!: ticket_authentic Confidentiality_S_temporal) 665 666 667text\<open>Temporal treatment of authentication\<close> 668 669text\<open>Authentication of A to B\<close> 670lemma B_authenticates_A_temporal: 671 "\<lbrakk> Crypt K \<lbrace>Agent A, Number Ta\<rbrace> \<in> parts (knows Spy evs); 672 Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace> 673 \<in> parts (knows Spy evs); 674 \<not> expiredK Tk evs; 675 A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets \<rbrakk> 676 \<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>, 677 Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs" 678by (blast dest!: ticket_authentic 679 intro!: lemma_A 680 elim!: Confidentiality_S_temporal [THEN [2] rev_notE]) 681 682text\<open>Authentication of B to A\<close> 683lemma A_authenticates_B_temporal: 684 "\<lbrakk> Crypt K (Number Ta) \<in> parts (knows Spy evs); 685 Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace> 686 \<in> parts (knows Spy evs); 687 \<not> expiredK Tk evs; 688 A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets \<rbrakk> 689 \<Longrightarrow> Says B A (Crypt K (Number Ta)) \<in> set evs" 690by (blast dest!: Kab_authentic 691 intro!: lemma_B elim!: Confidentiality_S_temporal [THEN [2] rev_notE]) 692 693 694subsection\<open>Combined guarantees of key distribution and non-injective agreement on the session keys\<close> 695 696lemma B_authenticates_and_keydist_to_A: 697 "\<lbrakk> Gets B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>, 698 Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs; 699 Key K \<notin> analz (spies evs); 700 A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets \<rbrakk> 701 \<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>, 702 Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs 703 \<and> Key K \<in> analz (knows A evs)" 704apply (blast dest: B_authenticates_A BK3_imp_Gets Gets_A_knows_K) 705done 706 707lemma A_authenticates_and_keydist_to_B: 708 "\<lbrakk> Gets A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) \<in> set evs; 709 Gets A (Crypt K (Number Ta)) \<in> set evs; 710 Key K \<notin> analz (spies evs); 711 A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets \<rbrakk> 712 \<Longrightarrow> Says B A (Crypt K (Number Ta)) \<in> set evs 713 \<and> Key K \<in> analz (knows B evs)" 714apply (blast dest: A_authenticates_B BK4_imp_Gets Gets_B_knows_K) 715done 716 717 718 719 720 721end 722