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