1(* Title: HOL/Auth/Yahalom.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1996 University of Cambridge 4*) 5 6section\<open>The Yahalom Protocol\<close> 7 8theory Yahalom imports Public begin 9 10text\<open>From page 257 of 11 Burrows, Abadi and Needham (1989). A Logic of Authentication. 12 Proc. Royal Soc. 426 13 14This theory has the prototypical example of a secrecy relation, KeyCryptNonce. 15\<close> 16 17inductive_set yahalom :: "event list set" 18 where 19 (*Initial trace is empty*) 20 Nil: "[] \<in> yahalom" 21 22 (*The spy MAY say anything he CAN say. We do not expect him to 23 invent new nonces here, but he can also use NS1. Common to 24 all similar protocols.*) 25 | Fake: "\<lbrakk>evsf \<in> yahalom; X \<in> synth (analz (knows Spy evsf))\<rbrakk> 26 \<Longrightarrow> Says Spy B X # evsf \<in> yahalom" 27 28 (*A message that has been sent can be received by the 29 intended recipient.*) 30 | Reception: "\<lbrakk>evsr \<in> yahalom; Says A B X \<in> set evsr\<rbrakk> 31 \<Longrightarrow> Gets B X # evsr \<in> yahalom" 32 33 (*Alice initiates a protocol run*) 34 | YM1: "\<lbrakk>evs1 \<in> yahalom; Nonce NA \<notin> used evs1\<rbrakk> 35 \<Longrightarrow> Says A B \<lbrace>Agent A, Nonce NA\<rbrace> # evs1 \<in> yahalom" 36 37 (*Bob's response to Alice's message.*) 38 | YM2: "\<lbrakk>evs2 \<in> yahalom; Nonce NB \<notin> used evs2; 39 Gets B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs2\<rbrakk> 40 \<Longrightarrow> Says B Server 41 \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace> 42 # evs2 \<in> yahalom" 43 44 (*The Server receives Bob's message. He responds by sending a 45 new session key to Alice, with a packet for forwarding to Bob.*) 46 | YM3: "\<lbrakk>evs3 \<in> yahalom; Key KAB \<notin> used evs3; KAB \<in> symKeys; 47 Gets Server 48 \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace> 49 \<in> set evs3\<rbrakk> 50 \<Longrightarrow> Says Server A 51 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key KAB, Nonce NA, Nonce NB\<rbrace>, 52 Crypt (shrK B) \<lbrace>Agent A, Key KAB\<rbrace>\<rbrace> 53 # evs3 \<in> yahalom" 54 55 | YM4: 56 \<comment> \<open>Alice receives the Server's (?) message, checks her Nonce, and 57 uses the new session key to send Bob his Nonce. The premise 58 \<^term>\<open>A \<noteq> Server\<close> is needed for \<open>Says_Server_not_range\<close>. 59 Alice can check that K is symmetric by its length.\<close> 60 "\<lbrakk>evs4 \<in> yahalom; A \<noteq> Server; K \<in> symKeys; 61 Gets A \<lbrace>Crypt(shrK A) \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>, X\<rbrace> 62 \<in> set evs4; 63 Says A B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs4\<rbrakk> 64 \<Longrightarrow> Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> # evs4 \<in> yahalom" 65 66 (*This message models possible leaks of session keys. The Nonces 67 identify the protocol run. Quoting Server here ensures they are 68 correct.*) 69 | Oops: "\<lbrakk>evso \<in> yahalom; 70 Says Server A \<lbrace>Crypt (shrK A) 71 \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>, 72 X\<rbrace> \<in> set evso\<rbrakk> 73 \<Longrightarrow> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> yahalom" 74 75 76definition KeyWithNonce :: "[key, nat, event list] \<Rightarrow> bool" where 77 "KeyWithNonce K NB evs == 78 \<exists>A B na X. 79 Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, Nonce NB\<rbrace>, X\<rbrace> 80 \<in> set evs" 81 82 83declare Says_imp_analz_Spy [dest] 84declare parts.Body [dest] 85declare Fake_parts_insert_in_Un [dest] 86declare analz_into_parts [dest] 87 88text\<open>A "possibility property": there are traces that reach the end\<close> 89lemma "\<lbrakk>A \<noteq> Server; K \<in> symKeys; Key K \<notin> used []\<rbrakk> 90 \<Longrightarrow> \<exists>X NB. \<exists>evs \<in> yahalom. 91 Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs" 92apply (intro exI bexI) 93apply (rule_tac [2] yahalom.Nil 94 [THEN yahalom.YM1, THEN yahalom.Reception, 95 THEN yahalom.YM2, THEN yahalom.Reception, 96 THEN yahalom.YM3, THEN yahalom.Reception, 97 THEN yahalom.YM4]) 98apply (possibility, simp add: used_Cons) 99done 100 101 102subsection\<open>Regularity Lemmas for Yahalom\<close> 103 104lemma Gets_imp_Says: 105 "\<lbrakk>Gets B X \<in> set evs; evs \<in> yahalom\<rbrakk> \<Longrightarrow> \<exists>A. Says A B X \<in> set evs" 106by (erule rev_mp, erule yahalom.induct, auto) 107 108text\<open>Must be proved separately for each protocol\<close> 109lemma Gets_imp_knows_Spy: 110 "\<lbrakk>Gets B X \<in> set evs; evs \<in> yahalom\<rbrakk> \<Longrightarrow> X \<in> knows Spy evs" 111by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) 112 113lemmas Gets_imp_analz_Spy = Gets_imp_knows_Spy [THEN analz.Inj] 114declare Gets_imp_analz_Spy [dest] 115 116 117text\<open>Lets us treat YM4 using a similar argument as for the Fake case.\<close> 118lemma YM4_analz_knows_Spy: 119 "\<lbrakk>Gets A \<lbrace>Crypt (shrK A) Y, X\<rbrace> \<in> set evs; evs \<in> yahalom\<rbrakk> 120 \<Longrightarrow> X \<in> analz (knows Spy evs)" 121by blast 122 123lemmas YM4_parts_knows_Spy = 124 YM4_analz_knows_Spy [THEN analz_into_parts] 125 126text\<open>For Oops\<close> 127lemma YM4_Key_parts_knows_Spy: 128 "Says Server A \<lbrace>Crypt (shrK A) \<lbrace>B,K,NA,NB\<rbrace>, X\<rbrace> \<in> set evs 129 \<Longrightarrow> K \<in> parts (knows Spy evs)" 130 by (metis parts.Body parts.Fst parts.Snd Says_imp_knows_Spy parts.Inj) 131 132text\<open>Theorems of the form \<^term>\<open>X \<notin> parts (knows Spy evs)\<close> imply 133that NOBODY sends messages containing X!\<close> 134 135text\<open>Spy never sees a good agent's shared key!\<close> 136lemma Spy_see_shrK [simp]: 137 "evs \<in> yahalom \<Longrightarrow> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" 138by (erule yahalom.induct, force, 139 drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+) 140 141lemma Spy_analz_shrK [simp]: 142 "evs \<in> yahalom \<Longrightarrow> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)" 143by auto 144 145lemma Spy_see_shrK_D [dest!]: 146 "\<lbrakk>Key (shrK A) \<in> parts (knows Spy evs); evs \<in> yahalom\<rbrakk> \<Longrightarrow> A \<in> bad" 147by (blast dest: Spy_see_shrK) 148 149text\<open>Nobody can have used non-existent keys! 150 Needed to apply \<open>analz_insert_Key\<close>\<close> 151lemma new_keys_not_used [simp]: 152 "\<lbrakk>Key K \<notin> used evs; K \<in> symKeys; evs \<in> yahalom\<rbrakk> 153 \<Longrightarrow> K \<notin> keysFor (parts (spies evs))" 154apply (erule rev_mp) 155apply (erule yahalom.induct, force, 156 frule_tac [6] YM4_parts_knows_Spy, simp_all) 157txt\<open>Fake\<close> 158apply (force dest!: keysFor_parts_insert, auto) 159done 160 161 162text\<open>Earlier, all protocol proofs declared this theorem. 163 But only a few proofs need it, e.g. Yahalom and Kerberos IV.\<close> 164lemma new_keys_not_analzd: 165 "\<lbrakk>K \<in> symKeys; evs \<in> yahalom; Key K \<notin> used evs\<rbrakk> 166 \<Longrightarrow> K \<notin> keysFor (analz (knows Spy evs))" 167by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD]) 168 169 170text\<open>Describes the form of K when the Server sends this message. Useful for 171 Oops as well as main secrecy property.\<close> 172lemma Says_Server_not_range [simp]: 173 "\<lbrakk>Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, X\<rbrace> 174 \<in> set evs; evs \<in> yahalom\<rbrakk> 175 \<Longrightarrow> K \<notin> range shrK" 176by (erule rev_mp, erule yahalom.induct, simp_all) 177 178 179subsection\<open>Secrecy Theorems\<close> 180 181(**** 182 The following is to prove theorems of the form 183 184 Key K \<in> analz (insert (Key KAB) (knows Spy evs)) \<Longrightarrow> 185 Key K \<in> analz (knows Spy evs) 186 187 A more general formula must be proved inductively. 188****) 189 190text\<open>Session keys are not used to encrypt other session keys\<close> 191 192lemma analz_image_freshK [rule_format]: 193 "evs \<in> yahalom \<Longrightarrow> 194 \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow> 195 (Key K \<in> analz (Key`KK \<union> (knows Spy evs))) = 196 (K \<in> KK | Key K \<in> analz (knows Spy evs))" 197apply (erule yahalom.induct, 198 drule_tac [7] YM4_analz_knows_Spy, analz_freshK, spy_analz, blast) 199apply (simp only: Says_Server_not_range analz_image_freshK_simps) 200apply safe 201done 202 203lemma analz_insert_freshK: 204 "\<lbrakk>evs \<in> yahalom; KAB \<notin> range shrK\<rbrakk> \<Longrightarrow> 205 (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = 206 (K = KAB | Key K \<in> analz (knows Spy evs))" 207by (simp only: analz_image_freshK analz_image_freshK_simps) 208 209 210text\<open>The Key K uniquely identifies the Server's message.\<close> 211lemma unique_session_keys: 212 "\<lbrakk>Says Server A 213 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, X\<rbrace> \<in> set evs; 214 Says Server A' 215 \<lbrace>Crypt (shrK A') \<lbrace>Agent B', Key K, na', nb'\<rbrace>, X'\<rbrace> \<in> set evs; 216 evs \<in> yahalom\<rbrakk> 217 \<Longrightarrow> A=A' \<and> B=B' \<and> na=na' \<and> nb=nb'" 218apply (erule rev_mp, erule rev_mp) 219apply (erule yahalom.induct, simp_all) 220txt\<open>YM3, by freshness, and YM4\<close> 221apply blast+ 222done 223 224 225text\<open>Crucial secrecy property: Spy does not see the keys sent in msg YM3\<close> 226lemma secrecy_lemma: 227 "\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 228 \<Longrightarrow> Says Server A 229 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, 230 Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> 231 \<in> set evs \<longrightarrow> 232 Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs \<longrightarrow> 233 Key K \<notin> analz (knows Spy evs)" 234apply (erule yahalom.induct, force, 235 drule_tac [6] YM4_analz_knows_Spy) 236apply (simp_all add: pushes analz_insert_eq analz_insert_freshK) 237 subgoal \<comment> \<open>Fake\<close> by spy_analz 238 subgoal \<comment> \<open>YM3\<close> by blast 239 subgoal \<comment> \<open>Oops\<close> by (blast dest: unique_session_keys) 240done 241 242text\<open>Final version\<close> 243lemma Spy_not_see_encrypted_key: 244 "\<lbrakk>Says Server A 245 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, 246 Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> 247 \<in> set evs; 248 Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs; 249 A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 250 \<Longrightarrow> Key K \<notin> analz (knows Spy evs)" 251by (blast dest: secrecy_lemma) 252 253 254subsubsection\<open>Security Guarantee for A upon receiving YM3\<close> 255 256text\<open>If the encrypted message appears then it originated with the Server\<close> 257lemma A_trusts_YM3: 258 "\<lbrakk>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace> \<in> parts (knows Spy evs); 259 A \<notin> bad; evs \<in> yahalom\<rbrakk> 260 \<Longrightarrow> Says Server A 261 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, 262 Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> 263 \<in> set evs" 264apply (erule rev_mp) 265apply (erule yahalom.induct, force, 266 frule_tac [6] YM4_parts_knows_Spy, simp_all) 267txt\<open>Fake, YM3\<close> 268apply blast+ 269done 270 271text\<open>The obvious combination of \<open>A_trusts_YM3\<close> with 272 \<open>Spy_not_see_encrypted_key\<close>\<close> 273lemma A_gets_good_key: 274 "\<lbrakk>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace> \<in> parts (knows Spy evs); 275 Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs; 276 A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 277 \<Longrightarrow> Key K \<notin> analz (knows Spy evs)" 278 by (metis A_trusts_YM3 secrecy_lemma) 279 280 281subsubsection\<open>Security Guarantees for B upon receiving YM4\<close> 282 283text\<open>B knows, by the first part of A's message, that the Server distributed 284 the key for A and B. But this part says nothing about nonces.\<close> 285lemma B_trusts_YM4_shrK: 286 "\<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace> \<in> parts (knows Spy evs); 287 B \<notin> bad; evs \<in> yahalom\<rbrakk> 288 \<Longrightarrow> \<exists>NA NB. Says Server A 289 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, 290 Nonce NA, Nonce NB\<rbrace>, 291 Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> 292 \<in> set evs" 293apply (erule rev_mp) 294apply (erule yahalom.induct, force, 295 frule_tac [6] YM4_parts_knows_Spy, simp_all) 296txt\<open>Fake, YM3\<close> 297apply blast+ 298done 299 300text\<open>B knows, by the second part of A's message, that the Server 301 distributed the key quoting nonce NB. This part says nothing about 302 agent names. Secrecy of NB is crucial. Note that \<^term>\<open>Nonce NB 303 \<notin> analz(knows Spy evs)\<close> must be the FIRST antecedent of the 304 induction formula.\<close> 305 306lemma B_trusts_YM4_newK [rule_format]: 307 "\<lbrakk>Crypt K (Nonce NB) \<in> parts (knows Spy evs); 308 Nonce NB \<notin> analz (knows Spy evs); evs \<in> yahalom\<rbrakk> 309 \<Longrightarrow> \<exists>A B NA. Says Server A 310 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>, 311 Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> 312 \<in> set evs" 313apply (erule rev_mp, erule rev_mp) 314apply (erule yahalom.induct, force, 315 frule_tac [6] YM4_parts_knows_Spy) 316 apply (analz_mono_contra, simp_all) 317 subgoal \<comment> \<open>Fake\<close> by blast 318 subgoal \<comment> \<open>YM3\<close> by blast 319txt\<open>YM4. A is uncompromised because NB is secure 320 A's certificate guarantees the existence of the Server message\<close> 321apply (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad 322 dest: Says_imp_spies 323 parts.Inj [THEN parts.Fst, THEN A_trusts_YM3]) 324done 325 326 327subsubsection\<open>Towards proving secrecy of Nonce NB\<close> 328 329text\<open>Lemmas about the predicate KeyWithNonce\<close> 330 331lemma KeyWithNonceI: 332 "Says Server A 333 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, Nonce NB\<rbrace>, X\<rbrace> 334 \<in> set evs \<Longrightarrow> KeyWithNonce K NB evs" 335by (unfold KeyWithNonce_def, blast) 336 337lemma KeyWithNonce_Says [simp]: 338 "KeyWithNonce K NB (Says S A X # evs) = 339 (Server = S \<and> 340 (\<exists>B n X'. X = \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, n, Nonce NB\<rbrace>, X'\<rbrace>) 341 | KeyWithNonce K NB evs)" 342by (simp add: KeyWithNonce_def, blast) 343 344 345lemma KeyWithNonce_Notes [simp]: 346 "KeyWithNonce K NB (Notes A X # evs) = KeyWithNonce K NB evs" 347by (simp add: KeyWithNonce_def) 348 349lemma KeyWithNonce_Gets [simp]: 350 "KeyWithNonce K NB (Gets A X # evs) = KeyWithNonce K NB evs" 351by (simp add: KeyWithNonce_def) 352 353text\<open>A fresh key cannot be associated with any nonce 354 (with respect to a given trace).\<close> 355lemma fresh_not_KeyWithNonce: 356 "Key K \<notin> used evs \<Longrightarrow> \<not> KeyWithNonce K NB evs" 357by (unfold KeyWithNonce_def, blast) 358 359text\<open>The Server message associates K with NB' and therefore not with any 360 other nonce NB.\<close> 361lemma Says_Server_KeyWithNonce: 362 "\<lbrakk>Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, Nonce NB'\<rbrace>, X\<rbrace> 363 \<in> set evs; 364 NB \<noteq> NB'; evs \<in> yahalom\<rbrakk> 365 \<Longrightarrow> \<not> KeyWithNonce K NB evs" 366by (unfold KeyWithNonce_def, blast dest: unique_session_keys) 367 368 369text\<open>The only nonces that can be found with the help of session keys are 370 those distributed as nonce NB by the Server. The form of the theorem 371 recalls \<open>analz_image_freshK\<close>, but it is much more complicated.\<close> 372 373 374text\<open>As with \<open>analz_image_freshK\<close>, we take some pains to express the 375 property as a logical equivalence so that the simplifier can apply it.\<close> 376lemma Nonce_secrecy_lemma: 377 "P \<longrightarrow> (X \<in> analz (G \<union> H)) \<longrightarrow> (X \<in> analz H) \<Longrightarrow> 378 P \<longrightarrow> (X \<in> analz (G \<union> H)) = (X \<in> analz H)" 379by (blast intro: analz_mono [THEN subsetD]) 380 381lemma Nonce_secrecy: 382 "evs \<in> yahalom \<Longrightarrow> 383 (\<forall>KK. KK \<subseteq> - (range shrK) \<longrightarrow> 384 (\<forall>K \<in> KK. K \<in> symKeys \<longrightarrow> \<not> KeyWithNonce K NB evs) \<longrightarrow> 385 (Nonce NB \<in> analz (Key`KK \<union> (knows Spy evs))) = 386 (Nonce NB \<in> analz (knows Spy evs)))" 387apply (erule yahalom.induct, 388 frule_tac [7] YM4_analz_knows_Spy) 389apply (safe del: allI impI intro!: Nonce_secrecy_lemma [THEN impI, THEN allI]) 390apply (simp_all del: image_insert image_Un 391 add: analz_image_freshK_simps split_ifs 392 all_conj_distrib ball_conj_distrib 393 analz_image_freshK fresh_not_KeyWithNonce 394 imp_disj_not1 (*Moves NBa\<noteq>NB to the front*) 395 Says_Server_KeyWithNonce) 396txt\<open>For Oops, simplification proves \<^prop>\<open>NBa\<noteq>NB\<close>. By 397 \<^term>\<open>Says_Server_KeyWithNonce\<close>, we get \<^prop>\<open>\<not> KeyWithNonce K NB 398 evs\<close>; then simplification can apply the induction hypothesis with 399 \<^term>\<open>KK = {K}\<close>.\<close> 400 subgoal \<comment> \<open>Fake\<close> by spy_analz 401 subgoal \<comment> \<open>YM2\<close> by blast 402 subgoal \<comment> \<open>YM3\<close> by blast 403 subgoal \<comment> \<open>YM4: If \<^prop>\<open>A \<in> bad\<close> then \<^term>\<open>NBa\<close> is known, therefore \<^prop>\<open>NBa \<noteq> NB\<close>.\<close> 404 by (metis A_trusts_YM3 Gets_imp_analz_Spy Gets_imp_knows_Spy KeyWithNonce_def 405 Spy_analz_shrK analz.Fst analz.Snd analz_shrK_Decrypt parts.Fst parts.Inj) 406done 407 408 409text\<open>Version required below: if NB can be decrypted using a session key then 410 it was distributed with that key. The more general form above is required 411 for the induction to carry through.\<close> 412lemma single_Nonce_secrecy: 413 "\<lbrakk>Says Server A 414 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key KAB, na, Nonce NB'\<rbrace>, X\<rbrace> 415 \<in> set evs; 416 NB \<noteq> NB'; KAB \<notin> range shrK; evs \<in> yahalom\<rbrakk> 417 \<Longrightarrow> (Nonce NB \<in> analz (insert (Key KAB) (knows Spy evs))) = 418 (Nonce NB \<in> analz (knows Spy evs))" 419by (simp_all del: image_insert image_Un imp_disjL 420 add: analz_image_freshK_simps split_ifs 421 Nonce_secrecy Says_Server_KeyWithNonce) 422 423 424subsubsection\<open>The Nonce NB uniquely identifies B's message.\<close> 425 426lemma unique_NB: 427 "\<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace> \<in> parts (knows Spy evs); 428 Crypt (shrK B') \<lbrace>Agent A', Nonce NA', nb\<rbrace> \<in> parts (knows Spy evs); 429 evs \<in> yahalom; B \<notin> bad; B' \<notin> bad\<rbrakk> 430 \<Longrightarrow> NA' = NA \<and> A' = A \<and> B' = B" 431apply (erule rev_mp, erule rev_mp) 432apply (erule yahalom.induct, force, 433 frule_tac [6] YM4_parts_knows_Spy, simp_all) 434txt\<open>Fake, and YM2 by freshness\<close> 435apply blast+ 436done 437 438 439text\<open>Variant useful for proving secrecy of NB. Because nb is assumed to be 440 secret, we no longer must assume B, B' not bad.\<close> 441lemma Says_unique_NB: 442 "\<lbrakk>Says C S \<lbrace>X, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace> 443 \<in> set evs; 444 Gets S' \<lbrace>X', Crypt (shrK B') \<lbrace>Agent A', Nonce NA', nb\<rbrace>\<rbrace> 445 \<in> set evs; 446 nb \<notin> analz (knows Spy evs); evs \<in> yahalom\<rbrakk> 447 \<Longrightarrow> NA' = NA \<and> A' = A \<and> B' = B" 448by (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad 449 dest: Says_imp_spies unique_NB parts.Inj analz.Inj) 450 451 452subsubsection\<open>A nonce value is never used both as NA and as NB\<close> 453 454lemma no_nonce_YM1_YM2: 455 "\<lbrakk>Crypt (shrK B') \<lbrace>Agent A', Nonce NB, nb'\<rbrace> \<in> parts(knows Spy evs); 456 Nonce NB \<notin> analz (knows Spy evs); evs \<in> yahalom\<rbrakk> 457 \<Longrightarrow> Crypt (shrK B) \<lbrace>Agent A, na, Nonce NB\<rbrace> \<notin> parts(knows Spy evs)" 458apply (erule rev_mp, erule rev_mp) 459apply (erule yahalom.induct, force, 460 frule_tac [6] YM4_parts_knows_Spy) 461apply (analz_mono_contra, simp_all) 462txt\<open>Fake, YM2\<close> 463apply blast+ 464done 465 466text\<open>The Server sends YM3 only in response to YM2.\<close> 467lemma Says_Server_imp_YM2: 468 "\<lbrakk>Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, k, na, nb\<rbrace>, X\<rbrace> \<in> set evs; 469 evs \<in> yahalom\<rbrakk> 470 \<Longrightarrow> Gets Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, na, nb\<rbrace>\<rbrace> 471 \<in> set evs" 472by (erule rev_mp, erule yahalom.induct, auto) 473 474text\<open>A vital theorem for B, that nonce NB remains secure from the Spy.\<close> 475theorem Spy_not_see_NB : 476 "\<lbrakk>Says B Server 477 \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace> 478 \<in> set evs; 479 (\<forall>k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs); 480 A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 481 \<Longrightarrow> Nonce NB \<notin> analz (knows Spy evs)" 482apply (erule rev_mp, erule rev_mp) 483apply (erule yahalom.induct, force, 484 frule_tac [6] YM4_analz_knows_Spy) 485apply (simp_all add: split_ifs pushes new_keys_not_analzd analz_insert_eq 486 analz_insert_freshK) 487 subgoal \<comment> \<open>Fake\<close> by spy_analz 488 subgoal \<comment> \<open>YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!\<close> by blast 489 subgoal \<comment> \<open>YM2\<close> by blast 490 subgoal \<comment> \<open>YM3: because no NB can also be an NA\<close> 491 by (blast dest!: no_nonce_YM1_YM2 dest: Gets_imp_Says Says_unique_NB) 492 subgoal \<comment> \<open>YM4: key K is visible to Spy, contradicting session key secrecy theorem\<close> 493 \<comment> \<open>Case analysis on whether Aa is bad; 494 use \<open>Says_unique_NB\<close> to identify message components: \<^term>\<open>Aa=A\<close>, \<^term>\<open>Ba=B\<close>\<close> 495 apply clarify 496 apply (blast dest!: Says_unique_NB analz_shrK_Decrypt 497 parts.Inj [THEN parts.Fst, THEN A_trusts_YM3] 498 dest: Gets_imp_Says Says_imp_spies Says_Server_imp_YM2 499 Spy_not_see_encrypted_key) 500 done 501 subgoal \<comment> \<open>Oops case: if the nonce is betrayed now, show that the Oops event is 502 covered by the quantified Oops assumption.\<close> 503 apply clarsimp 504 apply (metis Says_Server_imp_YM2 Gets_imp_Says Says_Server_not_range Says_unique_NB no_nonce_YM1_YM2 parts.Snd single_Nonce_secrecy spies_partsEs(1)) 505 done 506done 507 508text\<open>B's session key guarantee from YM4. The two certificates contribute to a 509 single conclusion about the Server's message. Note that the "Notes Spy" 510 assumption must quantify over \<open>\<forall>\<close> POSSIBLE keys instead of our particular K. 511 If this run is broken and the spy substitutes a certificate containing an 512 old key, B has no means of telling.\<close> 513lemma B_trusts_YM4: 514 "\<lbrakk>Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>, 515 Crypt K (Nonce NB)\<rbrace> \<in> set evs; 516 Says B Server 517 \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace> 518 \<in> set evs; 519 \<forall>k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs; 520 A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 521 \<Longrightarrow> Says Server A 522 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, 523 Nonce NA, Nonce NB\<rbrace>, 524 Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> 525 \<in> set evs" 526by (blast dest: Spy_not_see_NB Says_unique_NB 527 Says_Server_imp_YM2 B_trusts_YM4_newK) 528 529 530 531text\<open>The obvious combination of \<open>B_trusts_YM4\<close> with 532 \<open>Spy_not_see_encrypted_key\<close>\<close> 533lemma B_gets_good_key: 534 "\<lbrakk>Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>, 535 Crypt K (Nonce NB)\<rbrace> \<in> set evs; 536 Says B Server 537 \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace> 538 \<in> set evs; 539 \<forall>k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs; 540 A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 541 \<Longrightarrow> Key K \<notin> analz (knows Spy evs)" 542 by (metis B_trusts_YM4 Spy_not_see_encrypted_key) 543 544 545subsection\<open>Authenticating B to A\<close> 546 547text\<open>The encryption in message YM2 tells us it cannot be faked.\<close> 548lemma B_Said_YM2 [rule_format]: 549 "\<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace> \<in> parts (knows Spy evs); 550 evs \<in> yahalom\<rbrakk> 551 \<Longrightarrow> B \<notin> bad \<longrightarrow> 552 Says B Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace> 553 \<in> set evs" 554apply (erule rev_mp, erule yahalom.induct, force, 555 frule_tac [6] YM4_parts_knows_Spy, simp_all) 556txt\<open>Fake\<close> 557apply blast 558done 559 560text\<open>If the server sends YM3 then B sent YM2\<close> 561lemma YM3_auth_B_to_A_lemma: 562 "\<lbrakk>Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA, nb\<rbrace>, X\<rbrace> 563 \<in> set evs; evs \<in> yahalom\<rbrakk> 564 \<Longrightarrow> B \<notin> bad \<longrightarrow> 565 Says B Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace> 566 \<in> set evs" 567apply (erule rev_mp, erule yahalom.induct, simp_all) 568txt\<open>YM3, YM4\<close> 569apply (blast dest!: B_Said_YM2)+ 570done 571 572text\<open>If A receives YM3 then B has used nonce NA (and therefore is alive)\<close> 573theorem YM3_auth_B_to_A: 574 "\<lbrakk>Gets A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA, nb\<rbrace>, X\<rbrace> 575 \<in> set evs; 576 A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 577 \<Longrightarrow> Says B Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace> 578 \<in> set evs" 579 by (metis A_trusts_YM3 Gets_imp_analz_Spy YM3_auth_B_to_A_lemma analz.Fst 580 not_parts_not_analz) 581 582 583subsection\<open>Authenticating A to B using the certificate 584 \<^term>\<open>Crypt K (Nonce NB)\<close>\<close> 585 586text\<open>Assuming the session key is secure, if both certificates are present then 587 A has said NB. We can't be sure about the rest of A's message, but only 588 NB matters for freshness.\<close> 589theorem A_Said_YM3_lemma [rule_format]: 590 "evs \<in> yahalom 591 \<Longrightarrow> Key K \<notin> analz (knows Spy evs) \<longrightarrow> 592 Crypt K (Nonce NB) \<in> parts (knows Spy evs) \<longrightarrow> 593 Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace> \<in> parts (knows Spy evs) \<longrightarrow> 594 B \<notin> bad \<longrightarrow> 595 (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs)" 596apply (erule yahalom.induct, force, 597 frule_tac [6] YM4_parts_knows_Spy) 598apply (analz_mono_contra, simp_all) 599 subgoal \<comment> \<open>Fake\<close> by blast 600 subgoal \<comment> \<open>YM3 because the message \<^term>\<open>Crypt K (Nonce NB)\<close> could not exist\<close> 601 by (force dest!: Crypt_imp_keysFor) 602 subgoal \<comment> \<open>YM4: was \<^term>\<open>Crypt K (Nonce NB)\<close> the very last message? If not, use the induction hypothesis, 603 otherwise by unicity of session keys\<close> 604 by (blast dest!: Gets_imp_Says A_trusts_YM3 B_trusts_YM4_shrK Crypt_Spy_analz_bad 605 dest: Says_imp_knows_Spy [THEN parts.Inj] unique_session_keys) 606done 607 608text\<open>If B receives YM4 then A has used nonce NB (and therefore is alive). 609 Moreover, A associates K with NB (thus is talking about the same run). 610 Other premises guarantee secrecy of K.\<close> 611theorem YM4_imp_A_Said_YM3 [rule_format]: 612 "\<lbrakk>Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>, 613 Crypt K (Nonce NB)\<rbrace> \<in> set evs; 614 Says B Server 615 \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace> 616 \<in> set evs; 617 (\<forall>NA k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs); 618 A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 619 \<Longrightarrow> \<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs" 620by (metis A_Said_YM3_lemma B_gets_good_key Gets_imp_analz_Spy YM4_parts_knows_Spy analz.Fst not_parts_not_analz) 621 622end 623