src/HOL/Auth/CertifiedEmail.thy
author wenzelm
Mon Jan 11 21:21:02 2016 +0100 (2016-01-11)
changeset 62145 5b946c81dfbf
parent 61956 38b73f7940af
child 67443 3abf6a722518
permissions -rw-r--r--
eliminated old defs;
     1 (*  Title:      HOL/Auth/CertifiedEmail.thy
     2     Author:     Giampaolo Bella, Christiano Longo and Lawrence C Paulson
     3 *)
     4 
     5 section\<open>The Certified Electronic Mail Protocol by Abadi et al.\<close>
     6 
     7 theory CertifiedEmail imports Public begin
     8 
     9 abbreviation
    10   TTP :: agent where
    11   "TTP == Server"
    12 
    13 abbreviation
    14   RPwd :: "agent => 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.*)
    20 consts
    21   NoAuth   :: nat
    22   TTPAuth  :: nat
    23   SAuth    :: nat
    24   BothAuth :: nat
    25 
    26 text\<open>We formalize a fixed way of computing responses.  Could be better.\<close>
    27 definition "response" :: "agent => agent => nat => msg" where
    28    "response S R q == Hash \<lbrace>Agent S, Key (shrK R), Nonce q\<rbrace>"
    29 
    30 
    31 inductive_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 S2TTP} while transmitting it and her
    59      password to @{term TTP} 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 TTP} 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 R}), but @{term TTP} accepts the message only 
    72          if the given password is that of the claimed sender, @{term R}.
    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 
    89 declare Says_imp_knows_Spy [THEN analz.Inj, dest]
    90 declare analz_into_parts [dest]
    91 
    92 (*A "possibility property": there are traces that reach the end*)
    93 lemma "[| 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"
    96 apply (intro exI bexI)
    97 apply (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]) 
   101 apply (possibility, auto) 
   102 done
   103 
   104 
   105 lemma Gets_imp_Says:
   106  "[| Gets B X \<in> set evs; evs \<in> certified_mail |] ==> \<exists>A. Says A B X \<in> set evs"
   107 apply (erule rev_mp)
   108 apply (erule certified_mail.induct, auto)
   109 done
   110 
   111 
   112 lemma Gets_imp_parts_knows_Spy:
   113      "[|Gets A X \<in> set evs; evs \<in> certified_mail|] ==> X \<in> parts(spies evs)"
   114 apply (drule Gets_imp_Says, simp)
   115 apply (blast dest: Says_imp_knows_Spy parts.Inj) 
   116 done
   117 
   118 lemma 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)"
   123 apply (drule Gets_imp_Says, simp) 
   124 apply (blast dest: Says_imp_knows_Spy analz.Inj) 
   125 done
   126 
   127 lemmas CM2_S2TTP_parts_knows_Spy = 
   128     CM2_S2TTP_analz_knows_Spy [THEN analz_subset_parts [THEN subsetD]]
   129 
   130 lemma hr_form_lemma [rule_format]:
   131  "evs \<in> certified_mail
   132   ==> hr \<notin> synth (analz (spies evs)) --> 
   133       (\<forall>S2TTP. Notes TTP \<lbrace>Agent R, Agent TTP, S2TTP, pwd, hr\<rbrace>
   134           \<in> set evs --> 
   135       (\<exists>clt q S em. hr = Hash \<lbrace>Number clt, Nonce q, response S R q, em\<rbrace>))"
   136 apply (erule certified_mail.induct)
   137 apply (synth_analz_mono_contra, simp_all, blast+)
   138 done 
   139 
   140 text\<open>Cannot strengthen the first disjunct to @{term "R\<noteq>Spy"} because
   141 the fakessl rule allows Spy to spoof the sender's name.  Maybe can
   142 strengthen the second disjunct with @{term "R\<noteq>Spy"}.\<close>
   143 lemma 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>)"
   148 by (blast intro: hr_form_lemma) 
   149 
   150 lemma Spy_dont_know_private_keys [dest!]:
   151     "[|Key (privateKey b A) \<in> parts (spies evs); evs \<in> certified_mail|]
   152      ==> A \<in> bad"
   153 apply (erule rev_mp) 
   154 apply (erule certified_mail.induct, simp_all)
   155 txt\<open>Fake\<close>
   156 apply (blast dest: Fake_parts_insert_in_Un) 
   157 txt\<open>Message 1\<close>
   158 apply blast  
   159 txt\<open>Message 3\<close>
   160 apply (frule_tac hr_form, assumption)
   161 apply (elim disjE exE) 
   162 apply (simp_all add: parts_insert2) 
   163  apply (force dest!: parts_insert_subset_Un [THEN [2] rev_subsetD] 
   164                      analz_subset_parts [THEN subsetD], blast) 
   165 done
   166 
   167 lemma Spy_know_private_keys_iff [simp]:
   168     "evs \<in> certified_mail
   169      ==> (Key (privateKey b A) \<in> parts (spies evs)) = (A \<in> bad)"
   170 by blast 
   171 
   172 lemma Spy_dont_know_TTPKey_parts [simp]:
   173      "evs \<in> certified_mail ==> Key (privateKey b TTP) \<notin> parts(spies evs)" 
   174 by simp
   175 
   176 lemma Spy_dont_know_TTPKey_analz [simp]:
   177      "evs \<in> certified_mail ==> Key (privateKey b TTP) \<notin> analz(spies evs)"
   178 by auto
   179 
   180 text\<open>Thus, prove any goal that assumes that @{term Spy} knows a private key
   181 belonging to @{term TTP}\<close>
   182 declare Spy_dont_know_TTPKey_parts [THEN [2] rev_notE, elim!]
   183 
   184 
   185 lemma 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)"
   191 apply (rotate_tac 1)
   192 apply (erule rev_mp)
   193 apply (erule certified_mail.induct, simp_all)
   194    apply (blast  intro:parts_insertI)
   195 txt\<open>Fake SSL\<close>
   196 apply (blast dest: parts.Body) 
   197 txt\<open>Message 2\<close>
   198 apply (blast dest!: Gets_imp_Says elim!: knows_Spy_partsEs)
   199 txt\<open>Message 3\<close>
   200 apply (metis parts_insertI)
   201 done
   202 
   203 lemma Spy_dont_know_RPwd [rule_format]:
   204     "evs \<in> certified_mail ==> Key (RPwd A) \<in> parts(spies evs) --> A \<in> bad"
   205 apply (erule certified_mail.induct, simp_all) 
   206 txt\<open>Fake\<close>
   207 apply (blast dest: Fake_parts_insert_in_Un) 
   208 txt\<open>Message 1\<close>
   209 apply blast  
   210 txt\<open>Message 3\<close>
   211 apply (frule CM3_k_parts_knows_Spy, assumption)
   212 apply (frule_tac hr_form, assumption)
   213 apply (elim disjE exE) 
   214 apply (simp_all add: parts_insert2) 
   215 apply (force dest!: parts_insert_subset_Un [THEN [2] rev_subsetD]
   216                     analz_subset_parts [THEN subsetD])
   217 done
   218 
   219 
   220 lemma Spy_know_RPwd_iff [simp]:
   221     "evs \<in> certified_mail ==> (Key (RPwd A) \<in> parts(spies evs)) = (A\<in>bad)"
   222 by (auto simp add: Spy_dont_know_RPwd) 
   223 
   224 lemma Spy_analz_RPwd_iff [simp]:
   225     "evs \<in> certified_mail ==> (Key (RPwd A) \<in> analz(spies evs)) = (A\<in>bad)"
   226 by (metis Spy_know_RPwd_iff Spy_spies_bad_shrK analz.Inj analz_into_parts)
   227 
   228 text\<open>Unused, but a guarantee of sorts\<close>
   229 theorem 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"
   232 apply (erule rev_mp)
   233 apply (erule certified_mail.induct, simp_all) 
   234 txt\<open>Fake\<close>
   235 apply (blast dest: Spy_dont_know_private_keys Fake_parts_insert_in_Un)
   236 txt\<open>Message 1\<close>
   237 apply blast 
   238 txt\<open>Message 3\<close>
   239 apply (frule_tac hr_form, assumption)
   240 apply (elim disjE exE) 
   241 apply (simp_all add: parts_insert2 parts_insert_knows_A) 
   242  apply (blast dest!: Fake_parts_sing_imp_Un, blast)
   243 done
   244 
   245 
   246 subsection\<open>Proving Confidentiality Results\<close>
   247 
   248 lemma analz_image_freshK [rule_format]:
   249  "evs \<in> certified_mail ==>
   250    \<forall>K KK. invKey (pubEK TTP) \<notin> KK -->
   251           (Key K \<in> analz (Key`KK Un (spies evs))) =
   252           (K \<in> KK | Key K \<in> analz (spies evs))"
   253 apply (erule certified_mail.induct)
   254 apply (drule_tac [6] A=TTP in symKey_neq_priEK) 
   255 apply (erule_tac [6] disjE [OF hr_form]) 
   256 apply (drule_tac [5] CM2_S2TTP_analz_knows_Spy) 
   257 prefer 9
   258 apply (elim exE)
   259 apply (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)
   263 done
   264 
   265 
   266 lemma 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))"
   270 by (simp only: analz_image_freshK analz_image_freshK_simps)
   271 
   272 text\<open>@{term S2TTP} must have originated from a valid sender
   273     provided @{term K} is secure.  Proof is surprisingly hard.\<close>
   274 
   275 lemma Notes_SSL_imp_used:
   276      "[|Notes B \<lbrace>Agent A, Agent B, X\<rbrace> \<in> set evs|] ==> X \<in> used evs"
   277 by (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 *)
   282 lemma S2TTP_sender_lemma [rule_format]:
   283  "evs \<in> certified_mail ==>
   284     Key K \<notin> analz (spies evs) -->
   285     (\<forall>AO. Crypt (pubEK TTP)
   286            \<lbrace>Agent S, Number AO, Key K, Agent R, hs\<rbrace> \<in> used evs -->
   287     (\<exists>m ctxt q. 
   288         hs = Hash\<lbrace>Number ctxt, Nonce q, response S R q, Crypt K (Number m)\<rbrace> &
   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))" 
   294 apply (erule certified_mail.induct, analz_mono_contra)
   295 apply (drule_tac [5] CM2_S2TTP_parts_knows_Spy, simp)
   296 apply (simp add: used_Nil Crypt_notin_initState, simp_all)
   297 txt\<open>Fake\<close>
   298 apply (blast dest: Fake_parts_sing [THEN subsetD]
   299              dest!: analz_subset_parts [THEN subsetD])  
   300 txt\<open>Fake SSL\<close>
   301 apply (blast dest: Fake_parts_sing [THEN subsetD]
   302              dest: analz_subset_parts [THEN subsetD])  
   303 txt\<open>Message 1\<close>
   304 apply (clarsimp, blast)
   305 txt\<open>Message 2\<close>
   306 apply (simp add: parts_insert2, clarify) 
   307 apply (metis parts_cut Un_empty_left usedI)
   308 txt\<open>Message 3\<close> 
   309 apply (blast dest: Notes_SSL_imp_used used_parts_subset_parts) 
   310 done 
   311 
   312 lemma 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> &
   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" 
   323 by (blast intro: S2TTP_sender_lemma) 
   324 
   325 
   326 text\<open>Nobody can have used non-existent keys!\<close>
   327 lemma 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))"
   330 apply (erule rev_mp) 
   331 apply (erule certified_mail.induct, simp_all) 
   332 txt\<open>Fake\<close>
   333 apply (force dest!: keysFor_parts_insert) 
   334 txt\<open>Message 1\<close>
   335 apply blast 
   336 txt\<open>Message 3\<close>
   337 apply (frule CM3_k_parts_knows_Spy, assumption)
   338 apply (frule_tac hr_form, assumption) 
   339 apply (force dest!: keysFor_parts_insert)
   340 done
   341 
   342 
   343 text\<open>Less easy to prove @{term "m'=m"}.  Maybe needs a separate unicity
   344 theorem for ciphertexts of the form @{term "Crypt K (Number m)"}, 
   345 where @{term K} is secure.\<close>
   346 lemma Key_unique_lemma [rule_format]:
   347      "evs \<in> certified_mail ==>
   348        Key K \<notin> analz (spies evs) -->
   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 -->
   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 --> R' = R & S' = S & AO' = AO & hs' = hs))" 
   361 apply (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)
   365 txt\<open>Fake\<close>
   366 apply (auto dest!: usedI S2TTP_sender analz_subset_parts [THEN subsetD]) 
   367 done
   368 
   369 text\<open>The key determines the sender, recipient and protocol options.\<close>
   370 lemma 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 & S' = S & AO' = AO & hs' = hs"
   384 by (rule Key_unique_lemma, assumption+)
   385 
   386 
   387 subsection\<open>The Guarantees for Sender and Recipient\<close>
   388 
   389 text\<open>A Sender's guarantee:
   390       If Spy gets the key then @{term R} is bad and @{term S} moreover
   391       gets his return receipt (and therefore has no grounds for complaint).\<close>
   392 theorem 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 & Gets S (Crypt (priSK TTP) S2TTP) \<in> set evs"
   400 apply (erule rev_mp)
   401 apply (erule ssubst)
   402 apply (erule rev_mp)
   403 apply (erule certified_mail.induct, simp_all)
   404 txt\<open>Fake\<close>
   405 apply spy_analz
   406 txt\<open>Fake SSL\<close>
   407 apply spy_analz
   408 txt\<open>Message 3\<close>
   409 apply (frule_tac hr_form, assumption)
   410 apply (elim disjE exE) 
   411 apply (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) 
   415 apply (simp_all add: symKey_neq_priEK analz_insert_freshK)
   416 apply (blast dest: Notes_SSL_imp_used S2TTP_sender Key_unique)+
   417 done
   418 
   419 text\<open>Confidentially for the symmetric key\<close>
   420 theorem 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)"
   427 by (blast dest: S_fairness_bad_R) 
   428 
   429 
   430 text\<open>Agent @{term R}, who may be the Spy, doesn't receive the key
   431  until @{term S} has access to the return receipt.\<close> 
   432 theorem 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"
   439 apply (erule rev_mp)
   440 apply (erule ssubst)
   441 apply (erule rev_mp)
   442 apply (erule certified_mail.induct, simp_all)
   443 txt\<open>Message 1\<close>
   444 apply (blast dest: Notes_imp_used) 
   445 txt\<open>Message 3\<close>
   446 apply (blast dest: Notes_SSL_imp_used S2TTP_sender Key_unique S_fairness_bad_R) 
   447 done
   448 
   449 
   450 text\<open>If @{term R} sends message 2, and a delivery certificate exists, 
   451  then @{term R} receives the necessary key.  This result is also important
   452  to @{term S}, as it confirms the validity of the return receipt.\<close>
   453 theorem 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"
   461 apply (erule rev_mp)
   462 apply (erule ssubst)
   463 apply (erule ssubst)
   464 apply (erule certified_mail.induct, simp_all)
   465 txt\<open>Fake\<close> 
   466 apply (blast dest: Fake_parts_sing [THEN subsetD]
   467              dest!: analz_subset_parts [THEN subsetD])  
   468 txt\<open>Fake SSL\<close>
   469 apply (blast dest: Fake_parts_sing [THEN subsetD]
   470             dest!: analz_subset_parts [THEN subsetD])  
   471 txt\<open>Message 2\<close>
   472 apply (drule CM2_S2TTP_parts_knows_Spy, assumption)
   473 apply (force dest: parts_cut)
   474 txt\<open>Message 3\<close>
   475 apply (frule_tac hr_form, assumption)
   476 apply (elim disjE exE, simp_all) 
   477 apply (blast dest: Fake_parts_sing [THEN subsetD]
   478              dest!: analz_subset_parts [THEN subsetD]) 
   479 done
   480 
   481 end