1(* Title: HOL/Auth/KerberosIV.thy 2 Author: Giampaolo Bella, Cambridge University Computer Laboratory 3 Copyright 1998 University of Cambridge 4*) 5 6section\<open>The Kerberos Protocol, Version IV\<close> 7 8theory KerberosIV imports Public begin 9 10text\<open>The "u" prefix indicates theorems referring to an updated version of the protocol. The "r" suffix indicates theorems where the confidentiality assumptions are relaxed by the corresponding arguments.\<close> 11 12abbreviation 13 Kas :: agent where "Kas == Server" 14 15abbreviation 16 Tgs :: agent where "Tgs == Friend 0" 17 18 19axiomatization where 20 Tgs_not_bad [iff]: "Tgs \<notin> bad" 21 \<comment> \<open>Tgs is secure --- we already know that Kas is secure\<close> 22 23definition 24 (* authKeys are those contained in an authTicket *) 25 authKeys :: "event list \<Rightarrow> key set" where 26 "authKeys evs = {authK. \<exists>A Peer Ta. Says Kas A 27 (Crypt (shrK A) \<lbrace>Key authK, Agent Peer, Number Ta, 28 (Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key authK, Number Ta\<rbrace>) 29 \<rbrace>) \<in> set evs}" 30 31definition 32 (* A is the true creator of X if she has sent X and X never appeared on 33 the trace before this event. Recall that traces grow from head. *) 34 Issues :: "[agent, agent, msg, event list] \<Rightarrow> bool" 35 ("_ Issues _ with _ on _" [50, 0, 0, 50] 50) where 36 "(A Issues B with X on evs) = 37 (\<exists>Y. Says A B Y \<in> set evs \<and> X \<in> parts {Y} \<and> 38 X \<notin> parts (spies (takeWhile (\<lambda>z. z \<noteq> Says A B Y) (rev evs))))" 39 40definition 41 (* Yields the subtrace of a given trace from its beginning to a given event *) 42 before :: "[event, event list] \<Rightarrow> event list" ("before _ on _" [0, 50] 50) 43 where "(before ev on evs) = takeWhile (\<lambda>z. z \<noteq> ev) (rev evs)" 44 45definition 46 (* States than an event really appears only once on a trace *) 47 Unique :: "[event, event list] \<Rightarrow> bool" ("Unique _ on _" [0, 50] 50) 48 where "(Unique ev on evs) = (ev \<notin> set (tl (dropWhile (\<lambda>z. z \<noteq> ev) evs)))" 49 50 51consts 52 (*Duration of the authentication key*) 53 authKlife :: nat 54 55 (*Duration of the service key*) 56 servKlife :: nat 57 58 (*Duration of an authenticator*) 59 authlife :: nat 60 61 (*Upper bound on the time of reaction of a server*) 62 replylife :: nat 63 64specification (authKlife) 65 authKlife_LB [iff]: "2 \<le> authKlife" 66 by blast 67 68specification (servKlife) 69 servKlife_LB [iff]: "2 + authKlife \<le> servKlife" 70 by blast 71 72specification (authlife) 73 authlife_LB [iff]: "Suc 0 \<le> authlife" 74 by blast 75 76specification (replylife) 77 replylife_LB [iff]: "Suc 0 \<le> replylife" 78 by blast 79 80abbreviation 81 (*The current time is the length of the trace*) 82 CT :: "event list \<Rightarrow> nat" where 83 "CT == length" 84 85abbreviation 86 expiredAK :: "[nat, event list] \<Rightarrow> bool" where 87 "expiredAK Ta evs == authKlife + Ta < CT evs" 88 89abbreviation 90 expiredSK :: "[nat, event list] \<Rightarrow> bool" where 91 "expiredSK Ts evs == servKlife + Ts < CT evs" 92 93abbreviation 94 expiredA :: "[nat, event list] \<Rightarrow> bool" where 95 "expiredA T evs == authlife + T < CT evs" 96 97abbreviation 98 valid :: "[nat, nat] \<Rightarrow> bool" ("valid _ wrt _" [0, 50] 50) where 99 "valid T1 wrt T2 == T1 \<le> replylife + T2" 100 101(*---------------------------------------------------------------------*) 102 103 104(* Predicate formalising the association between authKeys and servKeys *) 105definition AKcryptSK :: "[key, key, event list] \<Rightarrow> bool" where 106 "AKcryptSK authK servK evs == 107 \<exists>A B Ts. 108 Says Tgs A (Crypt authK 109 \<lbrace>Key servK, Agent B, Number Ts, 110 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<rbrace>) 111 \<in> set evs" 112 113inductive_set kerbIV :: "event list set" 114 where 115 116 Nil: "[] \<in> kerbIV" 117 118 | Fake: "\<lbrakk> evsf \<in> kerbIV; X \<in> synth (analz (spies evsf)) \<rbrakk> 119 \<Longrightarrow> Says Spy B X # evsf \<in> kerbIV" 120 121(* FROM the initiator *) 122 | K1: "\<lbrakk> evs1 \<in> kerbIV \<rbrakk> 123 \<Longrightarrow> Says A Kas \<lbrace>Agent A, Agent Tgs, Number (CT evs1)\<rbrace> # evs1 124 \<in> kerbIV" 125 126(* Adding the timestamp serves to A in K3 to check that 127 she doesn't get a reply too late. This kind of timeouts are ordinary. 128 If a server's reply is late, then it is likely to be fake. *) 129 130(*---------------------------------------------------------------------*) 131 132(*FROM Kas *) 133 | K2: "\<lbrakk> evs2 \<in> kerbIV; Key authK \<notin> used evs2; authK \<in> symKeys; 134 Says A' Kas \<lbrace>Agent A, Agent Tgs, Number T1\<rbrace> \<in> set evs2 \<rbrakk> 135 \<Longrightarrow> Says Kas A 136 (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number (CT evs2), 137 (Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, 138 Number (CT evs2)\<rbrace>)\<rbrace>) # evs2 \<in> kerbIV" 139(* 140 The internal encryption builds the authTicket. 141 The timestamp doesn't change inside the two encryptions: the external copy 142 will be used by the initiator in K3; the one inside the 143 authTicket by Tgs in K4. 144*) 145 146(*---------------------------------------------------------------------*) 147 148(* FROM the initiator *) 149 | K3: "\<lbrakk> evs3 \<in> kerbIV; 150 Says A Kas \<lbrace>Agent A, Agent Tgs, Number T1\<rbrace> \<in> set evs3; 151 Says Kas' A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, 152 authTicket\<rbrace>) \<in> set evs3; 153 valid Ta wrt T1 154 \<rbrakk> 155 \<Longrightarrow> Says A Tgs \<lbrace>authTicket, 156 (Crypt authK \<lbrace>Agent A, Number (CT evs3)\<rbrace>), 157 Agent B\<rbrace> # evs3 \<in> kerbIV" 158(*The two events amongst the premises allow A to accept only those authKeys 159 that are not issued late. *) 160 161(*---------------------------------------------------------------------*) 162 163(* FROM Tgs *) 164(* Note that the last temporal check is not mentioned in the original MIT 165 specification. Adding it makes many goals "available" to the peers. 166 Theorems that exploit it have the suffix `_u', which stands for updated 167 protocol. 168*) 169 | K4: "\<lbrakk> evs4 \<in> kerbIV; Key servK \<notin> used evs4; servK \<in> symKeys; 170 B \<noteq> Tgs; authK \<in> symKeys; 171 Says A' Tgs \<lbrace> 172 (Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, 173 Number Ta\<rbrace>), 174 (Crypt authK \<lbrace>Agent A, Number T2\<rbrace>), Agent B\<rbrace> 175 \<in> set evs4; 176 \<not> expiredAK Ta evs4; 177 \<not> expiredA T2 evs4; 178 servKlife + (CT evs4) \<le> authKlife + Ta 179 \<rbrakk> 180 \<Longrightarrow> Says Tgs A 181 (Crypt authK \<lbrace>Key servK, Agent B, Number (CT evs4), 182 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, 183 Number (CT evs4)\<rbrace> \<rbrace>) 184 # evs4 \<in> kerbIV" 185(* Tgs creates a new session key per each request for a service, without 186 checking if there is still a fresh one for that service. 187 The cipher under Tgs' key is the authTicket, the cipher under B's key 188 is the servTicket, which is built now. 189 NOTE that the last temporal check is not present in the MIT specification. 190 191*) 192 193(*---------------------------------------------------------------------*) 194 195(* FROM the initiator *) 196 | K5: "\<lbrakk> evs5 \<in> kerbIV; authK \<in> symKeys; servK \<in> symKeys; 197 Says A Tgs 198 \<lbrace>authTicket, Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, 199 Agent B\<rbrace> 200 \<in> set evs5; 201 Says Tgs' A 202 (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 203 \<in> set evs5; 204 valid Ts wrt T2 \<rbrakk> 205 \<Longrightarrow> Says A B \<lbrace>servTicket, 206 Crypt servK \<lbrace>Agent A, Number (CT evs5)\<rbrace> \<rbrace> 207 # evs5 \<in> kerbIV" 208(* Checks similar to those in K3. *) 209 210(*---------------------------------------------------------------------*) 211 212(* FROM the responder*) 213 | K6: "\<lbrakk> evs6 \<in> kerbIV; 214 Says A' B \<lbrace> 215 (Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>), 216 (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>)\<rbrace> 217 \<in> set evs6; 218 \<not> expiredSK Ts evs6; 219 \<not> expiredA T3 evs6 220 \<rbrakk> 221 \<Longrightarrow> Says B A (Crypt servK (Number T3)) 222 # evs6 \<in> kerbIV" 223(* Checks similar to those in K4. *) 224 225(*---------------------------------------------------------------------*) 226 227(* Leaking an authK... *) 228 | Oops1: "\<lbrakk> evsO1 \<in> kerbIV; A \<noteq> Spy; 229 Says Kas A 230 (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, 231 authTicket\<rbrace>) \<in> set evsO1; 232 expiredAK Ta evsO1 \<rbrakk> 233 \<Longrightarrow> Says A Spy \<lbrace>Agent A, Agent Tgs, Number Ta, Key authK\<rbrace> 234 # evsO1 \<in> kerbIV" 235 236(*---------------------------------------------------------------------*) 237 238(*Leaking a servK... *) 239 | Oops2: "\<lbrakk> evsO2 \<in> kerbIV; A \<noteq> Spy; 240 Says Tgs A 241 (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 242 \<in> set evsO2; 243 expiredSK Ts evsO2 \<rbrakk> 244 \<Longrightarrow> Says A Spy \<lbrace>Agent A, Agent B, Number Ts, Key servK\<rbrace> 245 # evsO2 \<in> kerbIV" 246 247(*---------------------------------------------------------------------*) 248 249declare Says_imp_knows_Spy [THEN parts.Inj, dest] 250declare parts.Body [dest] 251declare analz_into_parts [dest] 252declare Fake_parts_insert_in_Un [dest] 253 254 255subsection\<open>Lemmas about lists, for reasoning about Issues\<close> 256 257lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)" 258apply (induct_tac "evs") 259apply (rename_tac [2] a b) 260apply (induct_tac [2] a, auto) 261done 262 263lemma spies_Gets_rev: "spies (evs @ [Gets A X]) = spies evs" 264apply (induct_tac "evs") 265apply (rename_tac [2] a b) 266apply (induct_tac [2] a, auto) 267done 268 269lemma spies_Notes_rev: "spies (evs @ [Notes A X]) = 270 (if A\<in>bad then insert X (spies evs) else spies evs)" 271apply (induct_tac "evs") 272apply (rename_tac [2] a b) 273apply (induct_tac [2] a, auto) 274done 275 276lemma spies_evs_rev: "spies evs = spies (rev evs)" 277apply (induct_tac "evs") 278apply (rename_tac [2] a b) 279apply (induct_tac [2] a) 280apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev) 281done 282 283lemmas parts_spies_evs_revD2 = spies_evs_rev [THEN equalityD2, THEN parts_mono] 284 285lemma spies_takeWhile: "spies (takeWhile P evs) \<subseteq> spies evs" 286apply (induct_tac "evs") 287apply (rename_tac [2] a b) 288apply (induct_tac [2] "a", auto) 289txt\<open>Resembles \<open>used_subset_append\<close> in theory Event.\<close> 290done 291 292lemmas parts_spies_takeWhile_mono = spies_takeWhile [THEN parts_mono] 293 294 295subsection\<open>Lemmas about @{term authKeys}\<close> 296 297lemma authKeys_empty: "authKeys [] = {}" 298apply (unfold authKeys_def) 299apply (simp (no_asm)) 300done 301 302lemma authKeys_not_insert: 303 "(\<forall>A Ta akey Peer. 304 ev \<noteq> Says Kas A (Crypt (shrK A) \<lbrace>akey, Agent Peer, Ta, 305 (Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, akey, Ta\<rbrace>)\<rbrace>)) 306 \<Longrightarrow> authKeys (ev # evs) = authKeys evs" 307by (unfold authKeys_def, auto) 308 309lemma authKeys_insert: 310 "authKeys 311 (Says Kas A (Crypt (shrK A) \<lbrace>Key K, Agent Peer, Number Ta, 312 (Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key K, Number Ta\<rbrace>)\<rbrace>) # evs) 313 = insert K (authKeys evs)" 314by (unfold authKeys_def, auto) 315 316lemma authKeys_simp: 317 "K \<in> authKeys 318 (Says Kas A (Crypt (shrK A) \<lbrace>Key K', Agent Peer, Number Ta, 319 (Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key K', Number Ta\<rbrace>)\<rbrace>) # evs) 320 \<Longrightarrow> K = K' | K \<in> authKeys evs" 321by (unfold authKeys_def, auto) 322 323lemma authKeysI: 324 "Says Kas A (Crypt (shrK A) \<lbrace>Key K, Agent Tgs, Number Ta, 325 (Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key K, Number Ta\<rbrace>)\<rbrace>) \<in> set evs 326 \<Longrightarrow> K \<in> authKeys evs" 327by (unfold authKeys_def, auto) 328 329lemma authKeys_used: "K \<in> authKeys evs \<Longrightarrow> Key K \<in> used evs" 330by (simp add: authKeys_def, blast) 331 332 333subsection\<open>Forwarding Lemmas\<close> 334 335text\<open>--For reasoning about the encrypted portion of message K3--\<close> 336lemma K3_msg_in_parts_spies: 337 "Says Kas' A (Crypt KeyA \<lbrace>authK, Peer, Ta, authTicket\<rbrace>) 338 \<in> set evs \<Longrightarrow> authTicket \<in> parts (spies evs)" 339by blast 340 341lemma Oops_range_spies1: 342 "\<lbrakk> Says Kas A (Crypt KeyA \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>) 343 \<in> set evs ; 344 evs \<in> kerbIV \<rbrakk> \<Longrightarrow> authK \<notin> range shrK \<and> authK \<in> symKeys" 345apply (erule rev_mp) 346apply (erule kerbIV.induct, auto) 347done 348 349text\<open>--For reasoning about the encrypted portion of message K5--\<close> 350lemma K5_msg_in_parts_spies: 351 "Says Tgs' A (Crypt authK \<lbrace>servK, Agent B, Ts, servTicket\<rbrace>) 352 \<in> set evs \<Longrightarrow> servTicket \<in> parts (spies evs)" 353by blast 354 355lemma Oops_range_spies2: 356 "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>) 357 \<in> set evs ; 358 evs \<in> kerbIV \<rbrakk> \<Longrightarrow> servK \<notin> range shrK \<and> servK \<in> symKeys" 359apply (erule rev_mp) 360apply (erule kerbIV.induct, auto) 361done 362 363lemma Says_ticket_parts: 364 "Says S A (Crypt K \<lbrace>SesKey, B, TimeStamp, Ticket\<rbrace>) \<in> set evs 365 \<Longrightarrow> Ticket \<in> parts (spies evs)" 366by blast 367 368(*Spy never sees another agent's shared key! (unless it's lost at start)*) 369lemma Spy_see_shrK [simp]: 370 "evs \<in> kerbIV \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)" 371apply (erule kerbIV.induct) 372apply (frule_tac [7] K5_msg_in_parts_spies) 373apply (frule_tac [5] K3_msg_in_parts_spies, simp_all) 374apply (blast+) 375done 376 377lemma Spy_analz_shrK [simp]: 378 "evs \<in> kerbIV \<Longrightarrow> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)" 379by auto 380 381lemma Spy_see_shrK_D [dest!]: 382 "\<lbrakk> Key (shrK A) \<in> parts (spies evs); evs \<in> kerbIV \<rbrakk> \<Longrightarrow> A\<in>bad" 383by (blast dest: Spy_see_shrK) 384 385lemmas Spy_analz_shrK_D = analz_subset_parts [THEN subsetD, THEN Spy_see_shrK_D, dest!] 386 387text\<open>Nobody can have used non-existent keys!\<close> 388lemma new_keys_not_used [simp]: 389 "\<lbrakk>Key K \<notin> used evs; K \<in> symKeys; evs \<in> kerbIV\<rbrakk> 390 \<Longrightarrow> K \<notin> keysFor (parts (spies evs))" 391apply (erule rev_mp) 392apply (erule kerbIV.induct) 393apply (frule_tac [7] K5_msg_in_parts_spies) 394apply (frule_tac [5] K3_msg_in_parts_spies, simp_all) 395txt\<open>Fake\<close> 396apply (force dest!: keysFor_parts_insert) 397txt\<open>Others\<close> 398apply (force dest!: analz_shrK_Decrypt)+ 399done 400 401(*Earlier, all protocol proofs declared this theorem. 402 But few of them actually need it! (Another is Yahalom) *) 403lemma new_keys_not_analzd: 404 "\<lbrakk>evs \<in> kerbIV; K \<in> symKeys; Key K \<notin> used evs\<rbrakk> 405 \<Longrightarrow> K \<notin> keysFor (analz (spies evs))" 406by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD]) 407 408 409 410subsection\<open>Lemmas for reasoning about predicate "before"\<close> 411 412lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)" 413apply (induct_tac "evs") 414apply simp 415apply (rename_tac a b) 416apply (induct_tac "a") 417apply auto 418done 419 420lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)" 421apply (induct_tac "evs") 422apply simp 423apply (rename_tac a b) 424apply (induct_tac "a") 425apply auto 426done 427 428lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs" 429apply (induct_tac "evs") 430apply simp 431apply (rename_tac a b) 432apply (induct_tac "a") 433apply auto 434done 435 436lemma used_evs_rev: "used evs = used (rev evs)" 437apply (induct_tac "evs") 438apply simp 439apply (rename_tac a b) 440apply (induct_tac "a") 441apply (simp add: used_Says_rev) 442apply (simp add: used_Gets_rev) 443apply (simp add: used_Notes_rev) 444done 445 446lemma used_takeWhile_used [rule_format]: 447 "x \<in> used (takeWhile P X) \<longrightarrow> x \<in> used X" 448apply (induct_tac "X") 449apply simp 450apply (rename_tac a b) 451apply (induct_tac "a") 452apply (simp_all add: used_Nil) 453apply (blast dest!: initState_into_used)+ 454done 455 456lemma set_evs_rev: "set evs = set (rev evs)" 457by auto 458 459lemma takeWhile_void [rule_format]: 460 "x \<notin> set evs \<longrightarrow> takeWhile (\<lambda>z. z \<noteq> x) evs = evs" 461by auto 462 463 464subsection\<open>Regularity Lemmas\<close> 465text\<open>These concern the form of items passed in messages\<close> 466 467text\<open>Describes the form of all components sent by Kas\<close> 468lemma Says_Kas_message_form: 469 "\<lbrakk> Says Kas A (Crypt K \<lbrace>Key authK, Agent Peer, Number Ta, authTicket\<rbrace>) 470 \<in> set evs; 471 evs \<in> kerbIV \<rbrakk> \<Longrightarrow> 472 K = shrK A \<and> Peer = Tgs \<and> 473 authK \<notin> range shrK \<and> authK \<in> authKeys evs \<and> authK \<in> symKeys \<and> 474 authTicket = (Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>) \<and> 475 Key authK \<notin> used(before 476 Says Kas A (Crypt K \<lbrace>Key authK, Agent Peer, Number Ta, authTicket\<rbrace>) 477 on evs) \<and> 478 Ta = CT (before 479 Says Kas A (Crypt K \<lbrace>Key authK, Agent Peer, Number Ta, authTicket\<rbrace>) 480 on evs)" 481apply (unfold before_def) 482apply (erule rev_mp) 483apply (erule kerbIV.induct) 484apply (simp_all (no_asm) add: authKeys_def authKeys_insert, blast, blast) 485txt\<open>K2\<close> 486apply (simp (no_asm) add: takeWhile_tail) 487apply (rule conjI) 488apply (metis Key_not_used authKeys_used length_rev set_rev takeWhile_void used_evs_rev) 489apply blast+ 490done 491 492 493 494(*This lemma is essential for proving Says_Tgs_message_form: 495 496 the session key authK 497 supplied by Kas in the authentication ticket 498 cannot be a long-term key! 499 500 Generalised to any session keys (both authK and servK). 501*) 502lemma SesKey_is_session_key: 503 "\<lbrakk> Crypt (shrK Tgs_B) \<lbrace>Agent A, Agent Tgs_B, Key SesKey, Number T\<rbrace> 504 \<in> parts (spies evs); Tgs_B \<notin> bad; 505 evs \<in> kerbIV \<rbrakk> 506 \<Longrightarrow> SesKey \<notin> range shrK" 507apply (erule rev_mp) 508apply (erule kerbIV.induct) 509apply (frule_tac [7] K5_msg_in_parts_spies) 510apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast) 511done 512 513lemma authTicket_authentic: 514 "\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace> 515 \<in> parts (spies evs); 516 evs \<in> kerbIV \<rbrakk> 517 \<Longrightarrow> Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, 518 Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>) 519 \<in> set evs" 520apply (erule rev_mp) 521apply (erule kerbIV.induct) 522apply (frule_tac [7] K5_msg_in_parts_spies) 523apply (frule_tac [5] K3_msg_in_parts_spies, simp_all) 524txt\<open>Fake, K4\<close> 525apply (blast+) 526done 527 528lemma authTicket_crypt_authK: 529 "\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace> 530 \<in> parts (spies evs); 531 evs \<in> kerbIV \<rbrakk> 532 \<Longrightarrow> authK \<in> authKeys evs" 533apply (frule authTicket_authentic, assumption) 534apply (simp (no_asm) add: authKeys_def) 535apply blast 536done 537 538text\<open>Describes the form of servK, servTicket and authK sent by Tgs\<close> 539lemma Says_Tgs_message_form: 540 "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 541 \<in> set evs; 542 evs \<in> kerbIV \<rbrakk> 543 \<Longrightarrow> B \<noteq> Tgs \<and> 544 authK \<notin> range shrK \<and> authK \<in> authKeys evs \<and> authK \<in> symKeys \<and> 545 servK \<notin> range shrK \<and> servK \<notin> authKeys evs \<and> servK \<in> symKeys \<and> 546 servTicket = (Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>) \<and> 547 Key servK \<notin> used (before 548 Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 549 on evs) \<and> 550 Ts = CT(before 551 Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 552 on evs) " 553apply (unfold before_def) 554apply (erule rev_mp) 555apply (erule kerbIV.induct) 556apply (simp_all add: authKeys_insert authKeys_not_insert authKeys_empty authKeys_simp, blast) 557txt\<open>We need this simplification only for Message 4\<close> 558apply (simp (no_asm) add: takeWhile_tail) 559apply auto 560txt\<open>Five subcases of Message 4\<close> 561apply (blast dest!: SesKey_is_session_key) 562apply (blast dest: authTicket_crypt_authK) 563apply (blast dest!: authKeys_used Says_Kas_message_form) 564txt\<open>subcase: used before\<close> 565apply (metis used_evs_rev used_takeWhile_used) 566txt\<open>subcase: CT before\<close> 567apply (metis length_rev set_evs_rev takeWhile_void) 568done 569 570lemma authTicket_form: 571 "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Ta, authTicket\<rbrace> 572 \<in> parts (spies evs); 573 A \<notin> bad; 574 evs \<in> kerbIV \<rbrakk> 575 \<Longrightarrow> authK \<notin> range shrK \<and> authK \<in> symKeys \<and> 576 authTicket = Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Ta\<rbrace>" 577apply (erule rev_mp) 578apply (erule kerbIV.induct) 579apply (frule_tac [7] K5_msg_in_parts_spies) 580apply (frule_tac [5] K3_msg_in_parts_spies, simp_all) 581apply (blast+) 582done 583 584text\<open>This form holds also over an authTicket, but is not needed below.\<close> 585lemma servTicket_form: 586 "\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace> 587 \<in> parts (spies evs); 588 Key authK \<notin> analz (spies evs); 589 evs \<in> kerbIV \<rbrakk> 590 \<Longrightarrow> servK \<notin> range shrK \<and> servK \<in> symKeys \<and> 591 (\<exists>A. servTicket = Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace>)" 592apply (erule rev_mp) 593apply (erule rev_mp) 594apply (erule kerbIV.induct, analz_mono_contra) 595apply (frule_tac [7] K5_msg_in_parts_spies) 596apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast) 597done 598 599text\<open>Essentially the same as \<open>authTicket_form\<close>\<close> 600lemma Says_kas_message_form: 601 "\<lbrakk> Says Kas' A (Crypt (shrK A) 602 \<lbrace>Key authK, Agent Tgs, Ta, authTicket\<rbrace>) \<in> set evs; 603 evs \<in> kerbIV \<rbrakk> 604 \<Longrightarrow> authK \<notin> range shrK \<and> authK \<in> symKeys \<and> 605 authTicket = 606 Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Ta\<rbrace> 607 | authTicket \<in> analz (spies evs)" 608by (blast dest: analz_shrK_Decrypt authTicket_form 609 Says_imp_spies [THEN analz.Inj]) 610 611lemma Says_tgs_message_form: 612 "\<lbrakk> Says Tgs' A (Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>) 613 \<in> set evs; authK \<in> symKeys; 614 evs \<in> kerbIV \<rbrakk> 615 \<Longrightarrow> servK \<notin> range shrK \<and> 616 (\<exists>A. servTicket = 617 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace>) 618 | servTicket \<in> analz (spies evs)" 619by (metis Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Decrypt analz.Snd invKey_K servTicket_form) 620 621 622subsection\<open>Authenticity theorems: confirm origin of sensitive messages\<close> 623 624lemma authK_authentic: 625 "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace> 626 \<in> parts (spies evs); 627 A \<notin> bad; evs \<in> kerbIV \<rbrakk> 628 \<Longrightarrow> Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>) 629 \<in> set evs" 630apply (erule rev_mp) 631apply (erule kerbIV.induct) 632apply (frule_tac [7] K5_msg_in_parts_spies) 633apply (frule_tac [5] K3_msg_in_parts_spies, simp_all) 634txt\<open>Fake\<close> 635apply blast 636txt\<open>K4\<close> 637apply (blast dest!: authTicket_authentic [THEN Says_Kas_message_form]) 638done 639 640text\<open>If a certain encrypted message appears then it originated with Tgs\<close> 641lemma servK_authentic: 642 "\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace> 643 \<in> parts (spies evs); 644 Key authK \<notin> analz (spies evs); 645 authK \<notin> range shrK; 646 evs \<in> kerbIV \<rbrakk> 647 \<Longrightarrow> \<exists>A. Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 648 \<in> set evs" 649apply (erule rev_mp) 650apply (erule rev_mp) 651apply (erule kerbIV.induct, analz_mono_contra) 652apply (frule_tac [7] K5_msg_in_parts_spies) 653apply (frule_tac [5] K3_msg_in_parts_spies, simp_all) 654txt\<open>Fake\<close> 655apply blast 656txt\<open>K2\<close> 657apply blast 658txt\<open>K4\<close> 659apply auto 660done 661 662lemma servK_authentic_bis: 663 "\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace> 664 \<in> parts (spies evs); 665 Key authK \<notin> analz (spies evs); 666 B \<noteq> Tgs; 667 evs \<in> kerbIV \<rbrakk> 668 \<Longrightarrow> \<exists>A. Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 669 \<in> set evs" 670apply (erule rev_mp) 671apply (erule rev_mp) 672apply (erule kerbIV.induct, analz_mono_contra) 673apply (frule_tac [7] K5_msg_in_parts_spies) 674apply (frule_tac [5] K3_msg_in_parts_spies, simp_all) 675txt\<open>Fake\<close> 676apply blast 677txt\<open>K4\<close> 678apply blast 679done 680 681text\<open>Authenticity of servK for B\<close> 682lemma servTicket_authentic_Tgs: 683 "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> 684 \<in> parts (spies evs); B \<noteq> Tgs; B \<notin> bad; 685 evs \<in> kerbIV \<rbrakk> 686 \<Longrightarrow> \<exists>authK. 687 Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, 688 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>) 689 \<in> set evs" 690apply (erule rev_mp) 691apply (erule rev_mp) 692apply (erule kerbIV.induct) 693apply (frule_tac [7] K5_msg_in_parts_spies) 694apply (frule_tac [5] K3_msg_in_parts_spies, simp_all) 695apply blast+ 696done 697 698text\<open>Anticipated here from next subsection\<close> 699lemma K4_imp_K2: 700"\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 701 \<in> set evs; evs \<in> kerbIV\<rbrakk> 702 \<Longrightarrow> \<exists>Ta. Says Kas A 703 (Crypt (shrK A) 704 \<lbrace>Key authK, Agent Tgs, Number Ta, 705 Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>) 706 \<in> set evs" 707apply (erule rev_mp) 708apply (erule kerbIV.induct) 709apply (frule_tac [7] K5_msg_in_parts_spies) 710apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, auto) 711apply (blast dest!: Says_imp_spies [THEN parts.Inj, THEN parts.Fst, THEN authTicket_authentic]) 712done 713 714text\<open>Anticipated here from next subsection\<close> 715lemma u_K4_imp_K2: 716"\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 717 \<in> set evs; evs \<in> kerbIV\<rbrakk> 718 \<Longrightarrow> \<exists>Ta. (Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, 719 Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>) 720 \<in> set evs 721 \<and> servKlife + Ts \<le> authKlife + Ta)" 722apply (erule rev_mp) 723apply (erule kerbIV.induct) 724apply (frule_tac [7] K5_msg_in_parts_spies) 725apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, auto) 726apply (blast dest!: Says_imp_spies [THEN parts.Inj, THEN parts.Fst, THEN authTicket_authentic]) 727done 728 729lemma servTicket_authentic_Kas: 730 "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> 731 \<in> parts (spies evs); B \<noteq> Tgs; B \<notin> bad; 732 evs \<in> kerbIV \<rbrakk> 733 \<Longrightarrow> \<exists>authK Ta. 734 Says Kas A 735 (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, 736 Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>) 737 \<in> set evs" 738by (blast dest!: servTicket_authentic_Tgs K4_imp_K2) 739 740lemma u_servTicket_authentic_Kas: 741 "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> 742 \<in> parts (spies evs); B \<noteq> Tgs; B \<notin> bad; 743 evs \<in> kerbIV \<rbrakk> 744 \<Longrightarrow> \<exists>authK Ta. Says Kas A (Crypt(shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, 745 Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>) 746 \<in> set evs 747 \<and> servKlife + Ts \<le> authKlife + Ta" 748by (blast dest!: servTicket_authentic_Tgs u_K4_imp_K2) 749 750lemma servTicket_authentic: 751 "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> 752 \<in> parts (spies evs); B \<noteq> Tgs; B \<notin> bad; 753 evs \<in> kerbIV \<rbrakk> 754 \<Longrightarrow> \<exists>Ta authK. 755 Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, 756 Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>) 757 \<in> set evs 758 \<and> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, 759 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>) 760 \<in> set evs" 761by (blast dest: servTicket_authentic_Tgs K4_imp_K2) 762 763lemma u_servTicket_authentic: 764 "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> 765 \<in> parts (spies evs); B \<noteq> Tgs; B \<notin> bad; 766 evs \<in> kerbIV \<rbrakk> 767 \<Longrightarrow> \<exists>Ta authK. 768 (Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, 769 Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>) 770 \<in> set evs 771 \<and> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, 772 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>) 773 \<in> set evs 774 \<and> servKlife + Ts \<le> authKlife + Ta)" 775by (blast dest: servTicket_authentic_Tgs u_K4_imp_K2) 776 777lemma u_NotexpiredSK_NotexpiredAK: 778 "\<lbrakk> \<not> expiredSK Ts evs; servKlife + Ts \<le> authKlife + Ta \<rbrakk> 779 \<Longrightarrow> \<not> expiredAK Ta evs" 780 by (metis le_less_trans) 781 782 783subsection\<open>Reliability: friendly agents send something if something else happened\<close> 784 785lemma K3_imp_K2: 786 "\<lbrakk> Says A Tgs 787 \<lbrace>authTicket, Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B\<rbrace> 788 \<in> set evs; 789 A \<notin> bad; evs \<in> kerbIV \<rbrakk> 790 \<Longrightarrow> \<exists>Ta. Says Kas A (Crypt (shrK A) 791 \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>) 792 \<in> set evs" 793apply (erule rev_mp) 794apply (erule kerbIV.induct) 795apply (frule_tac [7] K5_msg_in_parts_spies) 796apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast, blast) 797apply (blast dest: Says_imp_spies [THEN parts.Inj, THEN authK_authentic]) 798done 799 800text\<open>Anticipated here from next subsection. An authK is encrypted by one and only one Shared key. A servK is encrypted by one and only one authK.\<close> 801lemma Key_unique_SesKey: 802 "\<lbrakk> Crypt K \<lbrace>Key SesKey, Agent B, T, Ticket\<rbrace> 803 \<in> parts (spies evs); 804 Crypt K' \<lbrace>Key SesKey, Agent B', T', Ticket'\<rbrace> 805 \<in> parts (spies evs); Key SesKey \<notin> analz (spies evs); 806 evs \<in> kerbIV \<rbrakk> 807 \<Longrightarrow> K=K' \<and> B=B' \<and> T=T' \<and> Ticket=Ticket'" 808apply (erule rev_mp) 809apply (erule rev_mp) 810apply (erule rev_mp) 811apply (erule kerbIV.induct, analz_mono_contra) 812apply (frule_tac [7] K5_msg_in_parts_spies) 813apply (frule_tac [5] K3_msg_in_parts_spies, simp_all) 814txt\<open>Fake, K2, K4\<close> 815apply (blast+) 816done 817 818lemma Tgs_authenticates_A: 819 "\<lbrakk> Crypt authK \<lbrace>Agent A, Number T2\<rbrace> \<in> parts (spies evs); 820 Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace> 821 \<in> parts (spies evs); 822 Key authK \<notin> analz (spies evs); A \<notin> bad; evs \<in> kerbIV \<rbrakk> 823 \<Longrightarrow> \<exists> B. Says A Tgs \<lbrace> 824 Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>, 825 Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B \<rbrace> \<in> set evs" 826apply (drule authTicket_authentic, assumption, rotate_tac 4) 827apply (erule rev_mp, erule rev_mp, erule rev_mp) 828apply (erule kerbIV.induct, analz_mono_contra) 829apply (frule_tac [5] Says_ticket_parts) 830apply (frule_tac [7] Says_ticket_parts) 831apply (simp_all (no_asm_simp) add: all_conj_distrib) 832txt\<open>Fake\<close> 833apply blast 834txt\<open>K2\<close> 835apply (force dest!: Crypt_imp_keysFor) 836txt\<open>K3\<close> 837apply (blast dest: Key_unique_SesKey) 838txt\<open>K5\<close> 839apply (metis K3_imp_K2 Key_unique_SesKey Spy_see_shrK parts.Body parts.Fst 840 Says_imp_knows_Spy [THEN parts.Inj]) 841done 842 843lemma Says_K5: 844 "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs); 845 Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, 846 servTicket\<rbrace>) \<in> set evs; 847 Key servK \<notin> analz (spies evs); 848 A \<notin> bad; B \<notin> bad; evs \<in> kerbIV \<rbrakk> 849 \<Longrightarrow> Says A B \<lbrace>servTicket, Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> \<in> set evs" 850apply (erule rev_mp) 851apply (erule rev_mp) 852apply (erule rev_mp) 853apply (erule kerbIV.induct, analz_mono_contra) 854apply (frule_tac [5] Says_ticket_parts) 855apply (frule_tac [7] Says_ticket_parts) 856apply (simp_all (no_asm_simp) add: all_conj_distrib) 857apply blast 858txt\<open>K3\<close> 859apply (blast dest: authK_authentic Says_Kas_message_form Says_Tgs_message_form) 860txt\<open>K4\<close> 861apply (force dest!: Crypt_imp_keysFor) 862txt\<open>K5\<close> 863apply (blast dest: Key_unique_SesKey) 864done 865 866text\<open>Anticipated here from next subsection\<close> 867lemma unique_CryptKey: 868 "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key SesKey, T\<rbrace> 869 \<in> parts (spies evs); 870 Crypt (shrK B') \<lbrace>Agent A', Agent B', Key SesKey, T'\<rbrace> 871 \<in> parts (spies evs); Key SesKey \<notin> analz (spies evs); 872 evs \<in> kerbIV \<rbrakk> 873 \<Longrightarrow> A=A' \<and> B=B' \<and> T=T'" 874apply (erule rev_mp) 875apply (erule rev_mp) 876apply (erule rev_mp) 877apply (erule kerbIV.induct, analz_mono_contra) 878apply (frule_tac [7] K5_msg_in_parts_spies) 879apply (frule_tac [5] K3_msg_in_parts_spies, simp_all) 880txt\<open>Fake, K2, K4\<close> 881apply (blast+) 882done 883 884lemma Says_K6: 885 "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs); 886 Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, 887 servTicket\<rbrace>) \<in> set evs; 888 Key servK \<notin> analz (spies evs); 889 A \<notin> bad; B \<notin> bad; evs \<in> kerbIV \<rbrakk> 890 \<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> set evs" 891apply (erule rev_mp) 892apply (erule rev_mp) 893apply (erule rev_mp) 894apply (erule kerbIV.induct, analz_mono_contra) 895apply (frule_tac [5] Says_ticket_parts) 896apply (frule_tac [7] Says_ticket_parts) 897apply (simp_all (no_asm_simp)) 898apply blast 899apply (metis Crypt_imp_invKey_keysFor invKey_K new_keys_not_used) 900apply (clarify) 901apply (frule Says_Tgs_message_form, assumption) 902apply (metis K3_msg_in_parts_spies parts.Fst Says_imp_knows_Spy [THEN parts.Inj] 903 unique_CryptKey) 904done 905 906text\<open>Needs a unicity theorem, hence moved here\<close> 907lemma servK_authentic_ter: 908 "\<lbrakk> Says Kas A 909 (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>) \<in> set evs; 910 Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace> 911 \<in> parts (spies evs); 912 Key authK \<notin> analz (spies evs); 913 evs \<in> kerbIV \<rbrakk> 914 \<Longrightarrow> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 915 \<in> set evs" 916apply (frule Says_Kas_message_form, assumption) 917apply (erule rev_mp) 918apply (erule rev_mp) 919apply (erule rev_mp) 920apply (erule kerbIV.induct, analz_mono_contra) 921apply (frule_tac [7] K5_msg_in_parts_spies) 922apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast) 923txt\<open>K2\<close> 924apply (blast dest!: servK_authentic Says_Tgs_message_form authKeys_used) 925txt\<open>K4 remain\<close> 926apply (blast dest!: unique_CryptKey) 927done 928 929 930subsection\<open>Unicity Theorems\<close> 931 932text\<open>The session key, if secure, uniquely identifies the Ticket 933 whether authTicket or servTicket. As a matter of fact, one can read 934 also Tgs in the place of B.\<close> 935 936 937(* 938 At reception of any message mentioning A, Kas associates shrK A with 939 a new authK. Realistic, as the user gets a new authK at each login. 940 Similarly, at reception of any message mentioning an authK 941 (a legitimate user could make several requests to Tgs - by K3), Tgs 942 associates it with a new servK. 943 944 Therefore, a goal like 945 946 "evs \<in> kerbIV 947 \<Longrightarrow> Key Kc \<notin> analz (spies evs) \<longrightarrow> 948 (\<exists>K' B' T' Ticket'. \<forall>K B T Ticket. 949 Crypt Kc \<lbrace>Key K, Agent B, T, Ticket\<rbrace> 950 \<in> parts (spies evs) \<longrightarrow> K=K' \<and> B=B' \<and> T=T' \<and> Ticket=Ticket')" 951 952 would fail on the K2 and K4 cases. 953*) 954 955lemma unique_authKeys: 956 "\<lbrakk> Says Kas A 957 (Crypt Ka \<lbrace>Key authK, Agent Tgs, Ta, X\<rbrace>) \<in> set evs; 958 Says Kas A' 959 (Crypt Ka' \<lbrace>Key authK, Agent Tgs, Ta', X'\<rbrace>) \<in> set evs; 960 evs \<in> kerbIV \<rbrakk> \<Longrightarrow> A=A' \<and> Ka=Ka' \<and> Ta=Ta' \<and> X=X'" 961apply (erule rev_mp) 962apply (erule rev_mp) 963apply (erule kerbIV.induct) 964apply (frule_tac [7] K5_msg_in_parts_spies) 965apply (frule_tac [5] K3_msg_in_parts_spies, simp_all) 966txt\<open>K2\<close> 967apply blast 968done 969 970text\<open>servK uniquely identifies the message from Tgs\<close> 971lemma unique_servKeys: 972 "\<lbrakk> Says Tgs A 973 (Crypt K \<lbrace>Key servK, Agent B, Ts, X\<rbrace>) \<in> set evs; 974 Says Tgs A' 975 (Crypt K' \<lbrace>Key servK, Agent B', Ts', X'\<rbrace>) \<in> set evs; 976 evs \<in> kerbIV \<rbrakk> \<Longrightarrow> A=A' \<and> B=B' \<and> K=K' \<and> Ts=Ts' \<and> X=X'" 977apply (erule rev_mp) 978apply (erule rev_mp) 979apply (erule kerbIV.induct) 980apply (frule_tac [7] K5_msg_in_parts_spies) 981apply (frule_tac [5] K3_msg_in_parts_spies, simp_all) 982txt\<open>K4\<close> 983apply blast 984done 985 986text\<open>Revised unicity theorems\<close> 987 988lemma Kas_Unique: 989 "\<lbrakk> Says Kas A 990 (Crypt Ka \<lbrace>Key authK, Agent Tgs, Ta, authTicket\<rbrace>) \<in> set evs; 991 evs \<in> kerbIV \<rbrakk> \<Longrightarrow> 992 Unique (Says Kas A (Crypt Ka \<lbrace>Key authK, Agent Tgs, Ta, authTicket\<rbrace>)) 993 on evs" 994apply (erule rev_mp, erule kerbIV.induct, simp_all add: Unique_def) 995apply blast 996done 997 998lemma Tgs_Unique: 999 "\<lbrakk> Says Tgs A 1000 (Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>) \<in> set evs; 1001 evs \<in> kerbIV \<rbrakk> \<Longrightarrow> 1002 Unique (Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>)) 1003 on evs" 1004apply (erule rev_mp, erule kerbIV.induct, simp_all add: Unique_def) 1005apply blast 1006done 1007 1008 1009subsection\<open>Lemmas About the Predicate @{term AKcryptSK}\<close> 1010 1011lemma not_AKcryptSK_Nil [iff]: "\<not> AKcryptSK authK servK []" 1012by (simp add: AKcryptSK_def) 1013 1014lemma AKcryptSKI: 1015 "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, X \<rbrace>) \<in> set evs; 1016 evs \<in> kerbIV \<rbrakk> \<Longrightarrow> AKcryptSK authK servK evs" 1017apply (unfold AKcryptSK_def) 1018apply (blast dest: Says_Tgs_message_form) 1019done 1020 1021lemma AKcryptSK_Says [simp]: 1022 "AKcryptSK authK servK (Says S A X # evs) = 1023 (Tgs = S \<and> 1024 (\<exists>B Ts. X = Crypt authK 1025 \<lbrace>Key servK, Agent B, Number Ts, 1026 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<rbrace>) 1027 | AKcryptSK authK servK evs)" 1028by (auto simp add: AKcryptSK_def) 1029 1030 1031(*A fresh authK cannot be associated with any other 1032 (with respect to a given trace). *) 1033lemma Auth_fresh_not_AKcryptSK: 1034 "\<lbrakk> Key authK \<notin> used evs; evs \<in> kerbIV \<rbrakk> 1035 \<Longrightarrow> \<not> AKcryptSK authK servK evs" 1036apply (unfold AKcryptSK_def) 1037apply (erule rev_mp) 1038apply (erule kerbIV.induct) 1039apply (frule_tac [7] K5_msg_in_parts_spies) 1040apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast) 1041done 1042 1043(*A fresh servK cannot be associated with any other 1044 (with respect to a given trace). *) 1045lemma Serv_fresh_not_AKcryptSK: 1046 "Key servK \<notin> used evs \<Longrightarrow> \<not> AKcryptSK authK servK evs" 1047by (unfold AKcryptSK_def, blast) 1048 1049lemma authK_not_AKcryptSK: 1050 "\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, tk\<rbrace> 1051 \<in> parts (spies evs); evs \<in> kerbIV \<rbrakk> 1052 \<Longrightarrow> \<not> AKcryptSK K authK evs" 1053apply (erule rev_mp) 1054apply (erule kerbIV.induct) 1055apply (frule_tac [7] K5_msg_in_parts_spies) 1056apply (frule_tac [5] K3_msg_in_parts_spies, simp_all) 1057txt\<open>Fake\<close> 1058apply blast 1059txt\<open>K2: by freshness\<close> 1060apply (simp add: AKcryptSK_def) 1061txt\<open>K4\<close> 1062apply (blast+) 1063done 1064 1065text\<open>A secure serverkey cannot have been used to encrypt others\<close> 1066lemma servK_not_AKcryptSK: 1067 "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key SK, Number Ts\<rbrace> \<in> parts (spies evs); 1068 Key SK \<notin> analz (spies evs); SK \<in> symKeys; 1069 B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk> 1070 \<Longrightarrow> \<not> AKcryptSK SK K evs" 1071apply (erule rev_mp) 1072apply (erule rev_mp) 1073apply (erule kerbIV.induct, analz_mono_contra) 1074apply (frule_tac [7] K5_msg_in_parts_spies) 1075apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast) 1076txt\<open>K4\<close> 1077apply (metis Auth_fresh_not_AKcryptSK Crypt_imp_keysFor new_keys_not_used parts.Fst parts.Snd Says_imp_knows_Spy [THEN parts.Inj] unique_CryptKey) 1078done 1079 1080text\<open>Long term keys are not issued as servKeys\<close> 1081lemma shrK_not_AKcryptSK: 1082 "evs \<in> kerbIV \<Longrightarrow> \<not> AKcryptSK K (shrK A) evs" 1083apply (unfold AKcryptSK_def) 1084apply (erule kerbIV.induct) 1085apply (frule_tac [7] K5_msg_in_parts_spies) 1086apply (frule_tac [5] K3_msg_in_parts_spies, auto) 1087done 1088 1089text\<open>The Tgs message associates servK with authK and therefore not with any 1090 other key authK.\<close> 1091lemma Says_Tgs_AKcryptSK: 1092 "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, X \<rbrace>) 1093 \<in> set evs; 1094 authK' \<noteq> authK; evs \<in> kerbIV \<rbrakk> 1095 \<Longrightarrow> \<not> AKcryptSK authK' servK evs" 1096apply (unfold AKcryptSK_def) 1097apply (blast dest: unique_servKeys) 1098done 1099 1100text\<open>Equivalently\<close> 1101lemma not_different_AKcryptSK: 1102 "\<lbrakk> AKcryptSK authK servK evs; 1103 authK' \<noteq> authK; evs \<in> kerbIV \<rbrakk> 1104 \<Longrightarrow> \<not> AKcryptSK authK' servK evs \<and> servK \<in> symKeys" 1105apply (simp add: AKcryptSK_def) 1106apply (blast dest: unique_servKeys Says_Tgs_message_form) 1107done 1108 1109lemma AKcryptSK_not_AKcryptSK: 1110 "\<lbrakk> AKcryptSK authK servK evs; evs \<in> kerbIV \<rbrakk> 1111 \<Longrightarrow> \<not> AKcryptSK servK K evs" 1112apply (erule rev_mp) 1113apply (erule kerbIV.induct) 1114apply (frule_tac [7] K5_msg_in_parts_spies) 1115apply (frule_tac [5] K3_msg_in_parts_spies, simp_all) 1116apply (metis Auth_fresh_not_AKcryptSK Says_imp_spies authK_not_AKcryptSK 1117 authKeys_used authTicket_crypt_authK parts.Fst parts.Inj) 1118done 1119 1120text\<open>The only session keys that can be found with the help of session keys are 1121 those sent by Tgs in step K4.\<close> 1122 1123text\<open>We take some pains to express the property 1124 as a logical equivalence so that the simplifier can apply it.\<close> 1125lemma Key_analz_image_Key_lemma: 1126 "P \<longrightarrow> (Key K \<in> analz (Key`KK \<union> H)) \<longrightarrow> (K\<in>KK | Key K \<in> analz H) 1127 \<Longrightarrow> 1128 P \<longrightarrow> (Key K \<in> analz (Key`KK \<union> H)) = (K\<in>KK | Key K \<in> analz H)" 1129by (blast intro: analz_mono [THEN subsetD]) 1130 1131 1132lemma AKcryptSK_analz_insert: 1133 "\<lbrakk> AKcryptSK K K' evs; K \<in> symKeys; evs \<in> kerbIV \<rbrakk> 1134 \<Longrightarrow> Key K' \<in> analz (insert (Key K) (spies evs))" 1135apply (simp add: AKcryptSK_def, clarify) 1136apply (drule Says_imp_spies [THEN analz.Inj, THEN analz_insertI], auto) 1137done 1138 1139lemma authKeys_are_not_AKcryptSK: 1140 "\<lbrakk> K \<in> authKeys evs \<union> range shrK; evs \<in> kerbIV \<rbrakk> 1141 \<Longrightarrow> \<forall>SK. \<not> AKcryptSK SK K evs \<and> K \<in> symKeys" 1142apply (simp add: authKeys_def AKcryptSK_def) 1143apply (blast dest: Says_Kas_message_form Says_Tgs_message_form) 1144done 1145 1146lemma not_authKeys_not_AKcryptSK: 1147 "\<lbrakk> K \<notin> authKeys evs; 1148 K \<notin> range shrK; evs \<in> kerbIV \<rbrakk> 1149 \<Longrightarrow> \<forall>SK. \<not> AKcryptSK K SK evs" 1150apply (simp add: AKcryptSK_def) 1151apply (blast dest: Says_Tgs_message_form) 1152done 1153 1154 1155subsection\<open>Secrecy Theorems\<close> 1156 1157text\<open>For the Oops2 case of the next theorem\<close> 1158lemma Oops2_not_AKcryptSK: 1159 "\<lbrakk> evs \<in> kerbIV; 1160 Says Tgs A (Crypt authK 1161 \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 1162 \<in> set evs \<rbrakk> 1163 \<Longrightarrow> \<not> AKcryptSK servK SK evs" 1164by (blast dest: AKcryptSKI AKcryptSK_not_AKcryptSK) 1165 1166text\<open>Big simplification law for keys SK that are not crypted by keys in KK 1167 It helps prove three, otherwise hard, facts about keys. These facts are 1168 exploited as simplification laws for analz, and also "limit the damage" 1169 in case of loss of a key to the spy. See ESORICS98. 1170 [simplified by LCP]\<close> 1171lemma Key_analz_image_Key [rule_format (no_asm)]: 1172 "evs \<in> kerbIV \<Longrightarrow> 1173 (\<forall>SK KK. SK \<in> symKeys \<and> KK \<subseteq> -(range shrK) \<longrightarrow> 1174 (\<forall>K \<in> KK. \<not> AKcryptSK K SK evs) \<longrightarrow> 1175 (Key SK \<in> analz (Key`KK \<union> (spies evs))) = 1176 (SK \<in> KK | Key SK \<in> analz (spies evs)))" 1177apply (erule kerbIV.induct) 1178apply (frule_tac [10] Oops_range_spies2) 1179apply (frule_tac [9] Oops_range_spies1) 1180apply (frule_tac [7] Says_tgs_message_form) 1181apply (frule_tac [5] Says_kas_message_form) 1182apply (safe del: impI intro!: Key_analz_image_Key_lemma [THEN impI]) 1183txt\<open>Case-splits for Oops1 and message 5: the negated case simplifies using 1184 the induction hypothesis\<close> 1185apply (case_tac [11] "AKcryptSK authK SK evsO1") 1186apply (case_tac [8] "AKcryptSK servK SK evs5") 1187apply (simp_all del: image_insert 1188 add: analz_image_freshK_simps AKcryptSK_Says shrK_not_AKcryptSK 1189 Oops2_not_AKcryptSK Auth_fresh_not_AKcryptSK 1190 Serv_fresh_not_AKcryptSK Says_Tgs_AKcryptSK Spy_analz_shrK) 1191txt\<open>Fake\<close> 1192apply spy_analz 1193txt\<open>K2\<close> 1194apply blast 1195txt\<open>K3\<close> 1196apply blast 1197txt\<open>K4\<close> 1198apply (blast dest!: authK_not_AKcryptSK) 1199txt\<open>K5\<close> 1200apply (case_tac "Key servK \<in> analz (spies evs5) ") 1201txt\<open>If servK is compromised then the result follows directly...\<close> 1202apply (simp (no_asm_simp) add: analz_insert_eq Un_upper2 [THEN analz_mono, THEN subsetD]) 1203txt\<open>...therefore servK is uncompromised.\<close> 1204txt\<open>The AKcryptSK servK SK evs5 case leads to a contradiction.\<close> 1205apply (blast elim!: servK_not_AKcryptSK [THEN [2] rev_notE] del: allE ballE) 1206txt\<open>Another K5 case\<close> 1207apply blast 1208txt\<open>Oops1\<close> 1209apply simp 1210apply (blast dest!: AKcryptSK_analz_insert) 1211done 1212 1213text\<open>First simplification law for analz: no session keys encrypt 1214authentication keys or shared keys.\<close> 1215lemma analz_insert_freshK1: 1216 "\<lbrakk> evs \<in> kerbIV; K \<in> authKeys evs \<union> range shrK; 1217 SesKey \<notin> range shrK \<rbrakk> 1218 \<Longrightarrow> (Key K \<in> analz (insert (Key SesKey) (spies evs))) = 1219 (K = SesKey | Key K \<in> analz (spies evs))" 1220apply (frule authKeys_are_not_AKcryptSK, assumption) 1221apply (simp del: image_insert 1222 add: analz_image_freshK_simps add: Key_analz_image_Key) 1223done 1224 1225 1226text\<open>Second simplification law for analz: no service keys encrypt any other keys.\<close> 1227lemma analz_insert_freshK2: 1228 "\<lbrakk> evs \<in> kerbIV; servK \<notin> (authKeys evs); servK \<notin> range shrK; 1229 K \<in> symKeys \<rbrakk> 1230 \<Longrightarrow> (Key K \<in> analz (insert (Key servK) (spies evs))) = 1231 (K = servK | Key K \<in> analz (spies evs))" 1232apply (frule not_authKeys_not_AKcryptSK, assumption, assumption) 1233apply (simp del: image_insert 1234 add: analz_image_freshK_simps add: Key_analz_image_Key) 1235done 1236 1237 1238text\<open>Third simplification law for analz: only one authentication key encrypts a certain service key.\<close> 1239 1240lemma analz_insert_freshK3: 1241 "\<lbrakk> AKcryptSK authK servK evs; 1242 authK' \<noteq> authK; authK' \<notin> range shrK; evs \<in> kerbIV \<rbrakk> 1243 \<Longrightarrow> (Key servK \<in> analz (insert (Key authK') (spies evs))) = 1244 (servK = authK' | Key servK \<in> analz (spies evs))" 1245apply (drule_tac authK' = authK' in not_different_AKcryptSK, blast, assumption) 1246apply (simp del: image_insert 1247 add: analz_image_freshK_simps add: Key_analz_image_Key) 1248done 1249 1250lemma analz_insert_freshK3_bis: 1251 "\<lbrakk> Says Tgs A 1252 (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 1253 \<in> set evs; 1254 authK \<noteq> authK'; authK' \<notin> range shrK; evs \<in> kerbIV \<rbrakk> 1255 \<Longrightarrow> (Key servK \<in> analz (insert (Key authK') (spies evs))) = 1256 (servK = authK' | Key servK \<in> analz (spies evs))" 1257apply (frule AKcryptSKI, assumption) 1258apply (simp add: analz_insert_freshK3) 1259done 1260 1261text\<open>a weakness of the protocol\<close> 1262lemma authK_compromises_servK: 1263 "\<lbrakk> Says Tgs A 1264 (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 1265 \<in> set evs; authK \<in> symKeys; 1266 Key authK \<in> analz (spies evs); evs \<in> kerbIV \<rbrakk> 1267 \<Longrightarrow> Key servK \<in> analz (spies evs)" 1268 by (metis Says_imp_analz_Spy analz.Fst analz_Decrypt') 1269 1270lemma servK_notin_authKeysD: 1271 "\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Ts, 1272 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace>\<rbrace> 1273 \<in> parts (spies evs); 1274 Key servK \<notin> analz (spies evs); 1275 B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk> 1276 \<Longrightarrow> servK \<notin> authKeys evs" 1277apply (erule rev_mp) 1278apply (erule rev_mp) 1279apply (simp add: authKeys_def) 1280apply (erule kerbIV.induct, analz_mono_contra) 1281apply (frule_tac [7] K5_msg_in_parts_spies) 1282apply (frule_tac [5] K3_msg_in_parts_spies, simp_all) 1283apply (blast+) 1284done 1285 1286 1287text\<open>If Spy sees the Authentication Key sent in msg K2, then 1288 the Key has expired.\<close> 1289lemma Confidentiality_Kas_lemma [rule_format]: 1290 "\<lbrakk> authK \<in> symKeys; A \<notin> bad; evs \<in> kerbIV \<rbrakk> 1291 \<Longrightarrow> Says Kas A 1292 (Crypt (shrK A) 1293 \<lbrace>Key authK, Agent Tgs, Number Ta, 1294 Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>) 1295 \<in> set evs \<longrightarrow> 1296 Key authK \<in> analz (spies evs) \<longrightarrow> 1297 expiredAK Ta evs" 1298apply (erule kerbIV.induct) 1299apply (frule_tac [10] Oops_range_spies2) 1300apply (frule_tac [9] Oops_range_spies1) 1301apply (frule_tac [7] Says_tgs_message_form) 1302apply (frule_tac [5] Says_kas_message_form) 1303apply (safe del: impI conjI impCE) 1304apply (simp_all (no_asm_simp) add: Says_Kas_message_form less_SucI analz_insert_eq not_parts_not_analz analz_insert_freshK1 pushes) 1305txt\<open>Fake\<close> 1306apply spy_analz 1307txt\<open>K2\<close> 1308apply blast 1309txt\<open>K4\<close> 1310apply blast 1311txt\<open>Level 8: K5\<close> 1312apply (blast dest: servK_notin_authKeysD Says_Kas_message_form intro: less_SucI) 1313txt\<open>Oops1\<close> 1314apply (blast dest!: unique_authKeys intro: less_SucI) 1315txt\<open>Oops2\<close> 1316apply (blast dest: Says_Tgs_message_form Says_Kas_message_form) 1317done 1318 1319lemma Confidentiality_Kas: 1320 "\<lbrakk> Says Kas A 1321 (Crypt Ka \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>) 1322 \<in> set evs; 1323 \<not> expiredAK Ta evs; 1324 A \<notin> bad; evs \<in> kerbIV \<rbrakk> 1325 \<Longrightarrow> Key authK \<notin> analz (spies evs)" 1326by (blast dest: Says_Kas_message_form Confidentiality_Kas_lemma) 1327 1328text\<open>If Spy sees the Service Key sent in msg K4, then 1329 the Key has expired.\<close> 1330 1331lemma Confidentiality_lemma [rule_format]: 1332 "\<lbrakk> Says Tgs A 1333 (Crypt authK 1334 \<lbrace>Key servK, Agent B, Number Ts, 1335 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>) 1336 \<in> set evs; 1337 Key authK \<notin> analz (spies evs); 1338 servK \<in> symKeys; 1339 A \<notin> bad; B \<notin> bad; evs \<in> kerbIV \<rbrakk> 1340 \<Longrightarrow> Key servK \<in> analz (spies evs) \<longrightarrow> 1341 expiredSK Ts evs" 1342apply (erule rev_mp) 1343apply (erule rev_mp) 1344apply (erule kerbIV.induct) 1345apply (rule_tac [9] impI)+ 1346 \<comment> \<open>The Oops1 case is unusual: must simplify 1347 @{term "Authkey \<notin> analz (spies (ev#evs))"}, not letting 1348 \<open>analz_mono_contra\<close> weaken it to 1349 @{term "Authkey \<notin> analz (spies evs)"}, 1350 for we then conclude @{term "authK \<noteq> authKa"}.\<close> 1351apply analz_mono_contra 1352apply (frule_tac [10] Oops_range_spies2) 1353apply (frule_tac [9] Oops_range_spies1) 1354apply (frule_tac [7] Says_tgs_message_form) 1355apply (frule_tac [5] Says_kas_message_form) 1356apply (safe del: impI conjI impCE) 1357apply (simp_all add: less_SucI new_keys_not_analzd Says_Kas_message_form Says_Tgs_message_form analz_insert_eq not_parts_not_analz analz_insert_freshK1 analz_insert_freshK2 analz_insert_freshK3_bis pushes) 1358txt\<open>Fake\<close> 1359 apply spy_analz 1360txt\<open>K2\<close> 1361 apply (blast intro: parts_insertI less_SucI) 1362txt\<open>K4\<close> 1363 apply (blast dest: authTicket_authentic Confidentiality_Kas) 1364txt\<open>K5\<close> 1365 apply (metis Says_imp_spies Says_ticket_parts Tgs_not_bad analz_insert_freshK2 1366 less_SucI parts.Inj servK_notin_authKeysD unique_CryptKey) 1367txt\<open>Oops1\<close> 1368 apply (blast dest: Says_Kas_message_form Says_Tgs_message_form intro: less_SucI) 1369txt\<open>Oops2\<close> 1370apply (blast dest: Says_imp_spies [THEN parts.Inj] Key_unique_SesKey intro: less_SucI) 1371done 1372 1373 1374text\<open>In the real world Tgs can't check wheter authK is secure!\<close> 1375lemma Confidentiality_Tgs: 1376 "\<lbrakk> Says Tgs A 1377 (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 1378 \<in> set evs; 1379 Key authK \<notin> analz (spies evs); 1380 \<not> expiredSK Ts evs; 1381 A \<notin> bad; B \<notin> bad; evs \<in> kerbIV \<rbrakk> 1382 \<Longrightarrow> Key servK \<notin> analz (spies evs)" 1383by (blast dest: Says_Tgs_message_form Confidentiality_lemma) 1384 1385text\<open>In the real world Tgs CAN check what Kas sends!\<close> 1386lemma Confidentiality_Tgs_bis: 1387 "\<lbrakk> Says Kas A 1388 (Crypt Ka \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>) 1389 \<in> set evs; 1390 Says Tgs A 1391 (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 1392 \<in> set evs; 1393 \<not> expiredAK Ta evs; \<not> expiredSK Ts evs; 1394 A \<notin> bad; B \<notin> bad; evs \<in> kerbIV \<rbrakk> 1395 \<Longrightarrow> Key servK \<notin> analz (spies evs)" 1396by (blast dest!: Confidentiality_Kas Confidentiality_Tgs) 1397 1398text\<open>Most general form\<close> 1399lemmas Confidentiality_Tgs_ter = authTicket_authentic [THEN Confidentiality_Tgs_bis] 1400 1401lemmas Confidentiality_Auth_A = authK_authentic [THEN Confidentiality_Kas] 1402 1403text\<open>Needs a confidentiality guarantee, hence moved here. 1404 Authenticity of servK for A\<close> 1405lemma servK_authentic_bis_r: 1406 "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace> 1407 \<in> parts (spies evs); 1408 Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace> 1409 \<in> parts (spies evs); 1410 \<not> expiredAK Ta evs; A \<notin> bad; evs \<in> kerbIV \<rbrakk> 1411 \<Longrightarrow>Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 1412 \<in> set evs" 1413by (blast dest: authK_authentic Confidentiality_Auth_A servK_authentic_ter) 1414 1415lemma Confidentiality_Serv_A: 1416 "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace> 1417 \<in> parts (spies evs); 1418 Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace> 1419 \<in> parts (spies evs); 1420 \<not> expiredAK Ta evs; \<not> expiredSK Ts evs; 1421 A \<notin> bad; B \<notin> bad; evs \<in> kerbIV \<rbrakk> 1422 \<Longrightarrow> Key servK \<notin> analz (spies evs)" 1423apply (drule authK_authentic, assumption, assumption) 1424apply (blast dest: Confidentiality_Kas Says_Kas_message_form servK_authentic_ter Confidentiality_Tgs_bis) 1425done 1426 1427lemma Confidentiality_B: 1428 "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> 1429 \<in> parts (spies evs); 1430 Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace> 1431 \<in> parts (spies evs); 1432 Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace> 1433 \<in> parts (spies evs); 1434 \<not> expiredSK Ts evs; \<not> expiredAK Ta evs; 1435 A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk> 1436 \<Longrightarrow> Key servK \<notin> analz (spies evs)" 1437apply (frule authK_authentic) 1438apply (frule_tac [3] Confidentiality_Kas) 1439apply (frule_tac [6] servTicket_authentic, auto) 1440apply (blast dest!: Confidentiality_Tgs_bis dest: Says_Kas_message_form servK_authentic unique_servKeys unique_authKeys) 1441done 1442(* 1443The proof above is fast. It can be done in one command in 17 secs: 1444apply (blast dest: authK_authentic servK_authentic 1445 Says_Kas_message_form servTicket_authentic 1446 unique_servKeys unique_authKeys 1447 Confidentiality_Kas 1448 Confidentiality_Tgs_bis) 1449It is very brittle: we can't use this command partway 1450through the script above. 1451*) 1452 1453lemma u_Confidentiality_B: 1454 "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> 1455 \<in> parts (spies evs); 1456 \<not> expiredSK Ts evs; 1457 A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk> 1458 \<Longrightarrow> Key servK \<notin> analz (spies evs)" 1459by (blast dest: u_servTicket_authentic u_NotexpiredSK_NotexpiredAK Confidentiality_Tgs_bis) 1460 1461 1462 1463subsection\<open>Parties authentication: each party verifies "the identity of 1464 another party who generated some data" (quoted from Neuman and Ts'o).\<close> 1465 1466text\<open>These guarantees don't assess whether two parties agree on 1467 the same session key: sending a message containing a key 1468 doesn't a priori state knowledge of the key.\<close> 1469 1470 1471text\<open>\<open>Tgs_authenticates_A\<close> can be found above\<close> 1472 1473lemma A_authenticates_Tgs: 1474 "\<lbrakk> Says Kas A 1475 (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>) \<in> set evs; 1476 Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace> 1477 \<in> parts (spies evs); 1478 Key authK \<notin> analz (spies evs); 1479 evs \<in> kerbIV \<rbrakk> 1480 \<Longrightarrow> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 1481 \<in> set evs" 1482apply (frule Says_Kas_message_form, assumption) 1483apply (erule rev_mp) 1484apply (erule rev_mp) 1485apply (erule rev_mp) 1486apply (erule kerbIV.induct, analz_mono_contra) 1487apply (frule_tac [7] K5_msg_in_parts_spies) 1488apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast) 1489txt\<open>K2\<close> 1490apply (blast dest!: servK_authentic Says_Tgs_message_form authKeys_used) 1491txt\<open>K4\<close> 1492apply (blast dest!: unique_CryptKey) 1493done 1494 1495 1496lemma B_authenticates_A: 1497 "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs); 1498 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> 1499 \<in> parts (spies evs); 1500 Key servK \<notin> analz (spies evs); 1501 A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk> 1502 \<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>, 1503 Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> \<in> set evs" 1504by (blast dest: servTicket_authentic_Tgs intro: Says_K5) 1505 1506text\<open>The second assumption tells B what kind of key servK is.\<close> 1507lemma B_authenticates_A_r: 1508 "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs); 1509 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> 1510 \<in> parts (spies evs); 1511 Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace> 1512 \<in> parts (spies evs); 1513 Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace> 1514 \<in> parts (spies evs); 1515 \<not> expiredSK Ts evs; \<not> expiredAK Ta evs; 1516 B \<noteq> Tgs; A \<notin> bad; B \<notin> bad; evs \<in> kerbIV \<rbrakk> 1517 \<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>, 1518 Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<rbrace> \<in> set evs" 1519by (blast intro: Says_K5 dest: Confidentiality_B servTicket_authentic_Tgs) 1520 1521text\<open>\<open>u_B_authenticates_A\<close> would be the same as \<open>B_authenticates_A\<close> because the servK confidentiality assumption is yet unrelaxed\<close> 1522 1523lemma u_B_authenticates_A_r: 1524 "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs); 1525 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> 1526 \<in> parts (spies evs); 1527 \<not> expiredSK Ts evs; 1528 B \<noteq> Tgs; A \<notin> bad; B \<notin> bad; evs \<in> kerbIV \<rbrakk> 1529 \<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>, 1530 Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<rbrace> \<in> set evs" 1531by (blast intro: Says_K5 dest: u_Confidentiality_B servTicket_authentic_Tgs) 1532 1533lemma A_authenticates_B: 1534 "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs); 1535 Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace> 1536 \<in> parts (spies evs); 1537 Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace> 1538 \<in> parts (spies evs); 1539 Key authK \<notin> analz (spies evs); Key servK \<notin> analz (spies evs); 1540 A \<notin> bad; B \<notin> bad; evs \<in> kerbIV \<rbrakk> 1541 \<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> set evs" 1542by (blast dest: authK_authentic servK_authentic Says_Kas_message_form Key_unique_SesKey K4_imp_K2 intro: Says_K6) 1543 1544lemma A_authenticates_B_r: 1545 "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs); 1546 Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace> 1547 \<in> parts (spies evs); 1548 Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace> 1549 \<in> parts (spies evs); 1550 \<not> expiredAK Ta evs; \<not> expiredSK Ts evs; 1551 A \<notin> bad; B \<notin> bad; evs \<in> kerbIV \<rbrakk> 1552 \<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> set evs" 1553apply (frule authK_authentic) 1554apply (frule_tac [3] Says_Kas_message_form) 1555apply (frule_tac [4] Confidentiality_Kas) 1556apply (frule_tac [7] servK_authentic) 1557prefer 8 apply blast 1558apply (erule_tac [9] exE) 1559apply (frule_tac [9] K4_imp_K2) 1560apply assumption+ 1561apply (blast dest: Key_unique_SesKey intro!: Says_K6 dest: Confidentiality_Tgs 1562) 1563done 1564 1565 1566subsection\<open>Key distribution guarantees 1567 An agent knows a session key if he used it to issue a cipher. 1568 These guarantees also convey a stronger form of 1569 authentication - non-injective agreement on the session key\<close> 1570 1571 1572lemma Kas_Issues_A: 1573 "\<lbrakk> Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>) \<in> set evs; 1574 evs \<in> kerbIV \<rbrakk> 1575 \<Longrightarrow> Kas Issues A with (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>) 1576 on evs" 1577apply (simp (no_asm) add: Issues_def) 1578apply (rule exI) 1579apply (rule conjI, assumption) 1580apply (simp (no_asm)) 1581apply (erule rev_mp) 1582apply (erule kerbIV.induct) 1583apply (frule_tac [5] Says_ticket_parts) 1584apply (frule_tac [7] Says_ticket_parts) 1585apply (simp_all (no_asm_simp) add: all_conj_distrib) 1586txt\<open>K2\<close> 1587apply (simp add: takeWhile_tail) 1588apply (blast dest: authK_authentic parts_spies_takeWhile_mono [THEN subsetD] parts_spies_evs_revD2 [THEN subsetD]) 1589done 1590 1591lemma A_authenticates_and_keydist_to_Kas: 1592 "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace> \<in> parts (spies evs); 1593 A \<notin> bad; evs \<in> kerbIV \<rbrakk> 1594 \<Longrightarrow> Kas Issues A with (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>) 1595 on evs" 1596by (blast dest: authK_authentic Kas_Issues_A) 1597 1598lemma honest_never_says_newer_timestamp_in_auth: 1599 "\<lbrakk> (CT evs) \<le> T; A \<notin> bad; Number T \<in> parts {X}; evs \<in> kerbIV \<rbrakk> 1600 \<Longrightarrow> \<forall> B Y. Says A B \<lbrace>Y, X\<rbrace> \<notin> set evs" 1601apply (erule rev_mp) 1602apply (erule kerbIV.induct) 1603apply force+ 1604done 1605 1606lemma honest_never_says_current_timestamp_in_auth: 1607 "\<lbrakk> (CT evs) = T; Number T \<in> parts {X}; evs \<in> kerbIV \<rbrakk> 1608 \<Longrightarrow> \<forall> A B Y. A \<notin> bad \<longrightarrow> Says A B \<lbrace>Y, X\<rbrace> \<notin> set evs" 1609 by (metis eq_imp_le honest_never_says_newer_timestamp_in_auth) 1610 1611lemma A_trusts_secure_authenticator: 1612 "\<lbrakk> Crypt K \<lbrace>Agent A, Number T\<rbrace> \<in> parts (spies evs); 1613 Key K \<notin> analz (spies evs); evs \<in> kerbIV \<rbrakk> 1614\<Longrightarrow> \<exists> B X. Says A Tgs \<lbrace>X, Crypt K \<lbrace>Agent A, Number T\<rbrace>, Agent B\<rbrace> \<in> set evs \<or> 1615 Says A B \<lbrace>X, Crypt K \<lbrace>Agent A, Number T\<rbrace>\<rbrace> \<in> set evs" 1616apply (erule rev_mp) 1617apply (erule rev_mp) 1618apply (erule kerbIV.induct, analz_mono_contra) 1619apply (frule_tac [5] Says_ticket_parts) 1620apply (frule_tac [7] Says_ticket_parts) 1621apply (simp_all add: all_conj_distrib) 1622apply blast+ 1623done 1624 1625lemma A_Issues_Tgs: 1626 "\<lbrakk> Says A Tgs \<lbrace>authTicket, Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B\<rbrace> 1627 \<in> set evs; 1628 Key authK \<notin> analz (spies evs); 1629 A \<notin> bad; evs \<in> kerbIV \<rbrakk> 1630 \<Longrightarrow> A Issues Tgs with (Crypt authK \<lbrace>Agent A, Number T2\<rbrace>) on evs" 1631apply (simp (no_asm) add: Issues_def) 1632apply (rule exI) 1633apply (rule conjI, assumption) 1634apply (simp (no_asm)) 1635apply (erule rev_mp) 1636apply (erule rev_mp) 1637apply (erule kerbIV.induct, analz_mono_contra) 1638apply (frule_tac [5] Says_ticket_parts) 1639apply (frule_tac [7] Says_ticket_parts) 1640apply (simp_all (no_asm_simp) add: all_conj_distrib) 1641txt\<open>fake\<close> 1642apply blast 1643txt\<open>K3\<close> 1644(* 1645apply clarify 1646apply (drule Says_imp_knows_Spy [THEN parts.Inj, THEN authK_authentic, THEN Says_Kas_message_form], assumption, assumption, assumption) 1647*) 1648apply (simp add: takeWhile_tail) 1649apply auto 1650apply (force dest!: authK_authentic Says_Kas_message_form) 1651apply (drule parts_spies_takeWhile_mono [THEN subsetD, THEN parts_spies_evs_revD2 [THEN subsetD]]) 1652apply (drule A_trusts_secure_authenticator, assumption, assumption) 1653apply (simp add: honest_never_says_current_timestamp_in_auth) 1654done 1655 1656lemma Tgs_authenticates_and_keydist_to_A: 1657 "\<lbrakk> Crypt authK \<lbrace>Agent A, Number T2\<rbrace> \<in> parts (spies evs); 1658 Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace> 1659 \<in> parts (spies evs); 1660 Key authK \<notin> analz (spies evs); 1661 A \<notin> bad; evs \<in> kerbIV \<rbrakk> 1662 \<Longrightarrow> A Issues Tgs with (Crypt authK \<lbrace>Agent A, Number T2\<rbrace>) on evs" 1663by (blast dest: A_Issues_Tgs Tgs_authenticates_A) 1664 1665lemma Tgs_Issues_A: 1666 "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket \<rbrace>) 1667 \<in> set evs; 1668 Key authK \<notin> analz (spies evs); evs \<in> kerbIV \<rbrakk> 1669 \<Longrightarrow> Tgs Issues A with 1670 (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket \<rbrace>) on evs" 1671apply (simp (no_asm) add: Issues_def) 1672apply (rule exI) 1673apply (rule conjI, assumption) 1674apply (simp (no_asm)) 1675apply (erule rev_mp) 1676apply (erule rev_mp) 1677apply (erule kerbIV.induct, analz_mono_contra) 1678apply (frule_tac [5] Says_ticket_parts) 1679apply (frule_tac [7] Says_ticket_parts) 1680apply (simp_all (no_asm_simp) add: all_conj_distrib) 1681txt\<open>K4\<close> 1682apply (simp add: takeWhile_tail) 1683(*Last two thms installed only to derive authK \<notin> range shrK*) 1684apply (metis knows_Spy_partsEs(2) parts.Fst usedI used_evs_rev used_takeWhile_used) 1685done 1686 1687lemma A_authenticates_and_keydist_to_Tgs: 1688"\<lbrakk>Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace> \<in> parts (spies evs); 1689 Key authK \<notin> analz (spies evs); B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk> 1690 \<Longrightarrow> \<exists>A. Tgs Issues A with 1691 (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket \<rbrace>) on evs" 1692by (blast dest: Tgs_Issues_A servK_authentic_bis) 1693 1694 1695 1696lemma B_Issues_A: 1697 "\<lbrakk> Says B A (Crypt servK (Number T3)) \<in> set evs; 1698 Key servK \<notin> analz (spies evs); 1699 A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk> 1700 \<Longrightarrow> B Issues A with (Crypt servK (Number T3)) on evs" 1701apply (simp (no_asm) add: Issues_def) 1702apply (rule exI) 1703apply (rule conjI, assumption) 1704apply (simp (no_asm)) 1705apply (erule rev_mp) 1706apply (erule rev_mp) 1707apply (erule kerbIV.induct, analz_mono_contra) 1708apply (frule_tac [5] Says_ticket_parts) 1709apply (frule_tac [7] Says_ticket_parts) 1710apply (simp_all (no_asm_simp) add: all_conj_distrib) 1711apply blast 1712txt\<open>K6 requires numerous lemmas\<close> 1713apply (simp add: takeWhile_tail) 1714apply (blast dest: servTicket_authentic parts_spies_takeWhile_mono [THEN subsetD] parts_spies_evs_revD2 [THEN subsetD] intro: Says_K6) 1715done 1716 1717lemma B_Issues_A_r: 1718 "\<lbrakk> Says B A (Crypt servK (Number T3)) \<in> set evs; 1719 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> 1720 \<in> parts (spies evs); 1721 Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace> 1722 \<in> parts (spies evs); 1723 Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace> 1724 \<in> parts (spies evs); 1725 \<not> expiredSK Ts evs; \<not> expiredAK Ta evs; 1726 A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk> 1727 \<Longrightarrow> B Issues A with (Crypt servK (Number T3)) on evs" 1728by (blast dest!: Confidentiality_B B_Issues_A) 1729 1730lemma u_B_Issues_A_r: 1731 "\<lbrakk> Says B A (Crypt servK (Number T3)) \<in> set evs; 1732 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> 1733 \<in> parts (spies evs); 1734 \<not> expiredSK Ts evs; 1735 A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk> 1736 \<Longrightarrow> B Issues A with (Crypt servK (Number T3)) on evs" 1737by (blast dest!: u_Confidentiality_B B_Issues_A) 1738 1739lemma A_authenticates_and_keydist_to_B: 1740 "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs); 1741 Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace> 1742 \<in> parts (spies evs); 1743 Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace> 1744 \<in> parts (spies evs); 1745 Key authK \<notin> analz (spies evs); Key servK \<notin> analz (spies evs); 1746 A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk> 1747 \<Longrightarrow> B Issues A with (Crypt servK (Number T3)) on evs" 1748by (blast dest!: A_authenticates_B B_Issues_A) 1749 1750lemma A_authenticates_and_keydist_to_B_r: 1751 "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs); 1752 Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace> 1753 \<in> parts (spies evs); 1754 Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace> 1755 \<in> parts (spies evs); 1756 \<not> expiredAK Ta evs; \<not> expiredSK Ts evs; 1757 A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk> 1758 \<Longrightarrow> B Issues A with (Crypt servK (Number T3)) on evs" 1759by (blast dest!: A_authenticates_B_r Confidentiality_Serv_A B_Issues_A) 1760 1761 1762lemma A_Issues_B: 1763 "\<lbrakk> Says A B \<lbrace>servTicket, Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> 1764 \<in> set evs; 1765 Key servK \<notin> analz (spies evs); 1766 B \<noteq> Tgs; A \<notin> bad; B \<notin> bad; evs \<in> kerbIV \<rbrakk> 1767 \<Longrightarrow> A Issues B with (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>) on evs" 1768apply (simp (no_asm) add: Issues_def) 1769apply (rule exI) 1770apply (rule conjI, assumption) 1771apply (simp (no_asm)) 1772apply (erule rev_mp) 1773apply (erule rev_mp) 1774apply (erule kerbIV.induct, analz_mono_contra) 1775apply (frule_tac [5] Says_ticket_parts) 1776apply (frule_tac [7] Says_ticket_parts) 1777apply (simp_all (no_asm_simp)) 1778apply clarify 1779txt\<open>K5\<close> 1780apply auto 1781apply (simp add: takeWhile_tail) 1782txt\<open>Level 15: case analysis necessary because the assumption doesn't state 1783 the form of servTicket. The guarantee becomes stronger.\<close> 1784apply (blast dest: Says_imp_spies [THEN analz.Inj, THEN analz_Decrypt'] 1785 K3_imp_K2 servK_authentic_ter 1786 parts_spies_takeWhile_mono [THEN subsetD] 1787 parts_spies_evs_revD2 [THEN subsetD] 1788 intro: Says_K5) 1789apply (simp add: takeWhile_tail) 1790done 1791 1792lemma A_Issues_B_r: 1793 "\<lbrakk> Says A B \<lbrace>servTicket, Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> 1794 \<in> set evs; 1795 Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace> 1796 \<in> parts (spies evs); 1797 Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace> 1798 \<in> parts (spies evs); 1799 \<not> expiredAK Ta evs; \<not> expiredSK Ts evs; 1800 B \<noteq> Tgs; A \<notin> bad; B \<notin> bad; evs \<in> kerbIV \<rbrakk> 1801 \<Longrightarrow> A Issues B with (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>) on evs" 1802by (blast dest!: Confidentiality_Serv_A A_Issues_B) 1803 1804lemma B_authenticates_and_keydist_to_A: 1805 "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs); 1806 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> 1807 \<in> parts (spies evs); 1808 Key servK \<notin> analz (spies evs); 1809 B \<noteq> Tgs; A \<notin> bad; B \<notin> bad; evs \<in> kerbIV \<rbrakk> 1810 \<Longrightarrow> A Issues B with (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>) on evs" 1811by (blast dest: B_authenticates_A A_Issues_B) 1812 1813lemma B_authenticates_and_keydist_to_A_r: 1814 "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs); 1815 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> 1816 \<in> parts (spies evs); 1817 Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace> 1818 \<in> parts (spies evs); 1819 Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace> 1820 \<in> parts (spies evs); 1821 \<not> expiredSK Ts evs; \<not> expiredAK Ta evs; 1822 B \<noteq> Tgs; A \<notin> bad; B \<notin> bad; evs \<in> kerbIV \<rbrakk> 1823 \<Longrightarrow> A Issues B with (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>) on evs" 1824by (blast dest: B_authenticates_A Confidentiality_B A_Issues_B) 1825 1826text\<open>\<open>u_B_authenticates_and_keydist_to_A\<close> would be the same as \<open>B_authenticates_and_keydist_to_A\<close> because the 1827 servK confidentiality assumption is yet unrelaxed\<close> 1828 1829lemma u_B_authenticates_and_keydist_to_A_r: 1830 "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs); 1831 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> 1832 \<in> parts (spies evs); 1833 \<not> expiredSK Ts evs; 1834 B \<noteq> Tgs; A \<notin> bad; B \<notin> bad; evs \<in> kerbIV \<rbrakk> 1835 \<Longrightarrow> A Issues B with (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>) on evs" 1836by (blast dest: u_B_authenticates_A_r u_Confidentiality_B A_Issues_B) 1837 1838end 1839