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