1(* Title: HOL/Auth/KerberosIV_Gets.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_Gets 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 (* States than an event really appears only once on a trace *) 33 Unique :: "[event, event list] \<Rightarrow> bool" ("Unique _ on _" [0, 50] 50) 34 where "(Unique ev on evs) = (ev \<notin> set (tl (dropWhile (\<lambda>z. z \<noteq> ev) evs)))" 35 36 37consts 38 (*Duration of the authentication key*) 39 authKlife :: nat 40 41 (*Duration of the service key*) 42 servKlife :: nat 43 44 (*Duration of an authenticator*) 45 authlife :: nat 46 47 (*Upper bound on the time of reaction of a server*) 48 replylife :: nat 49 50specification (authKlife) 51 authKlife_LB [iff]: "2 \<le> authKlife" 52 by blast 53 54specification (servKlife) 55 servKlife_LB [iff]: "2 + authKlife \<le> servKlife" 56 by blast 57 58specification (authlife) 59 authlife_LB [iff]: "Suc 0 \<le> authlife" 60 by blast 61 62specification (replylife) 63 replylife_LB [iff]: "Suc 0 \<le> replylife" 64 by blast 65 66abbreviation 67 (*The current time is just the length of the trace!*) 68 CT :: "event list \<Rightarrow> nat" where 69 "CT == length" 70 71abbreviation 72 expiredAK :: "[nat, event list] \<Rightarrow> bool" where 73 "expiredAK Ta evs == authKlife + Ta < CT evs" 74 75abbreviation 76 expiredSK :: "[nat, event list] \<Rightarrow> bool" where 77 "expiredSK Ts evs == servKlife + Ts < CT evs" 78 79abbreviation 80 expiredA :: "[nat, event list] \<Rightarrow> bool" where 81 "expiredA T evs == authlife + T < CT evs" 82 83abbreviation 84 valid :: "[nat, nat] \<Rightarrow> bool" ("valid _ wrt _" [0, 50] 50) where 85 "valid T1 wrt T2 == T1 \<le> replylife + T2" 86 87(*---------------------------------------------------------------------*) 88 89 90(* Predicate formalising the association between authKeys and servKeys *) 91definition AKcryptSK :: "[key, key, event list] \<Rightarrow> bool" where 92 "AKcryptSK authK servK evs == 93 \<exists>A B Ts. 94 Says Tgs A (Crypt authK 95 \<lbrace>Key servK, Agent B, Number Ts, 96 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<rbrace>) 97 \<in> set evs" 98 99inductive_set "kerbIV_gets" :: "event list set" 100 where 101 102 Nil: "[] \<in> kerbIV_gets" 103 104 | Fake: "\<lbrakk> evsf \<in> kerbIV_gets; X \<in> synth (analz (spies evsf)) \<rbrakk> 105 \<Longrightarrow> Says Spy B X # evsf \<in> kerbIV_gets" 106 107 | Reception: "\<lbrakk> evsr \<in> kerbIV_gets; Says A B X \<in> set evsr \<rbrakk> 108 \<Longrightarrow> Gets B X # evsr \<in> kerbIV_gets" 109 110(* FROM the initiator *) 111 | K1: "\<lbrakk> evs1 \<in> kerbIV_gets \<rbrakk> 112 \<Longrightarrow> Says A Kas \<lbrace>Agent A, Agent Tgs, Number (CT evs1)\<rbrace> # evs1 113 \<in> kerbIV_gets" 114 115(* Adding the timestamp serves to A in K3 to check that 116 she doesn't get a reply too late. This kind of timeouts are ordinary. 117 If a server's reply is late, then it is likely to be fake. *) 118 119(*---------------------------------------------------------------------*) 120 121(*FROM Kas *) 122 | K2: "\<lbrakk> evs2 \<in> kerbIV_gets; Key authK \<notin> used evs2; authK \<in> symKeys; 123 Gets Kas \<lbrace>Agent A, Agent Tgs, Number T1\<rbrace> \<in> set evs2 \<rbrakk> 124 \<Longrightarrow> Says Kas A 125 (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number (CT evs2), 126 (Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, 127 Number (CT evs2)\<rbrace>)\<rbrace>) # evs2 \<in> kerbIV_gets" 128(* 129 The internal encryption builds the authTicket. 130 The timestamp doesn't change inside the two encryptions: the external copy 131 will be used by the initiator in K3; the one inside the 132 authTicket by Tgs in K4. 133*) 134 135(*---------------------------------------------------------------------*) 136 137(* FROM the initiator *) 138 | K3: "\<lbrakk> evs3 \<in> kerbIV_gets; 139 Says A Kas \<lbrace>Agent A, Agent Tgs, Number T1\<rbrace> \<in> set evs3; 140 Gets A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, 141 authTicket\<rbrace>) \<in> set evs3; 142 valid Ta wrt T1 143 \<rbrakk> 144 \<Longrightarrow> Says A Tgs \<lbrace>authTicket, 145 (Crypt authK \<lbrace>Agent A, Number (CT evs3)\<rbrace>), 146 Agent B\<rbrace> # evs3 \<in> kerbIV_gets" 147(*The two events amongst the premises allow A to accept only those authKeys 148 that are not issued late. *) 149 150(*---------------------------------------------------------------------*) 151 152(* FROM Tgs *) 153(* Note that the last temporal check is not mentioned in the original MIT 154 specification. Adding it makes many goals "available" to the peers. 155 Theorems that exploit it have the suffix `_u', which stands for updated 156 protocol. 157*) 158 | K4: "\<lbrakk> evs4 \<in> kerbIV_gets; Key servK \<notin> used evs4; servK \<in> symKeys; 159 B \<noteq> Tgs; authK \<in> symKeys; 160 Gets Tgs \<lbrace> 161 (Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, 162 Number Ta\<rbrace>), 163 (Crypt authK \<lbrace>Agent A, Number T2\<rbrace>), Agent B\<rbrace> 164 \<in> set evs4; 165 \<not> expiredAK Ta evs4; 166 \<not> expiredA T2 evs4; 167 servKlife + (CT evs4) \<le> authKlife + Ta 168 \<rbrakk> 169 \<Longrightarrow> Says Tgs A 170 (Crypt authK \<lbrace>Key servK, Agent B, Number (CT evs4), 171 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, 172 Number (CT evs4)\<rbrace> \<rbrace>) 173 # evs4 \<in> kerbIV_gets" 174(* Tgs creates a new session key per each request for a service, without 175 checking if there is still a fresh one for that service. 176 The cipher under Tgs' key is the authTicket, the cipher under B's key 177 is the servTicket, which is built now. 178 NOTE that the last temporal check is not present in the MIT specification. 179 180*) 181 182(*---------------------------------------------------------------------*) 183 184(* FROM the initiator *) 185 | K5: "\<lbrakk> evs5 \<in> kerbIV_gets; authK \<in> symKeys; servK \<in> symKeys; 186 Says A Tgs 187 \<lbrace>authTicket, Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, 188 Agent B\<rbrace> 189 \<in> set evs5; 190 Gets A 191 (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 192 \<in> set evs5; 193 valid Ts wrt T2 \<rbrakk> 194 \<Longrightarrow> Says A B \<lbrace>servTicket, 195 Crypt servK \<lbrace>Agent A, Number (CT evs5)\<rbrace> \<rbrace> 196 # evs5 \<in> kerbIV_gets" 197(* Checks similar to those in K3. *) 198 199(*---------------------------------------------------------------------*) 200 201(* FROM the responder*) 202 | K6: "\<lbrakk> evs6 \<in> kerbIV_gets; 203 Gets B \<lbrace> 204 (Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>), 205 (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>)\<rbrace> 206 \<in> set evs6; 207 \<not> expiredSK Ts evs6; 208 \<not> expiredA T3 evs6 209 \<rbrakk> 210 \<Longrightarrow> Says B A (Crypt servK (Number T3)) 211 # evs6 \<in> kerbIV_gets" 212(* Checks similar to those in K4. *) 213 214(*---------------------------------------------------------------------*) 215 216(* Leaking an authK... *) 217 | Oops1: "\<lbrakk> evsO1 \<in> kerbIV_gets; A \<noteq> Spy; 218 Says Kas A 219 (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, 220 authTicket\<rbrace>) \<in> set evsO1; 221 expiredAK Ta evsO1 \<rbrakk> 222 \<Longrightarrow> Says A Spy \<lbrace>Agent A, Agent Tgs, Number Ta, Key authK\<rbrace> 223 # evsO1 \<in> kerbIV_gets" 224 225(*---------------------------------------------------------------------*) 226 227(*Leaking a servK... *) 228 | Oops2: "\<lbrakk> evsO2 \<in> kerbIV_gets; A \<noteq> Spy; 229 Says Tgs A 230 (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 231 \<in> set evsO2; 232 expiredSK Ts evsO2 \<rbrakk> 233 \<Longrightarrow> Says A Spy \<lbrace>Agent A, Agent B, Number Ts, Key servK\<rbrace> 234 # evsO2 \<in> kerbIV_gets" 235 236(*---------------------------------------------------------------------*) 237 238declare Says_imp_knows_Spy [THEN parts.Inj, dest] 239declare parts.Body [dest] 240declare analz_into_parts [dest] 241declare Fake_parts_insert_in_Un [dest] 242 243subsection\<open>Lemmas about reception event\<close> 244 245lemma Gets_imp_Says : 246 "\<lbrakk> Gets B X \<in> set evs; evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> \<exists>A. Says A B X \<in> set evs" 247apply (erule rev_mp) 248apply (erule kerbIV_gets.induct) 249apply auto 250done 251 252lemma Gets_imp_knows_Spy: 253 "\<lbrakk> Gets B X \<in> set evs; evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> X \<in> knows Spy evs" 254by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) 255 256(*Needed for force to work for example in new_keys_not_used*) 257declare Gets_imp_knows_Spy [THEN parts.Inj, dest] 258 259lemma Gets_imp_knows: 260 "\<lbrakk> Gets B X \<in> set evs; evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> X \<in> knows B evs" 261by (metis Gets_imp_knows_Spy Gets_imp_knows_agents) 262 263subsection\<open>Lemmas about \<^term>\<open>authKeys\<close>\<close> 264 265lemma authKeys_empty: "authKeys [] = {}" 266by (simp add: authKeys_def) 267 268lemma authKeys_not_insert: 269 "(\<forall>A Ta akey Peer. 270 ev \<noteq> Says Kas A (Crypt (shrK A) \<lbrace>akey, Agent Peer, Ta, 271 (Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, akey, Ta\<rbrace>)\<rbrace>)) 272 \<Longrightarrow> authKeys (ev # evs) = authKeys evs" 273by (unfold authKeys_def, auto) 274 275lemma authKeys_insert: 276 "authKeys 277 (Says Kas A (Crypt (shrK A) \<lbrace>Key K, Agent Peer, Number Ta, 278 (Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key K, Number Ta\<rbrace>)\<rbrace>) # evs) 279 = insert K (authKeys evs)" 280by (unfold authKeys_def, auto) 281 282lemma authKeys_simp: 283 "K \<in> authKeys 284 (Says Kas A (Crypt (shrK A) \<lbrace>Key K', Agent Peer, Number Ta, 285 (Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key K', Number Ta\<rbrace>)\<rbrace>) # evs) 286 \<Longrightarrow> K = K' | K \<in> authKeys evs" 287by (unfold authKeys_def, auto) 288 289lemma authKeysI: 290 "Says Kas A (Crypt (shrK A) \<lbrace>Key K, Agent Tgs, Number Ta, 291 (Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key K, Number Ta\<rbrace>)\<rbrace>) \<in> set evs 292 \<Longrightarrow> K \<in> authKeys evs" 293by (unfold authKeys_def, auto) 294 295lemma authKeys_used: "K \<in> authKeys evs \<Longrightarrow> Key K \<in> used evs" 296by (simp add: authKeys_def, blast) 297 298 299subsection\<open>Forwarding Lemmas\<close> 300 301lemma Says_ticket_parts: 302 "Says S A (Crypt K \<lbrace>SesKey, B, TimeStamp, Ticket\<rbrace>) \<in> set evs 303 \<Longrightarrow> Ticket \<in> parts (spies evs)" 304by blast 305 306lemma Gets_ticket_parts: 307 "\<lbrakk>Gets A (Crypt K \<lbrace>SesKey, Peer, Ta, Ticket\<rbrace>) \<in> set evs; evs \<in> kerbIV_gets \<rbrakk> 308 \<Longrightarrow> Ticket \<in> parts (spies evs)" 309by (blast dest: Gets_imp_knows_Spy [THEN parts.Inj]) 310 311lemma Oops_range_spies1: 312 "\<lbrakk> Says Kas A (Crypt KeyA \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>) 313 \<in> set evs ; 314 evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> authK \<notin> range shrK \<and> authK \<in> symKeys" 315apply (erule rev_mp) 316apply (erule kerbIV_gets.induct, auto) 317done 318 319lemma Oops_range_spies2: 320 "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>) 321 \<in> set evs ; 322 evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> servK \<notin> range shrK \<and> servK \<in> symKeys" 323apply (erule rev_mp) 324apply (erule kerbIV_gets.induct, auto) 325done 326 327 328(*Spy never sees another agent's shared key! (unless it's lost at start)*) 329lemma Spy_see_shrK [simp]: 330 "evs \<in> kerbIV_gets \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)" 331apply (erule kerbIV_gets.induct) 332apply (frule_tac [8] Gets_ticket_parts) 333apply (frule_tac [6] Gets_ticket_parts, simp_all) 334apply (blast+) 335done 336 337lemma Spy_analz_shrK [simp]: 338 "evs \<in> kerbIV_gets \<Longrightarrow> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)" 339by auto 340 341lemma Spy_see_shrK_D [dest!]: 342 "\<lbrakk> Key (shrK A) \<in> parts (spies evs); evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> A\<in>bad" 343by (blast dest: Spy_see_shrK) 344lemmas Spy_analz_shrK_D = analz_subset_parts [THEN subsetD, THEN Spy_see_shrK_D, dest!] 345 346text\<open>Nobody can have used non-existent keys!\<close> 347lemma new_keys_not_used [simp]: 348 "\<lbrakk>Key K \<notin> used evs; K \<in> symKeys; evs \<in> kerbIV_gets\<rbrakk> 349 \<Longrightarrow> K \<notin> keysFor (parts (spies evs))" 350apply (erule rev_mp) 351apply (erule kerbIV_gets.induct) 352apply (frule_tac [8] Gets_ticket_parts) 353apply (frule_tac [6] Gets_ticket_parts, simp_all) 354txt\<open>Fake\<close> 355apply (force dest!: keysFor_parts_insert) 356txt\<open>Others\<close> 357apply (force dest!: analz_shrK_Decrypt)+ 358done 359 360(*Earlier, all protocol proofs declared this theorem. 361 But few of them actually need it! (Another is Yahalom) *) 362lemma new_keys_not_analzd: 363 "\<lbrakk>evs \<in> kerbIV_gets; K \<in> symKeys; Key K \<notin> used evs\<rbrakk> 364 \<Longrightarrow> K \<notin> keysFor (analz (spies evs))" 365by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD]) 366 367 368subsection\<open>Regularity Lemmas\<close> 369text\<open>These concern the form of items passed in messages\<close> 370 371text\<open>Describes the form of all components sent by Kas\<close> 372 373lemma Says_Kas_message_form: 374 "\<lbrakk> Says Kas A (Crypt K \<lbrace>Key authK, Agent Peer, Number Ta, authTicket\<rbrace>) 375 \<in> set evs; 376 evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> 377 K = shrK A \<and> Peer = Tgs \<and> 378 authK \<notin> range shrK \<and> authK \<in> authKeys evs \<and> authK \<in> symKeys \<and> 379 authTicket = (Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>)" 380apply (erule rev_mp) 381apply (erule kerbIV_gets.induct) 382apply (simp_all (no_asm) add: authKeys_def authKeys_insert) 383apply blast+ 384done 385 386 387lemma SesKey_is_session_key: 388 "\<lbrakk> Crypt (shrK Tgs_B) \<lbrace>Agent A, Agent Tgs_B, Key SesKey, Number T\<rbrace> 389 \<in> parts (spies evs); Tgs_B \<notin> bad; 390 evs \<in> kerbIV_gets \<rbrakk> 391 \<Longrightarrow> SesKey \<notin> range shrK" 392apply (erule rev_mp) 393apply (erule kerbIV_gets.induct) 394apply (frule_tac [8] Gets_ticket_parts) 395apply (frule_tac [6] Gets_ticket_parts, simp_all, blast) 396done 397 398lemma authTicket_authentic: 399 "\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace> 400 \<in> parts (spies evs); 401 evs \<in> kerbIV_gets \<rbrakk> 402 \<Longrightarrow> Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, 403 Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>) 404 \<in> set evs" 405apply (erule rev_mp) 406apply (erule kerbIV_gets.induct) 407apply (frule_tac [8] Gets_ticket_parts) 408apply (frule_tac [6] Gets_ticket_parts, simp_all) 409txt\<open>Fake, K4\<close> 410apply (blast+) 411done 412 413lemma authTicket_crypt_authK: 414 "\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace> 415 \<in> parts (spies evs); 416 evs \<in> kerbIV_gets \<rbrakk> 417 \<Longrightarrow> authK \<in> authKeys evs" 418apply (frule authTicket_authentic, assumption) 419apply (simp (no_asm) add: authKeys_def) 420apply blast 421done 422 423lemma Says_Tgs_message_form: 424 "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 425 \<in> set evs; 426 evs \<in> kerbIV_gets \<rbrakk> 427 \<Longrightarrow> B \<noteq> Tgs \<and> 428 authK \<notin> range shrK \<and> authK \<in> authKeys evs \<and> authK \<in> symKeys \<and> 429 servK \<notin> range shrK \<and> servK \<notin> authKeys evs \<and> servK \<in> symKeys \<and> 430 servTicket = (Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>)" 431apply (erule rev_mp) 432apply (erule kerbIV_gets.induct) 433apply (simp_all add: authKeys_insert authKeys_not_insert authKeys_empty authKeys_simp, blast, auto) 434txt\<open>Three subcases of Message 4\<close> 435apply (blast dest!: SesKey_is_session_key) 436apply (blast dest: authTicket_crypt_authK) 437apply (blast dest!: authKeys_used Says_Kas_message_form) 438done 439 440 441lemma authTicket_form: 442 "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Ta, authTicket\<rbrace> 443 \<in> parts (spies evs); 444 A \<notin> bad; 445 evs \<in> kerbIV_gets \<rbrakk> 446 \<Longrightarrow> authK \<notin> range shrK \<and> authK \<in> symKeys \<and> 447 authTicket = Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Ta\<rbrace>" 448apply (erule rev_mp) 449apply (erule kerbIV_gets.induct) 450apply (frule_tac [8] Gets_ticket_parts) 451apply (frule_tac [6] Gets_ticket_parts, simp_all) 452apply blast+ 453done 454 455text\<open>This form holds also over an authTicket, but is not needed below.\<close> 456lemma servTicket_form: 457 "\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace> 458 \<in> parts (spies evs); 459 Key authK \<notin> analz (spies evs); 460 evs \<in> kerbIV_gets \<rbrakk> 461 \<Longrightarrow> servK \<notin> range shrK \<and> servK \<in> symKeys \<and> 462 (\<exists>A. servTicket = Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace>)" 463apply (erule rev_mp) 464apply (erule rev_mp) 465apply (erule kerbIV_gets.induct, analz_mono_contra) 466apply (frule_tac [8] Gets_ticket_parts) 467apply (frule_tac [6] Gets_ticket_parts, simp_all, blast) 468done 469 470text\<open>Essentially the same as \<open>authTicket_form\<close>\<close> 471lemma Says_kas_message_form: 472 "\<lbrakk> Gets A (Crypt (shrK A) 473 \<lbrace>Key authK, Agent Tgs, Ta, authTicket\<rbrace>) \<in> set evs; 474 evs \<in> kerbIV_gets \<rbrakk> 475 \<Longrightarrow> authK \<notin> range shrK \<and> authK \<in> symKeys \<and> 476 authTicket = 477 Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Ta\<rbrace> 478 | authTicket \<in> analz (spies evs)" 479by (blast dest: analz_shrK_Decrypt authTicket_form 480 Gets_imp_knows_Spy [THEN analz.Inj]) 481 482lemma Says_tgs_message_form: 483 "\<lbrakk> Gets A (Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>) 484 \<in> set evs; authK \<in> symKeys; 485 evs \<in> kerbIV_gets \<rbrakk> 486 \<Longrightarrow> servK \<notin> range shrK \<and> 487 (\<exists>A. servTicket = 488 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace>) 489 | servTicket \<in> analz (spies evs)" 490apply (frule Gets_imp_knows_Spy [THEN analz.Inj], auto) 491 apply (force dest!: servTicket_form) 492apply (frule analz_into_parts) 493apply (frule servTicket_form, auto) 494done 495 496 497subsection\<open>Authenticity theorems: confirm origin of sensitive messages\<close> 498 499lemma authK_authentic: 500 "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace> 501 \<in> parts (spies evs); 502 A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk> 503 \<Longrightarrow> Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>) 504 \<in> set evs" 505apply (erule rev_mp) 506apply (erule kerbIV_gets.induct) 507apply (frule_tac [8] Gets_ticket_parts) 508apply (frule_tac [6] Gets_ticket_parts, simp_all) 509txt\<open>Fake\<close> 510apply blast 511txt\<open>K4\<close> 512apply (blast dest!: authTicket_authentic [THEN Says_Kas_message_form]) 513done 514 515text\<open>If a certain encrypted message appears then it originated with Tgs\<close> 516lemma servK_authentic: 517 "\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace> 518 \<in> parts (spies evs); 519 Key authK \<notin> analz (spies evs); 520 authK \<notin> range shrK; 521 evs \<in> kerbIV_gets \<rbrakk> 522 \<Longrightarrow> \<exists>A. Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 523 \<in> set evs" 524apply (erule rev_mp) 525apply (erule rev_mp) 526apply (erule kerbIV_gets.induct, analz_mono_contra) 527apply (frule_tac [8] Gets_ticket_parts) 528apply (frule_tac [6] Gets_ticket_parts, simp_all) 529txt\<open>Fake\<close> 530apply blast 531txt\<open>K2\<close> 532apply blast 533txt\<open>K4\<close> 534apply auto 535done 536 537lemma servK_authentic_bis: 538 "\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace> 539 \<in> parts (spies evs); 540 Key authK \<notin> analz (spies evs); 541 B \<noteq> Tgs; 542 evs \<in> kerbIV_gets \<rbrakk> 543 \<Longrightarrow> \<exists>A. Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 544 \<in> set evs" 545apply (erule rev_mp) 546apply (erule rev_mp) 547apply (erule kerbIV_gets.induct, analz_mono_contra) 548apply (frule_tac [8] Gets_ticket_parts) 549apply (frule_tac [6] Gets_ticket_parts, simp_all) 550txt\<open>Fake\<close> 551apply blast 552txt\<open>K4\<close> 553apply blast 554done 555 556text\<open>Authenticity of servK for B\<close> 557lemma servTicket_authentic_Tgs: 558 "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> 559 \<in> parts (spies evs); B \<noteq> Tgs; B \<notin> bad; 560 evs \<in> kerbIV_gets \<rbrakk> 561 \<Longrightarrow> \<exists>authK. 562 Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, 563 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>) 564 \<in> set evs" 565apply (erule rev_mp) 566apply (erule rev_mp) 567apply (erule kerbIV_gets.induct) 568apply (frule_tac [8] Gets_ticket_parts) 569apply (frule_tac [6] Gets_ticket_parts, simp_all) 570apply blast+ 571done 572 573text\<open>Anticipated here from next subsection\<close> 574lemma K4_imp_K2: 575"\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 576 \<in> set evs; evs \<in> kerbIV_gets\<rbrakk> 577 \<Longrightarrow> \<exists>Ta. Says Kas A 578 (Crypt (shrK A) 579 \<lbrace>Key authK, Agent Tgs, Number Ta, 580 Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>) 581 \<in> set evs" 582apply (erule rev_mp) 583apply (erule kerbIV_gets.induct) 584apply (frule_tac [8] Gets_ticket_parts) 585apply (frule_tac [6] Gets_ticket_parts, simp_all, auto) 586apply (blast dest!: Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Fst, THEN authTicket_authentic]) 587done 588 589text\<open>Anticipated here from next subsection\<close> 590lemma u_K4_imp_K2: 591"\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 592 \<in> set evs; evs \<in> kerbIV_gets\<rbrakk> 593 \<Longrightarrow> \<exists>Ta. (Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, 594 Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>) 595 \<in> set evs 596 \<and> servKlife + Ts \<le> authKlife + Ta)" 597apply (erule rev_mp) 598apply (erule kerbIV_gets.induct) 599apply (frule_tac [8] Gets_ticket_parts) 600apply (frule_tac [6] Gets_ticket_parts, simp_all, auto) 601apply (blast dest!: Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Fst, THEN authTicket_authentic]) 602done 603 604lemma servTicket_authentic_Kas: 605 "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> 606 \<in> parts (spies evs); B \<noteq> Tgs; B \<notin> bad; 607 evs \<in> kerbIV_gets \<rbrakk> 608 \<Longrightarrow> \<exists>authK Ta. 609 Says Kas A 610 (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, 611 Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>) 612 \<in> set evs" 613by (blast dest!: servTicket_authentic_Tgs K4_imp_K2) 614 615lemma u_servTicket_authentic_Kas: 616 "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> 617 \<in> parts (spies evs); B \<noteq> Tgs; B \<notin> bad; 618 evs \<in> kerbIV_gets \<rbrakk> 619 \<Longrightarrow> \<exists>authK Ta. Says Kas A (Crypt(shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, 620 Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>) 621 \<in> set evs 622 \<and> servKlife + Ts \<le> authKlife + Ta" 623by (blast dest!: servTicket_authentic_Tgs u_K4_imp_K2) 624 625lemma servTicket_authentic: 626 "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> 627 \<in> parts (spies evs); B \<noteq> Tgs; B \<notin> bad; 628 evs \<in> kerbIV_gets \<rbrakk> 629 \<Longrightarrow> \<exists>Ta authK. 630 Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, 631 Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>) 632 \<in> set evs 633 \<and> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, 634 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>) 635 \<in> set evs" 636by (blast dest: servTicket_authentic_Tgs K4_imp_K2) 637 638lemma u_servTicket_authentic: 639 "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> 640 \<in> parts (spies evs); B \<noteq> Tgs; B \<notin> bad; 641 evs \<in> kerbIV_gets \<rbrakk> 642 \<Longrightarrow> \<exists>Ta authK. 643 (Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, 644 Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>) 645 \<in> set evs 646 \<and> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, 647 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>) 648 \<in> set evs 649 \<and> servKlife + Ts \<le> authKlife + Ta)" 650by (blast dest: servTicket_authentic_Tgs u_K4_imp_K2) 651 652lemma u_NotexpiredSK_NotexpiredAK: 653 "\<lbrakk> \<not> expiredSK Ts evs; servKlife + Ts \<le> authKlife + Ta \<rbrakk> 654 \<Longrightarrow> \<not> expiredAK Ta evs" 655by (blast dest: leI le_trans dest: leD) 656 657 658subsection\<open>Reliability: friendly agents send something if something else happened\<close> 659 660lemma K3_imp_K2: 661 "\<lbrakk> Says A Tgs 662 \<lbrace>authTicket, Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B\<rbrace> 663 \<in> set evs; 664 A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk> 665 \<Longrightarrow> \<exists>Ta. Says Kas A (Crypt (shrK A) 666 \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>) 667 \<in> set evs" 668apply (erule rev_mp) 669apply (erule kerbIV_gets.induct) 670apply (frule_tac [8] Gets_ticket_parts) 671apply (frule_tac [6] Gets_ticket_parts, simp_all, blast, blast) 672apply (blast dest: Gets_imp_knows_Spy [THEN parts.Inj, THEN authK_authentic]) 673done 674 675text\<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> 676lemma Key_unique_SesKey: 677 "\<lbrakk> Crypt K \<lbrace>Key SesKey, Agent B, T, Ticket\<rbrace> 678 \<in> parts (spies evs); 679 Crypt K' \<lbrace>Key SesKey, Agent B', T', Ticket'\<rbrace> 680 \<in> parts (spies evs); Key SesKey \<notin> analz (spies evs); 681 evs \<in> kerbIV_gets \<rbrakk> 682 \<Longrightarrow> K=K' \<and> B=B' \<and> T=T' \<and> Ticket=Ticket'" 683apply (erule rev_mp) 684apply (erule rev_mp) 685apply (erule rev_mp) 686apply (erule kerbIV_gets.induct, analz_mono_contra) 687apply (frule_tac [8] Gets_ticket_parts) 688apply (frule_tac [6] Gets_ticket_parts, simp_all) 689txt\<open>Fake, K2, K4\<close> 690apply (blast+) 691done 692 693lemma Tgs_authenticates_A: 694 "\<lbrakk> Crypt authK \<lbrace>Agent A, Number T2\<rbrace> \<in> parts (spies evs); 695 Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace> 696 \<in> parts (spies evs); 697 Key authK \<notin> analz (spies evs); A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk> 698 \<Longrightarrow> \<exists> B. Says A Tgs \<lbrace> 699 Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>, 700 Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B \<rbrace> \<in> set evs" 701apply (drule authTicket_authentic, assumption, rotate_tac 4) 702apply (erule rev_mp, erule rev_mp, erule rev_mp) 703apply (erule kerbIV_gets.induct, analz_mono_contra) 704apply (frule_tac [6] Gets_ticket_parts) 705apply (frule_tac [9] Gets_ticket_parts) 706apply (simp_all (no_asm_simp) add: all_conj_distrib) 707txt\<open>Fake\<close> 708apply blast 709txt\<open>K2\<close> 710apply (force dest!: Crypt_imp_keysFor) 711txt\<open>K3\<close> 712apply (blast dest: Key_unique_SesKey) 713txt\<open>K5\<close> 714txt\<open>If authKa were compromised, so would be authK\<close> 715apply (case_tac "Key authKa \<in> analz (spies evs5)") 716apply (force dest!: Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst]) 717txt\<open>Besides, since authKa originated with Kas anyway...\<close> 718apply (clarify, drule K3_imp_K2, assumption, assumption) 719apply (clarify, drule Says_Kas_message_form, assumption) 720txt\<open>...it cannot be a shared key*. Therefore \<^term>\<open>servK_authentic\<close> applies. 721 Contradition: Tgs used authK as a servkey, 722 while Kas used it as an authkey\<close> 723apply (blast dest: servK_authentic Says_Tgs_message_form) 724done 725 726lemma Says_K5: 727 "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs); 728 Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, 729 servTicket\<rbrace>) \<in> set evs; 730 Key servK \<notin> analz (spies evs); 731 A \<notin> bad; B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk> 732 \<Longrightarrow> Says A B \<lbrace>servTicket, Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> \<in> set evs" 733apply (erule rev_mp) 734apply (erule rev_mp) 735apply (erule rev_mp) 736apply (erule kerbIV_gets.induct, analz_mono_contra) 737apply (frule_tac [6] Gets_ticket_parts) 738apply (frule_tac [9] Gets_ticket_parts) 739apply (simp_all (no_asm_simp) add: all_conj_distrib) 740apply blast 741txt\<open>K3\<close> 742apply (blast dest: authK_authentic Says_Kas_message_form Says_Tgs_message_form) 743txt\<open>K4\<close> 744apply (force dest!: Crypt_imp_keysFor) 745txt\<open>K5\<close> 746apply (blast dest: Key_unique_SesKey) 747done 748 749text\<open>Anticipated here from next subsection\<close> 750lemma unique_CryptKey: 751 "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key SesKey, T\<rbrace> 752 \<in> parts (spies evs); 753 Crypt (shrK B') \<lbrace>Agent A', Agent B', Key SesKey, T'\<rbrace> 754 \<in> parts (spies evs); Key SesKey \<notin> analz (spies evs); 755 evs \<in> kerbIV_gets \<rbrakk> 756 \<Longrightarrow> A=A' \<and> B=B' \<and> T=T'" 757apply (erule rev_mp) 758apply (erule rev_mp) 759apply (erule rev_mp) 760apply (erule kerbIV_gets.induct, analz_mono_contra) 761apply (frule_tac [8] Gets_ticket_parts) 762apply (frule_tac [6] Gets_ticket_parts, simp_all) 763txt\<open>Fake, K2, K4\<close> 764apply (blast+) 765done 766 767lemma Says_K6: 768 "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs); 769 Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, 770 servTicket\<rbrace>) \<in> set evs; 771 Key servK \<notin> analz (spies evs); 772 A \<notin> bad; B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk> 773 \<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> set evs" 774apply (erule rev_mp) 775apply (erule rev_mp) 776apply (erule rev_mp) 777apply (erule kerbIV_gets.induct, analz_mono_contra) 778apply (frule_tac [8] Gets_ticket_parts) 779apply (frule_tac [6] Gets_ticket_parts) 780apply (simp_all (no_asm_simp)) 781apply blast 782apply (force dest!: Crypt_imp_keysFor, clarify) 783apply (frule Says_Tgs_message_form, assumption, clarify) (*PROOF FAILED if omitted*) 784apply (blast dest: unique_CryptKey) 785done 786 787text\<open>Needs a unicity theorem, hence moved here\<close> 788lemma servK_authentic_ter: 789 "\<lbrakk> Says Kas A 790 (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>) \<in> set evs; 791 Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace> 792 \<in> parts (spies evs); 793 Key authK \<notin> analz (spies evs); 794 evs \<in> kerbIV_gets \<rbrakk> 795 \<Longrightarrow> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 796 \<in> set evs" 797apply (frule Says_Kas_message_form, assumption) 798apply (erule rev_mp) 799apply (erule rev_mp) 800apply (erule rev_mp) 801apply (erule kerbIV_gets.induct, analz_mono_contra) 802apply (frule_tac [8] Gets_ticket_parts) 803apply (frule_tac [6] Gets_ticket_parts, simp_all, blast) 804txt\<open>K2 and K4 remain\<close> 805prefer 2 apply (blast dest!: unique_CryptKey) 806apply (blast dest!: servK_authentic Says_Tgs_message_form authKeys_used) 807done 808 809 810subsection\<open>Unicity Theorems\<close> 811 812text\<open>The session key, if secure, uniquely identifies the Ticket 813 whether authTicket or servTicket. As a matter of fact, one can read 814 also Tgs in the place of B.\<close> 815 816 817lemma unique_authKeys: 818 "\<lbrakk> Says Kas A 819 (Crypt Ka \<lbrace>Key authK, Agent Tgs, Ta, X\<rbrace>) \<in> set evs; 820 Says Kas A' 821 (Crypt Ka' \<lbrace>Key authK, Agent Tgs, Ta', X'\<rbrace>) \<in> set evs; 822 evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> A=A' \<and> Ka=Ka' \<and> Ta=Ta' \<and> X=X'" 823apply (erule rev_mp) 824apply (erule rev_mp) 825apply (erule kerbIV_gets.induct) 826apply (frule_tac [8] Gets_ticket_parts) 827apply (frule_tac [6] Gets_ticket_parts, simp_all) 828txt\<open>K2\<close> 829apply blast 830done 831 832text\<open>servK uniquely identifies the message from Tgs\<close> 833lemma unique_servKeys: 834 "\<lbrakk> Says Tgs A 835 (Crypt K \<lbrace>Key servK, Agent B, Ts, X\<rbrace>) \<in> set evs; 836 Says Tgs A' 837 (Crypt K' \<lbrace>Key servK, Agent B', Ts', X'\<rbrace>) \<in> set evs; 838 evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> A=A' \<and> B=B' \<and> K=K' \<and> Ts=Ts' \<and> X=X'" 839apply (erule rev_mp) 840apply (erule rev_mp) 841apply (erule kerbIV_gets.induct) 842apply (frule_tac [8] Gets_ticket_parts) 843apply (frule_tac [6] Gets_ticket_parts, simp_all) 844txt\<open>K4\<close> 845apply blast 846done 847 848text\<open>Revised unicity theorems\<close> 849 850lemma Kas_Unique: 851 "\<lbrakk> Says Kas A 852 (Crypt Ka \<lbrace>Key authK, Agent Tgs, Ta, authTicket\<rbrace>) \<in> set evs; 853 evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> 854 Unique (Says Kas A (Crypt Ka \<lbrace>Key authK, Agent Tgs, Ta, authTicket\<rbrace>)) 855 on evs" 856apply (erule rev_mp, erule kerbIV_gets.induct, simp_all add: Unique_def) 857apply blast 858done 859 860lemma Tgs_Unique: 861 "\<lbrakk> Says Tgs A 862 (Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>) \<in> set evs; 863 evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> 864 Unique (Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>)) 865 on evs" 866apply (erule rev_mp, erule kerbIV_gets.induct, simp_all add: Unique_def) 867apply blast 868done 869 870 871subsection\<open>Lemmas About the Predicate \<^term>\<open>AKcryptSK\<close>\<close> 872 873lemma not_AKcryptSK_Nil [iff]: "\<not> AKcryptSK authK servK []" 874by (simp add: AKcryptSK_def) 875 876lemma AKcryptSKI: 877 "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, X \<rbrace>) \<in> set evs; 878 evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> AKcryptSK authK servK evs" 879apply (unfold AKcryptSK_def) 880apply (blast dest: Says_Tgs_message_form) 881done 882 883lemma AKcryptSK_Says [simp]: 884 "AKcryptSK authK servK (Says S A X # evs) = 885 (Tgs = S \<and> 886 (\<exists>B Ts. X = Crypt authK 887 \<lbrace>Key servK, Agent B, Number Ts, 888 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<rbrace>) 889 | AKcryptSK authK servK evs)" 890by (auto simp add: AKcryptSK_def) 891 892(*A fresh authK cannot be associated with any other 893 (with respect to a given trace). *) 894lemma Auth_fresh_not_AKcryptSK: 895 "\<lbrakk> Key authK \<notin> used evs; evs \<in> kerbIV_gets \<rbrakk> 896 \<Longrightarrow> \<not> AKcryptSK authK servK evs" 897apply (unfold AKcryptSK_def) 898apply (erule rev_mp) 899apply (erule kerbIV_gets.induct) 900apply (frule_tac [8] Gets_ticket_parts) 901apply (frule_tac [6] Gets_ticket_parts, simp_all, blast) 902done 903 904(*A fresh servK cannot be associated with any other 905 (with respect to a given trace). *) 906lemma Serv_fresh_not_AKcryptSK: 907 "Key servK \<notin> used evs \<Longrightarrow> \<not> AKcryptSK authK servK evs" 908by (unfold AKcryptSK_def, blast) 909 910lemma authK_not_AKcryptSK: 911 "\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, tk\<rbrace> 912 \<in> parts (spies evs); evs \<in> kerbIV_gets \<rbrakk> 913 \<Longrightarrow> \<not> AKcryptSK K authK evs" 914apply (erule rev_mp) 915apply (erule kerbIV_gets.induct) 916apply (frule_tac [8] Gets_ticket_parts) 917apply (frule_tac [6] Gets_ticket_parts, simp_all) 918txt\<open>Fake\<close> 919apply blast 920txt\<open>Reception\<close> 921apply (simp add: AKcryptSK_def) 922txt\<open>K2: by freshness\<close> 923apply (simp add: AKcryptSK_def) 924txt\<open>K4\<close> 925by (blast+) 926 927text\<open>A secure serverkey cannot have been used to encrypt others\<close> 928lemma servK_not_AKcryptSK: 929 "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key SK, Number Ts\<rbrace> \<in> parts (spies evs); 930 Key SK \<notin> analz (spies evs); SK \<in> symKeys; 931 B \<noteq> Tgs; evs \<in> kerbIV_gets \<rbrakk> 932 \<Longrightarrow> \<not> AKcryptSK SK K evs" 933apply (erule rev_mp) 934apply (erule rev_mp) 935apply (erule kerbIV_gets.induct, analz_mono_contra) 936apply (frule_tac [8] Gets_ticket_parts) 937apply (frule_tac [6] Gets_ticket_parts, simp_all, blast) 938txt\<open>Reception\<close> 939apply (simp add: AKcryptSK_def) 940txt\<open>K4 splits into distinct subcases\<close> 941apply auto 942txt\<open>servK can't have been enclosed in two certificates\<close> 943 prefer 2 apply (blast dest: unique_CryptKey) 944txt\<open>servK is fresh and so could not have been used, by 945 \<open>new_keys_not_used\<close>\<close> 946by (force dest!: Crypt_imp_invKey_keysFor simp add: AKcryptSK_def) 947 948text\<open>Long term keys are not issued as servKeys\<close> 949lemma shrK_not_AKcryptSK: 950 "evs \<in> kerbIV_gets \<Longrightarrow> \<not> AKcryptSK K (shrK A) evs" 951apply (unfold AKcryptSK_def) 952apply (erule kerbIV_gets.induct) 953apply (frule_tac [8] Gets_ticket_parts) 954by (frule_tac [6] Gets_ticket_parts, auto) 955 956text\<open>The Tgs message associates servK with authK and therefore not with any 957 other key authK.\<close> 958lemma Says_Tgs_AKcryptSK: 959 "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, X \<rbrace>) 960 \<in> set evs; 961 authK' \<noteq> authK; evs \<in> kerbIV_gets \<rbrakk> 962 \<Longrightarrow> \<not> AKcryptSK authK' servK evs" 963apply (unfold AKcryptSK_def) 964by (blast dest: unique_servKeys) 965 966text\<open>Equivalently\<close> 967lemma not_different_AKcryptSK: 968 "\<lbrakk> AKcryptSK authK servK evs; 969 authK' \<noteq> authK; evs \<in> kerbIV_gets \<rbrakk> 970 \<Longrightarrow> \<not> AKcryptSK authK' servK evs \<and> servK \<in> symKeys" 971apply (simp add: AKcryptSK_def) 972by (blast dest: unique_servKeys Says_Tgs_message_form) 973 974lemma AKcryptSK_not_AKcryptSK: 975 "\<lbrakk> AKcryptSK authK servK evs; evs \<in> kerbIV_gets \<rbrakk> 976 \<Longrightarrow> \<not> AKcryptSK servK K evs" 977apply (erule rev_mp) 978apply (erule kerbIV_gets.induct) 979apply (frule_tac [8] Gets_ticket_parts) 980apply (frule_tac [6] Gets_ticket_parts) 981txt\<open>Reception\<close> 982prefer 3 apply (simp add: AKcryptSK_def) 983apply (simp_all, safe) 984txt\<open>K4 splits into subcases\<close> 985prefer 4 apply (blast dest!: authK_not_AKcryptSK) 986txt\<open>servK is fresh and so could not have been used, by 987 \<open>new_keys_not_used\<close>\<close> 988 prefer 2 989 apply (force dest!: Crypt_imp_invKey_keysFor simp add: AKcryptSK_def) 990txt\<open>Others by freshness\<close> 991by (blast+) 992 993text\<open>The only session keys that can be found with the help of session keys are 994 those sent by Tgs in step K4.\<close> 995 996text\<open>We take some pains to express the property 997 as a logical equivalence so that the simplifier can apply it.\<close> 998lemma Key_analz_image_Key_lemma: 999 "P \<longrightarrow> (Key K \<in> analz (Key`KK \<union> H)) \<longrightarrow> (K \<in> KK | Key K \<in> analz H) 1000 \<Longrightarrow> 1001 P \<longrightarrow> (Key K \<in> analz (Key`KK \<union> H)) = (K \<in> KK | Key K \<in> analz H)" 1002by (blast intro: analz_mono [THEN subsetD]) 1003 1004 1005lemma AKcryptSK_analz_insert: 1006 "\<lbrakk> AKcryptSK K K' evs; K \<in> symKeys; evs \<in> kerbIV_gets \<rbrakk> 1007 \<Longrightarrow> Key K' \<in> analz (insert (Key K) (spies evs))" 1008apply (simp add: AKcryptSK_def, clarify) 1009by (drule Says_imp_spies [THEN analz.Inj, THEN analz_insertI], auto) 1010 1011lemma authKeys_are_not_AKcryptSK: 1012 "\<lbrakk> K \<in> authKeys evs \<union> range shrK; evs \<in> kerbIV_gets \<rbrakk> 1013 \<Longrightarrow> \<forall>SK. \<not> AKcryptSK SK K evs \<and> K \<in> symKeys" 1014apply (simp add: authKeys_def AKcryptSK_def) 1015by (blast dest: Says_Kas_message_form Says_Tgs_message_form) 1016 1017lemma not_authKeys_not_AKcryptSK: 1018 "\<lbrakk> K \<notin> authKeys evs; 1019 K \<notin> range shrK; evs \<in> kerbIV_gets \<rbrakk> 1020 \<Longrightarrow> \<forall>SK. \<not> AKcryptSK K SK evs" 1021apply (simp add: AKcryptSK_def) 1022by (blast dest: Says_Tgs_message_form) 1023 1024 1025subsection\<open>Secrecy Theorems\<close> 1026 1027text\<open>For the Oops2 case of the next theorem\<close> 1028lemma Oops2_not_AKcryptSK: 1029 "\<lbrakk> evs \<in> kerbIV_gets; 1030 Says Tgs A (Crypt authK 1031 \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 1032 \<in> set evs \<rbrakk> 1033 \<Longrightarrow> \<not> AKcryptSK servK SK evs" 1034by (blast dest: AKcryptSKI AKcryptSK_not_AKcryptSK) 1035 1036text\<open>Big simplification law for keys SK that are not crypted by keys in KK 1037 It helps prove three, otherwise hard, facts about keys. These facts are 1038 exploited as simplification laws for analz, and also "limit the damage" 1039 in case of loss of a key to the spy. See ESORICS98.\<close> 1040lemma Key_analz_image_Key [rule_format (no_asm)]: 1041 "evs \<in> kerbIV_gets \<Longrightarrow> 1042 (\<forall>SK KK. SK \<in> symKeys \<and> KK \<subseteq> -(range shrK) \<longrightarrow> 1043 (\<forall>K \<in> KK. \<not> AKcryptSK K SK evs) \<longrightarrow> 1044 (Key SK \<in> analz (Key`KK \<union> (spies evs))) = 1045 (SK \<in> KK | Key SK \<in> analz (spies evs)))" 1046apply (erule kerbIV_gets.induct) 1047apply (frule_tac [11] Oops_range_spies2) 1048apply (frule_tac [10] Oops_range_spies1) 1049apply (frule_tac [8] Says_tgs_message_form) 1050apply (frule_tac [6] Says_kas_message_form) 1051apply (safe del: impI intro!: Key_analz_image_Key_lemma [THEN impI]) 1052txt\<open>Case-splits for Oops1 and message 5: the negated case simplifies using 1053 the induction hypothesis\<close> 1054apply (case_tac [12] "AKcryptSK authK SK evsO1") 1055apply (case_tac [9] "AKcryptSK servK SK evs5") 1056apply (simp_all del: image_insert 1057 add: analz_image_freshK_simps AKcryptSK_Says shrK_not_AKcryptSK 1058 Oops2_not_AKcryptSK Auth_fresh_not_AKcryptSK 1059 Serv_fresh_not_AKcryptSK Says_Tgs_AKcryptSK Spy_analz_shrK) 1060 \<comment> \<open>18 seconds on a 1.8GHz machine??\<close> 1061txt\<open>Fake\<close> 1062apply spy_analz 1063txt\<open>Reception\<close> 1064apply (simp add: AKcryptSK_def) 1065txt\<open>K2\<close> 1066apply blast 1067txt\<open>K3\<close> 1068apply blast 1069txt\<open>K4\<close> 1070apply (blast dest!: authK_not_AKcryptSK) 1071txt\<open>K5\<close> 1072apply (case_tac "Key servK \<in> analz (spies evs5) ") 1073txt\<open>If servK is compromised then the result follows directly...\<close> 1074apply (simp (no_asm_simp) add: analz_insert_eq Un_upper2 [THEN analz_mono, THEN subsetD]) 1075txt\<open>...therefore servK is uncompromised.\<close> 1076txt\<open>The AKcryptSK servK SK evs5 case leads to a contradiction.\<close> 1077apply (blast elim!: servK_not_AKcryptSK [THEN [2] rev_notE] del: allE ballE) 1078txt\<open>Another K5 case\<close> 1079apply blast 1080txt\<open>Oops1\<close> 1081apply simp 1082by (blast dest!: AKcryptSK_analz_insert) 1083 1084text\<open>First simplification law for analz: no session keys encrypt 1085authentication keys or shared keys.\<close> 1086lemma analz_insert_freshK1: 1087 "\<lbrakk> evs \<in> kerbIV_gets; K \<in> authKeys evs \<union> range shrK; 1088 SesKey \<notin> range shrK \<rbrakk> 1089 \<Longrightarrow> (Key K \<in> analz (insert (Key SesKey) (spies evs))) = 1090 (K = SesKey | Key K \<in> analz (spies evs))" 1091apply (frule authKeys_are_not_AKcryptSK, assumption) 1092apply (simp del: image_insert 1093 add: analz_image_freshK_simps add: Key_analz_image_Key) 1094done 1095 1096 1097text\<open>Second simplification law for analz: no service keys encrypt any other keys.\<close> 1098lemma analz_insert_freshK2: 1099 "\<lbrakk> evs \<in> kerbIV_gets; servK \<notin> (authKeys evs); servK \<notin> range shrK; 1100 K \<in> symKeys \<rbrakk> 1101 \<Longrightarrow> (Key K \<in> analz (insert (Key servK) (spies evs))) = 1102 (K = servK | Key K \<in> analz (spies evs))" 1103apply (frule not_authKeys_not_AKcryptSK, assumption, assumption) 1104apply (simp del: image_insert 1105 add: analz_image_freshK_simps add: Key_analz_image_Key) 1106done 1107 1108 1109text\<open>Third simplification law for analz: only one authentication key encrypts a certain service key.\<close> 1110 1111lemma analz_insert_freshK3: 1112 "\<lbrakk> AKcryptSK authK servK evs; 1113 authK' \<noteq> authK; authK' \<notin> range shrK; evs \<in> kerbIV_gets \<rbrakk> 1114 \<Longrightarrow> (Key servK \<in> analz (insert (Key authK') (spies evs))) = 1115 (servK = authK' | Key servK \<in> analz (spies evs))" 1116apply (drule_tac authK' = authK' in not_different_AKcryptSK, blast, assumption) 1117apply (simp del: image_insert 1118 add: analz_image_freshK_simps add: Key_analz_image_Key) 1119done 1120 1121lemma analz_insert_freshK3_bis: 1122 "\<lbrakk> Says Tgs A 1123 (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 1124 \<in> set evs; 1125 authK \<noteq> authK'; authK' \<notin> range shrK; evs \<in> kerbIV_gets \<rbrakk> 1126 \<Longrightarrow> (Key servK \<in> analz (insert (Key authK') (spies evs))) = 1127 (servK = authK' | Key servK \<in> analz (spies evs))" 1128apply (frule AKcryptSKI, assumption) 1129by (simp add: analz_insert_freshK3) 1130 1131text\<open>a weakness of the protocol\<close> 1132lemma authK_compromises_servK: 1133 "\<lbrakk> Says Tgs A 1134 (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 1135 \<in> set evs; authK \<in> symKeys; 1136 Key authK \<in> analz (spies evs); evs \<in> kerbIV_gets \<rbrakk> 1137 \<Longrightarrow> Key servK \<in> analz (spies evs)" 1138by (force dest: Says_imp_spies [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst]) 1139 1140lemma servK_notin_authKeysD: 1141 "\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Ts, 1142 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace>\<rbrace> 1143 \<in> parts (spies evs); 1144 Key servK \<notin> analz (spies evs); 1145 B \<noteq> Tgs; evs \<in> kerbIV_gets \<rbrakk> 1146 \<Longrightarrow> servK \<notin> authKeys evs" 1147apply (erule rev_mp) 1148apply (erule rev_mp) 1149apply (simp add: authKeys_def) 1150apply (erule kerbIV_gets.induct, analz_mono_contra) 1151apply (frule_tac [8] Gets_ticket_parts) 1152apply (frule_tac [6] Gets_ticket_parts, simp_all) 1153by (blast+) 1154 1155 1156text\<open>If Spy sees the Authentication Key sent in msg K2, then 1157 the Key has expired.\<close> 1158lemma Confidentiality_Kas_lemma [rule_format]: 1159 "\<lbrakk> authK \<in> symKeys; A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk> 1160 \<Longrightarrow> Says Kas A 1161 (Crypt (shrK A) 1162 \<lbrace>Key authK, Agent Tgs, Number Ta, 1163 Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>) 1164 \<in> set evs \<longrightarrow> 1165 Key authK \<in> analz (spies evs) \<longrightarrow> 1166 expiredAK Ta evs" 1167apply (erule kerbIV_gets.induct) 1168apply (frule_tac [11] Oops_range_spies2) 1169apply (frule_tac [10] Oops_range_spies1) 1170apply (frule_tac [8] Says_tgs_message_form) 1171apply (frule_tac [6] Says_kas_message_form) 1172apply (safe del: impI conjI impCE) 1173apply (simp_all (no_asm_simp) add: Says_Kas_message_form less_SucI analz_insert_eq not_parts_not_analz analz_insert_freshK1 pushes) 1174txt\<open>Fake\<close> 1175apply spy_analz 1176txt\<open>K2\<close> 1177apply blast 1178txt\<open>K4\<close> 1179apply blast 1180txt\<open>Level 8: K5\<close> 1181apply (blast dest: servK_notin_authKeysD Says_Kas_message_form intro: less_SucI) 1182txt\<open>Oops1\<close> 1183apply (blast dest!: unique_authKeys intro: less_SucI) 1184txt\<open>Oops2\<close> 1185by (blast dest: Says_Tgs_message_form Says_Kas_message_form) 1186 1187lemma Confidentiality_Kas: 1188 "\<lbrakk> Says Kas A 1189 (Crypt Ka \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>) 1190 \<in> set evs; 1191 \<not> expiredAK Ta evs; 1192 A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk> 1193 \<Longrightarrow> Key authK \<notin> analz (spies evs)" 1194by (blast dest: Says_Kas_message_form Confidentiality_Kas_lemma) 1195 1196text\<open>If Spy sees the Service Key sent in msg K4, then 1197 the Key has expired.\<close> 1198 1199lemma Confidentiality_lemma [rule_format]: 1200 "\<lbrakk> Says Tgs A 1201 (Crypt authK 1202 \<lbrace>Key servK, Agent B, Number Ts, 1203 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>) 1204 \<in> set evs; 1205 Key authK \<notin> analz (spies evs); 1206 servK \<in> symKeys; 1207 A \<notin> bad; B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk> 1208 \<Longrightarrow> Key servK \<in> analz (spies evs) \<longrightarrow> 1209 expiredSK Ts evs" 1210apply (erule rev_mp) 1211apply (erule rev_mp) 1212apply (erule kerbIV_gets.induct) 1213apply (rule_tac [10] impI)+ 1214 \<comment> \<open>The Oops1 case is unusual: must simplify 1215 \<^term>\<open>Authkey \<notin> analz (spies (ev#evs))\<close>, not letting 1216 \<open>analz_mono_contra\<close> weaken it to 1217 \<^term>\<open>Authkey \<notin> analz (spies evs)\<close>, 1218 for we then conclude \<^term>\<open>authK \<noteq> authKa\<close>.\<close> 1219apply analz_mono_contra 1220apply (frule_tac [11] Oops_range_spies2) 1221apply (frule_tac [10] Oops_range_spies1) 1222apply (frule_tac [8] Says_tgs_message_form) 1223apply (frule_tac [6] Says_kas_message_form) 1224apply (safe del: impI conjI impCE) 1225apply (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) 1226txt\<open>Fake\<close> 1227apply spy_analz 1228txt\<open>K2\<close> 1229apply (blast intro: parts_insertI less_SucI) 1230txt\<open>K4\<close> 1231apply (blast dest: authTicket_authentic Confidentiality_Kas) 1232txt\<open>Oops2\<close> 1233 prefer 3 1234 apply (blast dest: Says_imp_spies [THEN parts.Inj] Key_unique_SesKey intro: less_SucI) 1235txt\<open>Oops1\<close> 1236 prefer 2 1237apply (blast dest: Says_Kas_message_form Says_Tgs_message_form intro: less_SucI) 1238txt\<open>K5. Not clear how this step could be integrated with the main 1239 simplification step. Done in KerberosV.thy\<close> 1240apply clarify 1241apply (erule_tac V = "Says Aa Tgs X \<in> set evs" for X evs in thin_rl) 1242apply (frule Gets_imp_knows_Spy [THEN parts.Inj, THEN servK_notin_authKeysD]) 1243apply (assumption, assumption, blast, assumption) 1244apply (simp add: analz_insert_freshK2) 1245apply (blast dest: Key_unique_SesKey intro: less_SucI) 1246done 1247 1248 1249text\<open>In the real world Tgs can't check wheter authK is secure!\<close> 1250lemma Confidentiality_Tgs: 1251 "\<lbrakk> Says Tgs A 1252 (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 1253 \<in> set evs; 1254 Key authK \<notin> analz (spies evs); 1255 \<not> expiredSK Ts evs; 1256 A \<notin> bad; B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk> 1257 \<Longrightarrow> Key servK \<notin> analz (spies evs)" 1258by (blast dest: Says_Tgs_message_form Confidentiality_lemma) 1259 1260text\<open>In the real world Tgs CAN check what Kas sends!\<close> 1261lemma Confidentiality_Tgs_bis: 1262 "\<lbrakk> Says Kas A 1263 (Crypt Ka \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>) 1264 \<in> set evs; 1265 Says Tgs A 1266 (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 1267 \<in> set evs; 1268 \<not> expiredAK Ta evs; \<not> expiredSK Ts evs; 1269 A \<notin> bad; B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk> 1270 \<Longrightarrow> Key servK \<notin> analz (spies evs)" 1271by (blast dest!: Confidentiality_Kas Confidentiality_Tgs) 1272 1273text\<open>Most general form\<close> 1274lemmas Confidentiality_Tgs_ter = authTicket_authentic [THEN Confidentiality_Tgs_bis] 1275 1276lemmas Confidentiality_Auth_A = authK_authentic [THEN Confidentiality_Kas] 1277 1278text\<open>Needs a confidentiality guarantee, hence moved here. 1279 Authenticity of servK for A\<close> 1280lemma servK_authentic_bis_r: 1281 "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace> 1282 \<in> parts (spies evs); 1283 Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace> 1284 \<in> parts (spies evs); 1285 \<not> expiredAK Ta evs; A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk> 1286 \<Longrightarrow>Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 1287 \<in> set evs" 1288by (blast dest: authK_authentic Confidentiality_Auth_A servK_authentic_ter) 1289 1290lemma Confidentiality_Serv_A: 1291 "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace> 1292 \<in> parts (spies evs); 1293 Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace> 1294 \<in> parts (spies evs); 1295 \<not> expiredAK Ta evs; \<not> expiredSK Ts evs; 1296 A \<notin> bad; B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk> 1297 \<Longrightarrow> Key servK \<notin> analz (spies evs)" 1298by (metis Confidentiality_Auth_A Confidentiality_Tgs K4_imp_K2 authK_authentic authTicket_form servK_authentic unique_authKeys) 1299 1300(*deleted Confidentiality_B, which was identical to Confidentiality_Serv_A*) 1301 1302lemma u_Confidentiality_B: 1303 "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> 1304 \<in> parts (spies evs); 1305 \<not> expiredSK Ts evs; 1306 A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV_gets \<rbrakk> 1307 \<Longrightarrow> Key servK \<notin> analz (spies evs)" 1308by (blast dest: u_servTicket_authentic u_NotexpiredSK_NotexpiredAK Confidentiality_Tgs_bis) 1309 1310 1311 1312subsection\<open>2. Parties' strong authentication: 1313 non-injective agreement on the session key. The same guarantees also 1314 express key distribution, hence their names\<close> 1315 1316text\<open>Authentication here still is weak agreement - of B with A\<close> 1317lemma A_authenticates_B: 1318 "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs); 1319 Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace> 1320 \<in> parts (spies evs); 1321 Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace> 1322 \<in> parts (spies evs); 1323 Key authK \<notin> analz (spies evs); Key servK \<notin> analz (spies evs); 1324 A \<notin> bad; B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk> 1325 \<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> set evs" 1326by (blast dest: authK_authentic servK_authentic Says_Kas_message_form Key_unique_SesKey K4_imp_K2 intro: Says_K6) 1327 1328(*These two have never been proved, because never were they needed before!*) 1329lemma shrK_in_initState_Server[iff]: "Key (shrK A) \<in> initState Kas" 1330by (induct_tac "A", auto) 1331 1332lemma shrK_in_knows_Server [iff]: "Key (shrK A) \<in> knows Kas evs" 1333by (simp add: initState_subset_knows [THEN subsetD]) 1334(*Because of our simple model of Tgs, the equivalent for it required an axiom*) 1335 1336 1337lemma A_authenticates_and_keydist_to_Kas: 1338 "\<lbrakk> Gets A (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>) \<in> set evs; 1339 A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk> 1340 \<Longrightarrow> Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>) \<in> set evs 1341 \<and> Key authK \<in> analz(knows Kas evs)" 1342by (force dest!: authK_authentic Says_imp_knows [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst]) 1343 1344 1345lemma K3_imp_Gets_evs: 1346 "\<lbrakk> Says A Tgs \<lbrace>Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>, 1347 Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B\<rbrace> 1348 \<in> set evs; A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk> 1349 \<Longrightarrow> Gets A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, 1350 Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>) 1351 \<in> set evs" 1352apply (erule rev_mp) 1353apply (erule kerbIV_gets.induct) 1354apply auto 1355apply (blast dest: authTicket_form) 1356done 1357 1358lemma Tgs_authenticates_and_keydist_to_A: 1359 "\<lbrakk> Gets Tgs \<lbrace> 1360 Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>, 1361 Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B \<rbrace> \<in> set evs; 1362 Key authK \<notin> analz (spies evs); A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk> 1363 \<Longrightarrow> \<exists> B. Says A Tgs \<lbrace> 1364 Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>, 1365 Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B \<rbrace> \<in> set evs 1366 \<and> Key authK \<in> analz (knows A evs)" 1367apply (frule Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Fst], assumption) 1368apply (drule Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Snd, THEN parts.Fst], assumption) 1369apply (drule Tgs_authenticates_A, assumption+, simp) 1370apply (force dest!: K3_imp_Gets_evs Gets_imp_knows [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst]) 1371done 1372 1373lemma K4_imp_Gets: 1374 "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 1375 \<in> set evs; evs \<in> kerbIV_gets \<rbrakk> 1376 \<Longrightarrow> \<exists> Ta X. 1377 Gets Tgs \<lbrace>Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>, X\<rbrace> 1378 \<in> set evs" 1379apply (erule rev_mp) 1380apply (erule kerbIV_gets.induct) 1381apply auto 1382done 1383 1384lemma A_authenticates_and_keydist_to_Tgs: 1385 "\<lbrakk> Gets A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>) 1386 \<in> set evs; 1387 Gets A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 1388 \<in> set evs; 1389 Key authK \<notin> analz (spies evs); A \<notin> bad; 1390 evs \<in> kerbIV_gets \<rbrakk> 1391 \<Longrightarrow> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) 1392 \<in> set evs 1393 \<and> Key authK \<in> analz (knows Tgs evs) 1394 \<and> Key servK \<in> analz (knows Tgs evs)" 1395apply (drule Gets_imp_knows_Spy [THEN parts.Inj], assumption) 1396apply (drule Gets_imp_knows_Spy [THEN parts.Inj], assumption) 1397apply (frule authK_authentic, assumption+) 1398apply (drule servK_authentic_ter, assumption+) 1399apply (frule K4_imp_Gets, assumption, erule exE, erule exE) 1400apply (drule Gets_imp_knows [THEN analz.Inj, THEN analz.Fst, THEN analz.Decrypt, THEN analz.Snd, THEN analz.Snd, THEN analz.Fst], assumption, force) 1401apply (metis Says_imp_knows analz.Fst analz.Inj analz_symKeys_Decrypt authTicket_form) 1402done 1403 1404lemma K5_imp_Gets: 1405 "\<lbrakk> Says A B \<lbrace>servTicket, Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> \<in> set evs; 1406 A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk> 1407 \<Longrightarrow> \<exists> authK Ts authTicket T2. 1408 Gets A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) \<in> set evs 1409 \<and> Says A Tgs \<lbrace>authTicket, Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B\<rbrace> \<in> set evs" 1410apply (erule rev_mp) 1411apply (erule kerbIV_gets.induct) 1412apply auto 1413done 1414 1415lemma K3_imp_Gets: 1416 "\<lbrakk> Says A Tgs \<lbrace>authTicket, Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B\<rbrace> 1417 \<in> set evs; 1418 A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk> 1419 \<Longrightarrow> \<exists> Ta. Gets A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>) \<in> set evs" 1420apply (erule rev_mp) 1421apply (erule kerbIV_gets.induct) 1422apply auto 1423done 1424 1425lemma B_authenticates_and_keydist_to_A: 1426 "\<lbrakk> Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>, 1427 Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> \<in> set evs; 1428 Key servK \<notin> analz (spies evs); 1429 A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV_gets \<rbrakk> 1430 \<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>, 1431 Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> \<in> set evs 1432 \<and> Key servK \<in> analz (knows A evs)" 1433apply (frule Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Fst, THEN servTicket_authentic_Tgs], assumption+) 1434apply (drule Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Snd], assumption) 1435apply (erule exE, drule Says_K5, assumption+) 1436apply (frule K5_imp_Gets, assumption+) 1437apply clarify 1438apply (drule K3_imp_Gets, assumption+) 1439apply (erule exE) 1440apply (frule Gets_imp_knows_Spy [THEN parts.Inj, THEN authK_authentic, THEN Says_Kas_message_form], assumption+, clarify) 1441apply (force dest!: Gets_imp_knows [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst]) 1442done 1443 1444 1445lemma K6_imp_Gets: 1446 "\<lbrakk> Says B A (Crypt servK (Number T3)) \<in> set evs; 1447 B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk> 1448\<Longrightarrow> \<exists> Ts X. Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>,X\<rbrace> 1449 \<in> set evs" 1450apply (erule rev_mp) 1451apply (erule kerbIV_gets.induct) 1452apply auto 1453done 1454 1455 1456lemma A_authenticates_and_keydist_to_B: 1457 "\<lbrakk> Gets A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>, 1458 Crypt servK (Number T3)\<rbrace> \<in> set evs; 1459 Gets A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>) 1460 \<in> set evs; 1461 Key authK \<notin> analz (spies evs); Key servK \<notin> analz (spies evs); 1462 A \<notin> bad; B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk> 1463 \<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> set evs 1464 \<and> Key servK \<in> analz (knows B evs)" 1465apply (frule Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Fst], assumption) 1466apply (drule Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Snd], assumption) 1467apply (drule Gets_imp_knows_Spy [THEN parts.Inj], assumption) 1468apply (drule A_authenticates_B, assumption+) 1469apply (force dest!: K6_imp_Gets Gets_imp_knows [THEN analz.Inj, THEN analz.Fst, THEN analz.Decrypt, THEN analz.Snd, THEN analz.Snd, THEN analz.Fst]) 1470done 1471 1472end 1473 1474