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