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