1(* Title: HOL/Auth/CertifiedEmail.thy 2 Author: Giampaolo Bella, Christiano Longo and Lawrence C Paulson 3*) 4 5section\<open>The Certified Electronic Mail Protocol by Abadi et al.\<close> 6 7theory CertifiedEmail imports Public begin 8 9abbreviation 10 TTP :: agent where 11 "TTP == Server" 12 13abbreviation 14 RPwd :: "agent \<Rightarrow> key" where 15 "RPwd == shrK" 16 17 18(*FIXME: the four options should be represented by pairs of 0 or 1. 19 Right now only BothAuth is modelled.*) 20consts 21 NoAuth :: nat 22 TTPAuth :: nat 23 SAuth :: nat 24 BothAuth :: nat 25 26text\<open>We formalize a fixed way of computing responses. Could be better.\<close> 27definition "response" :: "agent \<Rightarrow> agent \<Rightarrow> nat \<Rightarrow> msg" where 28 "response S R q == Hash \<lbrace>Agent S, Key (shrK R), Nonce q\<rbrace>" 29 30 31inductive_set certified_mail :: "event list set" 32 where 33 34 Nil: \<comment> \<open>The empty trace\<close> 35 "[] \<in> certified_mail" 36 37| Fake: \<comment> \<open>The Spy may say anything he can say. The sender field is correct, 38 but agents don't use that information.\<close> 39 "[| evsf \<in> certified_mail; X \<in> synth(analz(spies evsf))|] 40 ==> Says Spy B X # evsf \<in> certified_mail" 41 42| FakeSSL: \<comment> \<open>The Spy may open SSL sessions with TTP, who is the only agent 43 equipped with the necessary credentials to serve as an SSL server.\<close> 44 "[| evsfssl \<in> certified_mail; X \<in> synth(analz(spies evsfssl))|] 45 ==> Notes TTP \<lbrace>Agent Spy, Agent TTP, X\<rbrace> # evsfssl \<in> certified_mail" 46 47| CM1: \<comment> \<open>The sender approaches the recipient. The message is a number.\<close> 48 "[|evs1 \<in> certified_mail; 49 Key K \<notin> used evs1; 50 K \<in> symKeys; 51 Nonce q \<notin> used evs1; 52 hs = Hash\<lbrace>Number cleartext, Nonce q, response S R q, Crypt K (Number m)\<rbrace>; 53 S2TTP = Crypt(pubEK TTP) \<lbrace>Agent S, Number BothAuth, Key K, Agent R, hs\<rbrace>|] 54 ==> Says S R \<lbrace>Agent S, Agent TTP, Crypt K (Number m), Number BothAuth, 55 Number cleartext, Nonce q, S2TTP\<rbrace> # evs1 56 \<in> certified_mail" 57 58| CM2: \<comment> \<open>The recipient records \<^term>\<open>S2TTP\<close> while transmitting it and her 59 password to \<^term>\<open>TTP\<close> over an SSL channel.\<close> 60 "[|evs2 \<in> certified_mail; 61 Gets R \<lbrace>Agent S, Agent TTP, em, Number BothAuth, Number cleartext, 62 Nonce q, S2TTP\<rbrace> \<in> set evs2; 63 TTP \<noteq> R; 64 hr = Hash \<lbrace>Number cleartext, Nonce q, response S R q, em\<rbrace> |] 65 ==> 66 Notes TTP \<lbrace>Agent R, Agent TTP, S2TTP, Key(RPwd R), hr\<rbrace> # evs2 67 \<in> certified_mail" 68 69| CM3: \<comment> \<open>\<^term>\<open>TTP\<close> simultaneously reveals the key to the recipient and gives 70 a receipt to the sender. The SSL channel does not authenticate 71 the client (\<^term>\<open>R\<close>), but \<^term>\<open>TTP\<close> accepts the message only 72 if the given password is that of the claimed sender, \<^term>\<open>R\<close>. 73 He replies over the established SSL channel.\<close> 74 "[|evs3 \<in> certified_mail; 75 Notes TTP \<lbrace>Agent R, Agent TTP, S2TTP, Key(RPwd R), hr\<rbrace> \<in> set evs3; 76 S2TTP = Crypt (pubEK TTP) 77 \<lbrace>Agent S, Number BothAuth, Key k, Agent R, hs\<rbrace>; 78 TTP \<noteq> R; hs = hr; k \<in> symKeys|] 79 ==> 80 Notes R \<lbrace>Agent TTP, Agent R, Key k, hr\<rbrace> # 81 Gets S (Crypt (priSK TTP) S2TTP) # 82 Says TTP S (Crypt (priSK TTP) S2TTP) # evs3 \<in> certified_mail" 83 84| Reception: 85 "[|evsr \<in> certified_mail; Says A B X \<in> set evsr|] 86 ==> Gets B X#evsr \<in> certified_mail" 87 88 89declare Says_imp_knows_Spy [THEN analz.Inj, dest] 90declare analz_into_parts [dest] 91 92(*A "possibility property": there are traces that reach the end*) 93lemma "[| Key K \<notin> used []; K \<in> symKeys |] ==> 94 \<exists>S2TTP. \<exists>evs \<in> certified_mail. 95 Says TTP S (Crypt (priSK TTP) S2TTP) \<in> set evs" 96apply (intro exI bexI) 97apply (rule_tac [2] certified_mail.Nil 98 [THEN certified_mail.CM1, THEN certified_mail.Reception, 99 THEN certified_mail.CM2, 100 THEN certified_mail.CM3]) 101apply (possibility, auto) 102done 103 104 105lemma Gets_imp_Says: 106 "[| Gets B X \<in> set evs; evs \<in> certified_mail |] ==> \<exists>A. Says A B X \<in> set evs" 107apply (erule rev_mp) 108apply (erule certified_mail.induct, auto) 109done 110 111 112lemma Gets_imp_parts_knows_Spy: 113 "[|Gets A X \<in> set evs; evs \<in> certified_mail|] ==> X \<in> parts(spies evs)" 114apply (drule Gets_imp_Says, simp) 115apply (blast dest: Says_imp_knows_Spy parts.Inj) 116done 117 118lemma CM2_S2TTP_analz_knows_Spy: 119 "[|Gets R \<lbrace>Agent A, Agent B, em, Number AO, Number cleartext, 120 Nonce q, S2TTP\<rbrace> \<in> set evs; 121 evs \<in> certified_mail|] 122 ==> S2TTP \<in> analz(spies evs)" 123apply (drule Gets_imp_Says, simp) 124apply (blast dest: Says_imp_knows_Spy analz.Inj) 125done 126 127lemmas CM2_S2TTP_parts_knows_Spy = 128 CM2_S2TTP_analz_knows_Spy [THEN analz_subset_parts [THEN subsetD]] 129 130lemma hr_form_lemma [rule_format]: 131 "evs \<in> certified_mail 132 \<Longrightarrow> hr \<notin> synth (analz (spies evs)) \<longrightarrow> 133 (\<forall>S2TTP. Notes TTP \<lbrace>Agent R, Agent TTP, S2TTP, pwd, hr\<rbrace> 134 \<in> set evs \<longrightarrow> 135 (\<exists>clt q S em. hr = Hash \<lbrace>Number clt, Nonce q, response S R q, em\<rbrace>))" 136apply (erule certified_mail.induct) 137apply (synth_analz_mono_contra, simp_all, blast+) 138done 139 140text\<open>Cannot strengthen the first disjunct to \<^term>\<open>R\<noteq>Spy\<close> because 141the fakessl rule allows Spy to spoof the sender's name. Maybe can 142strengthen the second disjunct with \<^term>\<open>R\<noteq>Spy\<close>.\<close> 143lemma hr_form: 144 "[|Notes TTP \<lbrace>Agent R, Agent TTP, S2TTP, pwd, hr\<rbrace> \<in> set evs; 145 evs \<in> certified_mail|] 146 ==> hr \<in> synth (analz (spies evs)) | 147 (\<exists>clt q S em. hr = Hash \<lbrace>Number clt, Nonce q, response S R q, em\<rbrace>)" 148by (blast intro: hr_form_lemma) 149 150lemma Spy_dont_know_private_keys [dest!]: 151 "[|Key (privateKey b A) \<in> parts (spies evs); evs \<in> certified_mail|] 152 ==> A \<in> bad" 153apply (erule rev_mp) 154apply (erule certified_mail.induct, simp_all) 155txt\<open>Fake\<close> 156apply (blast dest: Fake_parts_insert_in_Un) 157txt\<open>Message 1\<close> 158apply blast 159txt\<open>Message 3\<close> 160apply (frule_tac hr_form, assumption) 161apply (elim disjE exE) 162apply (simp_all add: parts_insert2) 163 apply (force dest!: parts_insert_subset_Un [THEN [2] rev_subsetD] 164 analz_subset_parts [THEN subsetD], blast) 165done 166 167lemma Spy_know_private_keys_iff [simp]: 168 "evs \<in> certified_mail 169 ==> (Key (privateKey b A) \<in> parts (spies evs)) = (A \<in> bad)" 170by blast 171 172lemma Spy_dont_know_TTPKey_parts [simp]: 173 "evs \<in> certified_mail ==> Key (privateKey b TTP) \<notin> parts(spies evs)" 174by simp 175 176lemma Spy_dont_know_TTPKey_analz [simp]: 177 "evs \<in> certified_mail ==> Key (privateKey b TTP) \<notin> analz(spies evs)" 178by auto 179 180text\<open>Thus, prove any goal that assumes that \<^term>\<open>Spy\<close> knows a private key 181belonging to \<^term>\<open>TTP\<close>\<close> 182declare Spy_dont_know_TTPKey_parts [THEN [2] rev_notE, elim!] 183 184 185lemma CM3_k_parts_knows_Spy: 186 "[| evs \<in> certified_mail; 187 Notes TTP \<lbrace>Agent A, Agent TTP, 188 Crypt (pubEK TTP) \<lbrace>Agent S, Number AO, Key K, 189 Agent R, hs\<rbrace>, Key (RPwd R), hs\<rbrace> \<in> set evs|] 190 ==> Key K \<in> parts(spies evs)" 191apply (rotate_tac 1) 192apply (erule rev_mp) 193apply (erule certified_mail.induct, simp_all) 194 apply (blast intro:parts_insertI) 195txt\<open>Fake SSL\<close> 196apply (blast dest: parts.Body) 197txt\<open>Message 2\<close> 198apply (blast dest!: Gets_imp_Says elim!: knows_Spy_partsEs) 199txt\<open>Message 3\<close> 200apply (metis parts_insertI) 201done 202 203lemma Spy_dont_know_RPwd [rule_format]: 204 "evs \<in> certified_mail ==> Key (RPwd A) \<in> parts(spies evs) \<longrightarrow> A \<in> bad" 205apply (erule certified_mail.induct, simp_all) 206txt\<open>Fake\<close> 207apply (blast dest: Fake_parts_insert_in_Un) 208txt\<open>Message 1\<close> 209apply blast 210txt\<open>Message 3\<close> 211apply (frule CM3_k_parts_knows_Spy, assumption) 212apply (frule_tac hr_form, assumption) 213apply (elim disjE exE) 214apply (simp_all add: parts_insert2) 215apply (force dest!: parts_insert_subset_Un [THEN [2] rev_subsetD] 216 analz_subset_parts [THEN subsetD]) 217done 218 219 220lemma Spy_know_RPwd_iff [simp]: 221 "evs \<in> certified_mail ==> (Key (RPwd A) \<in> parts(spies evs)) = (A\<in>bad)" 222by (auto simp add: Spy_dont_know_RPwd) 223 224lemma Spy_analz_RPwd_iff [simp]: 225 "evs \<in> certified_mail ==> (Key (RPwd A) \<in> analz(spies evs)) = (A\<in>bad)" 226by (metis Spy_know_RPwd_iff Spy_spies_bad_shrK analz.Inj analz_into_parts) 227 228text\<open>Unused, but a guarantee of sorts\<close> 229theorem CertAutenticity: 230 "[|Crypt (priSK TTP) X \<in> parts (spies evs); evs \<in> certified_mail|] 231 ==> \<exists>A. Says TTP A (Crypt (priSK TTP) X) \<in> set evs" 232apply (erule rev_mp) 233apply (erule certified_mail.induct, simp_all) 234txt\<open>Fake\<close> 235apply (blast dest: Spy_dont_know_private_keys Fake_parts_insert_in_Un) 236txt\<open>Message 1\<close> 237apply blast 238txt\<open>Message 3\<close> 239apply (frule_tac hr_form, assumption) 240apply (elim disjE exE) 241apply (simp_all add: parts_insert2 parts_insert_knows_A) 242 apply (blast dest!: Fake_parts_sing_imp_Un, blast) 243done 244 245 246subsection\<open>Proving Confidentiality Results\<close> 247 248lemma analz_image_freshK [rule_format]: 249 "evs \<in> certified_mail ==> 250 \<forall>K KK. invKey (pubEK TTP) \<notin> KK \<longrightarrow> 251 (Key K \<in> analz (Key`KK \<union> (spies evs))) = 252 (K \<in> KK | Key K \<in> analz (spies evs))" 253apply (erule certified_mail.induct) 254apply (drule_tac [6] A=TTP in symKey_neq_priEK) 255apply (erule_tac [6] disjE [OF hr_form]) 256apply (drule_tac [5] CM2_S2TTP_analz_knows_Spy) 257prefer 9 258apply (elim exE) 259apply (simp_all add: synth_analz_insert_eq 260 subset_trans [OF _ subset_insertI] 261 subset_trans [OF _ Un_upper2] 262 del: image_insert image_Un add: analz_image_freshK_simps) 263done 264 265 266lemma analz_insert_freshK: 267 "[| evs \<in> certified_mail; KAB \<noteq> invKey (pubEK TTP) |] ==> 268 (Key K \<in> analz (insert (Key KAB) (spies evs))) = 269 (K = KAB | Key K \<in> analz (spies evs))" 270by (simp only: analz_image_freshK analz_image_freshK_simps) 271 272text\<open>\<^term>\<open>S2TTP\<close> must have originated from a valid sender 273 provided \<^term>\<open>K\<close> is secure. Proof is surprisingly hard.\<close> 274 275lemma Notes_SSL_imp_used: 276 "[|Notes B \<lbrace>Agent A, Agent B, X\<rbrace> \<in> set evs|] ==> X \<in> used evs" 277by (blast dest!: Notes_imp_used) 278 279 280(*The weaker version, replacing "used evs" by "parts (spies evs)", 281 isn't inductive: message 3 case can't be proved *) 282lemma S2TTP_sender_lemma [rule_format]: 283 "evs \<in> certified_mail ==> 284 Key K \<notin> analz (spies evs) \<longrightarrow> 285 (\<forall>AO. Crypt (pubEK TTP) 286 \<lbrace>Agent S, Number AO, Key K, Agent R, hs\<rbrace> \<in> used evs \<longrightarrow> 287 (\<exists>m ctxt q. 288 hs = Hash\<lbrace>Number ctxt, Nonce q, response S R q, Crypt K (Number m)\<rbrace> \<and> 289 Says S R 290 \<lbrace>Agent S, Agent TTP, Crypt K (Number m), Number AO, 291 Number ctxt, Nonce q, 292 Crypt (pubEK TTP) 293 \<lbrace>Agent S, Number AO, Key K, Agent R, hs \<rbrace>\<rbrace> \<in> set evs))" 294apply (erule certified_mail.induct, analz_mono_contra) 295apply (drule_tac [5] CM2_S2TTP_parts_knows_Spy, simp) 296apply (simp add: used_Nil Crypt_notin_initState, simp_all) 297txt\<open>Fake\<close> 298apply (blast dest: Fake_parts_sing [THEN subsetD] 299 dest!: analz_subset_parts [THEN subsetD]) 300txt\<open>Fake SSL\<close> 301apply (blast dest: Fake_parts_sing [THEN subsetD] 302 dest: analz_subset_parts [THEN subsetD]) 303txt\<open>Message 1\<close> 304apply (clarsimp, blast) 305txt\<open>Message 2\<close> 306apply (simp add: parts_insert2, clarify) 307apply (metis parts_cut Un_empty_left usedI) 308txt\<open>Message 3\<close> 309apply (blast dest: Notes_SSL_imp_used used_parts_subset_parts) 310done 311 312lemma S2TTP_sender: 313 "[|Crypt (pubEK TTP) \<lbrace>Agent S, Number AO, Key K, Agent R, hs\<rbrace> \<in> used evs; 314 Key K \<notin> analz (spies evs); 315 evs \<in> certified_mail|] 316 ==> \<exists>m ctxt q. 317 hs = Hash\<lbrace>Number ctxt, Nonce q, response S R q, Crypt K (Number m)\<rbrace> \<and> 318 Says S R 319 \<lbrace>Agent S, Agent TTP, Crypt K (Number m), Number AO, 320 Number ctxt, Nonce q, 321 Crypt (pubEK TTP) 322 \<lbrace>Agent S, Number AO, Key K, Agent R, hs\<rbrace>\<rbrace> \<in> set evs" 323by (blast intro: S2TTP_sender_lemma) 324 325 326text\<open>Nobody can have used non-existent keys!\<close> 327lemma new_keys_not_used [simp]: 328 "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> certified_mail|] 329 ==> K \<notin> keysFor (parts (spies evs))" 330apply (erule rev_mp) 331apply (erule certified_mail.induct, simp_all) 332txt\<open>Fake\<close> 333apply (force dest!: keysFor_parts_insert) 334txt\<open>Message 1\<close> 335apply blast 336txt\<open>Message 3\<close> 337apply (frule CM3_k_parts_knows_Spy, assumption) 338apply (frule_tac hr_form, assumption) 339apply (force dest!: keysFor_parts_insert) 340done 341 342 343text\<open>Less easy to prove \<^term>\<open>m'=m\<close>. Maybe needs a separate unicity 344theorem for ciphertexts of the form \<^term>\<open>Crypt K (Number m)\<close>, 345where \<^term>\<open>K\<close> is secure.\<close> 346lemma Key_unique_lemma [rule_format]: 347 "evs \<in> certified_mail ==> 348 Key K \<notin> analz (spies evs) \<longrightarrow> 349 (\<forall>m cleartext q hs. 350 Says S R 351 \<lbrace>Agent S, Agent TTP, Crypt K (Number m), Number AO, 352 Number cleartext, Nonce q, 353 Crypt (pubEK TTP) \<lbrace>Agent S, Number AO, Key K, Agent R, hs\<rbrace>\<rbrace> 354 \<in> set evs \<longrightarrow> 355 (\<forall>m' cleartext' q' hs'. 356 Says S' R' 357 \<lbrace>Agent S', Agent TTP, Crypt K (Number m'), Number AO', 358 Number cleartext', Nonce q', 359 Crypt (pubEK TTP) \<lbrace>Agent S', Number AO', Key K, Agent R', hs'\<rbrace>\<rbrace> 360 \<in> set evs \<longrightarrow> R' = R \<and> S' = S \<and> AO' = AO \<and> hs' = hs))" 361apply (erule certified_mail.induct, analz_mono_contra, simp_all) 362 prefer 2 363 txt\<open>Message 1\<close> 364 apply (blast dest!: Says_imp_knows_Spy [THEN parts.Inj] new_keys_not_used Crypt_imp_keysFor) 365txt\<open>Fake\<close> 366apply (auto dest!: usedI S2TTP_sender analz_subset_parts [THEN subsetD]) 367done 368 369text\<open>The key determines the sender, recipient and protocol options.\<close> 370lemma Key_unique: 371 "[|Says S R 372 \<lbrace>Agent S, Agent TTP, Crypt K (Number m), Number AO, 373 Number cleartext, Nonce q, 374 Crypt (pubEK TTP) \<lbrace>Agent S, Number AO, Key K, Agent R, hs\<rbrace>\<rbrace> 375 \<in> set evs; 376 Says S' R' 377 \<lbrace>Agent S', Agent TTP, Crypt K (Number m'), Number AO', 378 Number cleartext', Nonce q', 379 Crypt (pubEK TTP) \<lbrace>Agent S', Number AO', Key K, Agent R', hs'\<rbrace>\<rbrace> 380 \<in> set evs; 381 Key K \<notin> analz (spies evs); 382 evs \<in> certified_mail|] 383 ==> R' = R \<and> S' = S \<and> AO' = AO \<and> hs' = hs" 384by (rule Key_unique_lemma, assumption+) 385 386 387subsection\<open>The Guarantees for Sender and Recipient\<close> 388 389text\<open>A Sender's guarantee: 390 If Spy gets the key then \<^term>\<open>R\<close> is bad and \<^term>\<open>S\<close> moreover 391 gets his return receipt (and therefore has no grounds for complaint).\<close> 392theorem S_fairness_bad_R: 393 "[|Says S R \<lbrace>Agent S, Agent TTP, Crypt K (Number m), Number AO, 394 Number cleartext, Nonce q, S2TTP\<rbrace> \<in> set evs; 395 S2TTP = Crypt (pubEK TTP) \<lbrace>Agent S, Number AO, Key K, Agent R, hs\<rbrace>; 396 Key K \<in> analz (spies evs); 397 evs \<in> certified_mail; 398 S\<noteq>Spy|] 399 ==> R \<in> bad \<and> Gets S (Crypt (priSK TTP) S2TTP) \<in> set evs" 400apply (erule rev_mp) 401apply (erule ssubst) 402apply (erule rev_mp) 403apply (erule certified_mail.induct, simp_all) 404txt\<open>Fake\<close> 405apply spy_analz 406txt\<open>Fake SSL\<close> 407apply spy_analz 408txt\<open>Message 3\<close> 409apply (frule_tac hr_form, assumption) 410apply (elim disjE exE) 411apply (simp_all add: synth_analz_insert_eq 412 subset_trans [OF _ subset_insertI] 413 subset_trans [OF _ Un_upper2] 414 del: image_insert image_Un add: analz_image_freshK_simps) 415apply (simp_all add: symKey_neq_priEK analz_insert_freshK) 416apply (blast dest: Notes_SSL_imp_used S2TTP_sender Key_unique)+ 417done 418 419text\<open>Confidentially for the symmetric key\<close> 420theorem Spy_not_see_encrypted_key: 421 "[|Says S R \<lbrace>Agent S, Agent TTP, Crypt K (Number m), Number AO, 422 Number cleartext, Nonce q, S2TTP\<rbrace> \<in> set evs; 423 S2TTP = Crypt (pubEK TTP) \<lbrace>Agent S, Number AO, Key K, Agent R, hs\<rbrace>; 424 evs \<in> certified_mail; 425 S\<noteq>Spy; R \<notin> bad|] 426 ==> Key K \<notin> analz(spies evs)" 427by (blast dest: S_fairness_bad_R) 428 429 430text\<open>Agent \<^term>\<open>R\<close>, who may be the Spy, doesn't receive the key 431 until \<^term>\<open>S\<close> has access to the return receipt.\<close> 432theorem S_guarantee: 433 "[|Says S R \<lbrace>Agent S, Agent TTP, Crypt K (Number m), Number AO, 434 Number cleartext, Nonce q, S2TTP\<rbrace> \<in> set evs; 435 S2TTP = Crypt (pubEK TTP) \<lbrace>Agent S, Number AO, Key K, Agent R, hs\<rbrace>; 436 Notes R \<lbrace>Agent TTP, Agent R, Key K, hs\<rbrace> \<in> set evs; 437 S\<noteq>Spy; evs \<in> certified_mail|] 438 ==> Gets S (Crypt (priSK TTP) S2TTP) \<in> set evs" 439apply (erule rev_mp) 440apply (erule ssubst) 441apply (erule rev_mp) 442apply (erule certified_mail.induct, simp_all) 443txt\<open>Message 1\<close> 444apply (blast dest: Notes_imp_used) 445txt\<open>Message 3\<close> 446apply (blast dest: Notes_SSL_imp_used S2TTP_sender Key_unique S_fairness_bad_R) 447done 448 449 450text\<open>If \<^term>\<open>R\<close> sends message 2, and a delivery certificate exists, 451 then \<^term>\<open>R\<close> receives the necessary key. This result is also important 452 to \<^term>\<open>S\<close>, as it confirms the validity of the return receipt.\<close> 453theorem RR_validity: 454 "[|Crypt (priSK TTP) S2TTP \<in> used evs; 455 S2TTP = Crypt (pubEK TTP) 456 \<lbrace>Agent S, Number AO, Key K, Agent R, 457 Hash \<lbrace>Number cleartext, Nonce q, r, em\<rbrace>\<rbrace>; 458 hr = Hash \<lbrace>Number cleartext, Nonce q, r, em\<rbrace>; 459 R\<noteq>Spy; evs \<in> certified_mail|] 460 ==> Notes R \<lbrace>Agent TTP, Agent R, Key K, hr\<rbrace> \<in> set evs" 461apply (erule rev_mp) 462apply (erule ssubst) 463apply (erule ssubst) 464apply (erule certified_mail.induct, simp_all) 465txt\<open>Fake\<close> 466apply (blast dest: Fake_parts_sing [THEN subsetD] 467 dest!: analz_subset_parts [THEN subsetD]) 468txt\<open>Fake SSL\<close> 469apply (blast dest: Fake_parts_sing [THEN subsetD] 470 dest!: analz_subset_parts [THEN subsetD]) 471txt\<open>Message 2\<close> 472apply (drule CM2_S2TTP_parts_knows_Spy, assumption) 473apply (force dest: parts_cut) 474txt\<open>Message 3\<close> 475apply (frule_tac hr_form, assumption) 476apply (elim disjE exE, simp_all) 477apply (blast dest: Fake_parts_sing [THEN subsetD] 478 dest!: analz_subset_parts [THEN subsetD]) 479done 480 481end 482