1(* Title: HOL/Auth/Yahalom2.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1996 University of Cambridge 4*) 5 6section\<open>The Yahalom Protocol, Variant 2\<close> 7 8theory Yahalom2 imports Public begin 9 10text\<open> 11This version trades encryption of NB for additional explicitness in YM3. 12Also in YM3, care is taken to make the two certificates distinct. 13 14From page 259 of 15 Burrows, Abadi and Needham (1989). A Logic of Authentication. 16 Proc. Royal Soc. 426 17 18This theory has the prototypical example of a secrecy relation, KeyCryptNonce. 19\<close> 20 21inductive_set yahalom :: "event list set" 22 where 23 (*Initial trace is empty*) 24 Nil: "[] \<in> yahalom" 25 26 (*The spy MAY say anything he CAN say. We do not expect him to 27 invent new nonces here, but he can also use NS1. Common to 28 all similar protocols.*) 29 | Fake: "\<lbrakk>evsf \<in> yahalom; X \<in> synth (analz (knows Spy evsf))\<rbrakk> 30 \<Longrightarrow> Says Spy B X # evsf \<in> yahalom" 31 32 (*A message that has been sent can be received by the 33 intended recipient.*) 34 | Reception: "\<lbrakk>evsr \<in> yahalom; Says A B X \<in> set evsr\<rbrakk> 35 \<Longrightarrow> Gets B X # evsr \<in> yahalom" 36 37 (*Alice initiates a protocol run*) 38 | YM1: "\<lbrakk>evs1 \<in> yahalom; Nonce NA \<notin> used evs1\<rbrakk> 39 \<Longrightarrow> Says A B \<lbrace>Agent A, Nonce NA\<rbrace> # evs1 \<in> yahalom" 40 41 (*Bob's response to Alice's message.*) 42 | YM2: "\<lbrakk>evs2 \<in> yahalom; Nonce NB \<notin> used evs2; 43 Gets B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs2\<rbrakk> 44 \<Longrightarrow> Says B Server 45 \<lbrace>Agent B, Nonce NB, Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace> 46 # evs2 \<in> yahalom" 47 48 (*The Server receives Bob's message. He responds by sending a 49 new session key to Alice, with a certificate for forwarding to Bob. 50 Both agents are quoted in the 2nd certificate to prevent attacks!*) 51 | YM3: "\<lbrakk>evs3 \<in> yahalom; Key KAB \<notin> used evs3; 52 Gets Server \<lbrace>Agent B, Nonce NB, 53 Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace> 54 \<in> set evs3\<rbrakk> 55 \<Longrightarrow> Says Server A 56 \<lbrace>Nonce NB, 57 Crypt (shrK A) \<lbrace>Agent B, Key KAB, Nonce NA\<rbrace>, 58 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key KAB, Nonce NB\<rbrace>\<rbrace> 59 # evs3 \<in> yahalom" 60 61 (*Alice receives the Server's (?) message, checks her Nonce, and 62 uses the new session key to send Bob his Nonce.*) 63 | YM4: "\<lbrakk>evs4 \<in> yahalom; 64 Gets A \<lbrace>Nonce NB, Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA\<rbrace>, 65 X\<rbrace> \<in> set evs4; 66 Says A B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs4\<rbrakk> 67 \<Longrightarrow> Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> # evs4 \<in> yahalom" 68 69 (*This message models possible leaks of session keys. The nonces 70 identify the protocol run. Quoting Server here ensures they are 71 correct. *) 72 | Oops: "\<lbrakk>evso \<in> yahalom; 73 Says Server A \<lbrace>Nonce NB, 74 Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA\<rbrace>, 75 X\<rbrace> \<in> set evso\<rbrakk> 76 \<Longrightarrow> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> yahalom" 77 78 79declare Says_imp_knows_Spy [THEN analz.Inj, dest] 80declare parts.Body [dest] 81declare Fake_parts_insert_in_Un [dest] 82declare analz_into_parts [dest] 83 84text\<open>A "possibility property": there are traces that reach the end\<close> 85lemma "Key K \<notin> used [] 86 \<Longrightarrow> \<exists>X NB. \<exists>evs \<in> yahalom. 87 Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs" 88apply (intro exI bexI) 89apply (rule_tac [2] yahalom.Nil 90 [THEN yahalom.YM1, THEN yahalom.Reception, 91 THEN yahalom.YM2, THEN yahalom.Reception, 92 THEN yahalom.YM3, THEN yahalom.Reception, 93 THEN yahalom.YM4]) 94apply (possibility, simp add: used_Cons) 95done 96 97lemma Gets_imp_Says: 98 "\<lbrakk>Gets B X \<in> set evs; evs \<in> yahalom\<rbrakk> \<Longrightarrow> \<exists>A. Says A B X \<in> set evs" 99by (erule rev_mp, erule yahalom.induct, auto) 100 101text\<open>Must be proved separately for each protocol\<close> 102lemma Gets_imp_knows_Spy: 103 "\<lbrakk>Gets B X \<in> set evs; evs \<in> yahalom\<rbrakk> \<Longrightarrow> X \<in> knows Spy evs" 104by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) 105 106declare Gets_imp_knows_Spy [THEN analz.Inj, dest] 107 108 109subsection\<open>Inductive Proofs\<close> 110 111text\<open>Result for reasoning about the encrypted portion of messages. 112Lets us treat YM4 using a similar argument as for the Fake case.\<close> 113lemma YM4_analz_knows_Spy: 114 "\<lbrakk>Gets A \<lbrace>NB, Crypt (shrK A) Y, X\<rbrace> \<in> set evs; evs \<in> yahalom\<rbrakk> 115 \<Longrightarrow> X \<in> analz (knows Spy evs)" 116by blast 117 118lemmas YM4_parts_knows_Spy = 119 YM4_analz_knows_Spy [THEN analz_into_parts] 120 121 122(** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY 123 sends messages containing X! **) 124 125text\<open>Spy never sees a good agent's shared key!\<close> 126lemma Spy_see_shrK [simp]: 127 "evs \<in> yahalom \<Longrightarrow> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" 128by (erule yahalom.induct, force, 129 drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+) 130 131lemma Spy_analz_shrK [simp]: 132 "evs \<in> yahalom \<Longrightarrow> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)" 133by auto 134 135lemma Spy_see_shrK_D [dest!]: 136 "\<lbrakk>Key (shrK A) \<in> parts (knows Spy evs); evs \<in> yahalom\<rbrakk> \<Longrightarrow> A \<in> bad" 137by (blast dest: Spy_see_shrK) 138 139text\<open>Nobody can have used non-existent keys! 140 Needed to apply \<open>analz_insert_Key\<close>\<close> 141lemma new_keys_not_used [simp]: 142 "\<lbrakk>Key K \<notin> used evs; K \<in> symKeys; evs \<in> yahalom\<rbrakk> 143 \<Longrightarrow> K \<notin> keysFor (parts (spies evs))" 144apply (erule rev_mp) 145apply (erule yahalom.induct, force, 146 frule_tac [6] YM4_parts_knows_Spy, simp_all) 147subgoal \<comment> \<open>Fake\<close> by (force dest!: keysFor_parts_insert) 148subgoal \<comment> \<open>YM3\<close>by blast 149subgoal \<comment> \<open>YM4\<close> by (fastforce dest!: Gets_imp_knows_Spy [THEN parts.Inj]) 150done 151 152 153text\<open>Describes the form of K when the Server sends this message. Useful for 154 Oops as well as main secrecy property.\<close> 155lemma Says_Server_message_form: 156 "\<lbrakk>Says Server A \<lbrace>nb', Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace>, X\<rbrace> 157 \<in> set evs; evs \<in> yahalom\<rbrakk> 158 \<Longrightarrow> K \<notin> range shrK" 159by (erule rev_mp, erule yahalom.induct, simp_all) 160 161 162(**** 163 The following is to prove theorems of the form 164 165 Key K \<in> analz (insert (Key KAB) (knows Spy evs)) \<Longrightarrow> 166 Key K \<in> analz (knows Spy evs) 167 168 A more general formula must be proved inductively. 169****) 170 171(** Session keys are not used to encrypt other session keys **) 172 173lemma analz_image_freshK [rule_format]: 174 "evs \<in> yahalom \<Longrightarrow> 175 \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow> 176 (Key K \<in> analz (Key`KK \<union> (knows Spy evs))) = 177 (K \<in> KK | Key K \<in> analz (knows Spy evs))" 178apply (erule yahalom.induct) 179apply (frule_tac [8] Says_Server_message_form) 180apply (drule_tac [7] YM4_analz_knows_Spy, analz_freshK, spy_analz, blast) 181done 182 183lemma analz_insert_freshK: 184 "\<lbrakk>evs \<in> yahalom; KAB \<notin> range shrK\<rbrakk> \<Longrightarrow> 185 (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = 186 (K = KAB | Key K \<in> analz (knows Spy evs))" 187by (simp only: analz_image_freshK analz_image_freshK_simps) 188 189 190text\<open>The Key K uniquely identifies the Server's message\<close> 191lemma unique_session_keys: 192 "\<lbrakk>Says Server A 193 \<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace>, X\<rbrace> \<in> set evs; 194 Says Server A' 195 \<lbrace>nb', Crypt (shrK A') \<lbrace>Agent B', Key K, na'\<rbrace>, X'\<rbrace> \<in> set evs; 196 evs \<in> yahalom\<rbrakk> 197 \<Longrightarrow> A=A' \<and> B=B' \<and> na=na' \<and> nb=nb'" 198apply (erule rev_mp, erule rev_mp) 199apply (erule yahalom.induct, simp_all) 200txt\<open>YM3, by freshness\<close> 201apply blast 202done 203 204 205subsection\<open>Crucial Secrecy Property: Spy Does Not See Key \<^term>\<open>KAB\<close>\<close> 206 207lemma secrecy_lemma: 208 "\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 209 \<Longrightarrow> Says Server A 210 \<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace>, 211 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, nb\<rbrace>\<rbrace> 212 \<in> set evs \<longrightarrow> 213 Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs \<longrightarrow> 214 Key K \<notin> analz (knows Spy evs)" 215apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form, 216 drule_tac [6] YM4_analz_knows_Spy) 217apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz) 218apply (blast dest: unique_session_keys)+ (*YM3, Oops*) 219done 220 221 222text\<open>Final version\<close> 223lemma Spy_not_see_encrypted_key: 224 "\<lbrakk>Says Server A 225 \<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace>, 226 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, nb\<rbrace>\<rbrace> 227 \<in> set evs; 228 Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs; 229 A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 230 \<Longrightarrow> Key K \<notin> analz (knows Spy evs)" 231by (blast dest: secrecy_lemma Says_Server_message_form) 232 233 234 235text\<open>This form is an immediate consequence of the previous result. It is 236similar to the assertions established by other methods. It is equivalent 237to the previous result in that the Spy already has \<^term>\<open>analz\<close> and 238\<^term>\<open>synth\<close> at his disposal. However, the conclusion 239\<^term>\<open>Key K \<notin> knows Spy evs\<close> appears not to be inductive: all the cases 240other than Fake are trivial, while Fake requires 241\<^term>\<open>Key K \<notin> analz (knows Spy evs)\<close>.\<close> 242lemma Spy_not_know_encrypted_key: 243 "\<lbrakk>Says Server A 244 \<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace>, 245 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, nb\<rbrace>\<rbrace> 246 \<in> set evs; 247 Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs; 248 A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 249 \<Longrightarrow> Key K \<notin> knows Spy evs" 250by (blast dest: Spy_not_see_encrypted_key) 251 252 253subsection\<open>Security Guarantee for A upon receiving YM3\<close> 254 255text\<open>If the encrypted message appears then it originated with the Server. 256 May now apply \<open>Spy_not_see_encrypted_key\<close>, subject to its conditions.\<close> 257lemma A_trusts_YM3: 258 "\<lbrakk>Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace> \<in> parts (knows Spy evs); 259 A \<notin> bad; evs \<in> yahalom\<rbrakk> 260 \<Longrightarrow> \<exists>nb. Says Server A 261 \<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace>, 262 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, nb\<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> 273theorem A_gets_good_key: 274 "\<lbrakk>Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace> \<in> parts (knows Spy evs); 275 \<forall>nb. 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)" 278by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key) 279 280 281subsection\<open>Security Guarantee 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, and has associated it with NB.\<close> 285lemma B_trusts_YM4_shrK: 286 "\<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> 287 \<in> parts (knows Spy evs); 288 B \<notin> bad; evs \<in> yahalom\<rbrakk> 289 \<Longrightarrow> \<exists>NA. Says Server A 290 \<lbrace>Nonce NB, 291 Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA\<rbrace>, 292 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace>\<rbrace> 293 \<in> set evs" 294apply (erule rev_mp) 295apply (erule yahalom.induct, force, 296 frule_tac [6] YM4_parts_knows_Spy, simp_all) 297txt\<open>Fake, YM3\<close> 298apply blast+ 299done 300 301 302text\<open>With this protocol variant, we don't need the 2nd part of YM4 at all: 303 Nonce NB is available in the first part.\<close> 304 305text\<open>What can B deduce from receipt of YM4? Stronger and simpler than Yahalom 306 because we do not have to show that NB is secret.\<close> 307lemma B_trusts_YM4: 308 "\<lbrakk>Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace>, X\<rbrace> 309 \<in> set evs; 310 A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 311 \<Longrightarrow> \<exists>NA. Says Server A 312 \<lbrace>Nonce NB, 313 Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA\<rbrace>, 314 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace>\<rbrace> 315 \<in> set evs" 316by (blast dest!: B_trusts_YM4_shrK) 317 318 319text\<open>The obvious combination of \<open>B_trusts_YM4\<close> with 320\<open>Spy_not_see_encrypted_key\<close>\<close> 321theorem B_gets_good_key: 322 "\<lbrakk>Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace>, X\<rbrace> 323 \<in> set evs; 324 \<forall>na. Notes Spy \<lbrace>na, Nonce NB, Key K\<rbrace> \<notin> set evs; 325 A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 326 \<Longrightarrow> Key K \<notin> analz (knows Spy evs)" 327by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key) 328 329 330subsection\<open>Authenticating B to A\<close> 331 332text\<open>The encryption in message YM2 tells us it cannot be faked.\<close> 333lemma B_Said_YM2: 334 "\<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace> \<in> parts (knows Spy evs); 335 B \<notin> bad; evs \<in> yahalom\<rbrakk> 336 \<Longrightarrow> \<exists>NB. Says B Server \<lbrace>Agent B, Nonce NB, 337 Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace> 338 \<in> set evs" 339apply (erule rev_mp) 340apply (erule yahalom.induct, force, 341 frule_tac [6] YM4_parts_knows_Spy, simp_all) 342txt\<open>Fake, YM2\<close> 343apply blast+ 344done 345 346 347text\<open>If the server sends YM3 then B sent YM2, perhaps with a different NB\<close> 348lemma YM3_auth_B_to_A_lemma: 349 "\<lbrakk>Says Server A \<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA\<rbrace>, X\<rbrace> 350 \<in> set evs; 351 B \<notin> bad; evs \<in> yahalom\<rbrakk> 352 \<Longrightarrow> \<exists>nb'. Says B Server \<lbrace>Agent B, nb', 353 Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace> 354 \<in> set evs" 355apply (erule rev_mp) 356apply (erule yahalom.induct, simp_all) 357txt\<open>Fake, YM2, YM3\<close> 358apply (blast dest!: B_Said_YM2)+ 359done 360 361text\<open>If A receives YM3 then B has used nonce NA (and therefore is alive)\<close> 362theorem YM3_auth_B_to_A: 363 "\<lbrakk>Gets A \<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA\<rbrace>, X\<rbrace> 364 \<in> set evs; 365 A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 366 \<Longrightarrow> \<exists>nb'. Says B Server 367 \<lbrace>Agent B, nb', Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace> 368 \<in> set evs" 369by (blast dest!: A_trusts_YM3 YM3_auth_B_to_A_lemma) 370 371 372subsection\<open>Authenticating A to B\<close> 373 374text\<open>using the certificate \<^term>\<open>Crypt K (Nonce NB)\<close>\<close> 375 376text\<open>Assuming the session key is secure, if both certificates are present then 377 A has said NB. We can't be sure about the rest of A's message, but only 378 NB matters for freshness. Note that \<^term>\<open>Key K \<notin> analz (knows Spy evs)\<close> 379 must be the FIRST antecedent of the induction formula.\<close> 380 381text\<open>This lemma allows a use of \<open>unique_session_keys\<close> in the next proof, 382 which otherwise is extremely slow.\<close> 383lemma secure_unique_session_keys: 384 "\<lbrakk>Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace> \<in> analz (spies evs); 385 Crypt (shrK A') \<lbrace>Agent B', Key K, na'\<rbrace> \<in> analz (spies evs); 386 Key K \<notin> analz (knows Spy evs); evs \<in> yahalom\<rbrakk> 387 \<Longrightarrow> A=A' \<and> B=B'" 388by (blast dest!: A_trusts_YM3 dest: unique_session_keys Crypt_Spy_analz_bad) 389 390 391lemma Auth_A_to_B_lemma [rule_format]: 392 "evs \<in> yahalom 393 \<Longrightarrow> Key K \<notin> analz (knows Spy evs) \<longrightarrow> 394 K \<in> symKeys \<longrightarrow> 395 Crypt K (Nonce NB) \<in> parts (knows Spy evs) \<longrightarrow> 396 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> 397 \<in> parts (knows Spy evs) \<longrightarrow> 398 B \<notin> bad \<longrightarrow> 399 (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs)" 400apply (erule yahalom.induct, force, 401 frule_tac [6] YM4_parts_knows_Spy) 402apply (analz_mono_contra, simp_all) 403 subgoal \<comment> \<open>Fake\<close> by blast 404 subgoal \<comment> \<open>YM3 because the message \<^term>\<open>Crypt K (Nonce NB)\<close> could not exist\<close> 405 by (force dest!: Crypt_imp_keysFor) 406 subgoal \<comment> \<open>YM4: was \<^term>\<open>Crypt K (Nonce NB)\<close> the very last message? If not, use the induction hypothesis, 407 otherwise by unicity of session keys\<close> 408 by (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys) 409done 410 411 412text\<open>If B receives YM4 then A has used nonce NB (and therefore is alive). 413 Moreover, A associates K with NB (thus is talking about the same run). 414 Other premises guarantee secrecy of K.\<close> 415theorem YM4_imp_A_Said_YM3 [rule_format]: 416 "\<lbrakk>Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace>, 417 Crypt K (Nonce NB)\<rbrace> \<in> set evs; 418 (\<forall>NA. Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> \<notin> set evs); 419 K \<in> symKeys; A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 420 \<Longrightarrow> \<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs" 421by (blast intro: Auth_A_to_B_lemma 422 dest: Spy_not_see_encrypted_key B_trusts_YM4_shrK) 423 424end 425