Theory CertifiedEmail

(*  Title:      HOL/Auth/CertifiedEmail.thy
    Author:     Giampaolo Bella, Christiano Longo and Lawrence C Paulson
*)

sectionThe Certified Electronic Mail Protocol by Abadi et al.

theory CertifiedEmail imports Public begin

abbreviation
  TTP :: agent where
  "TTP == Server"

abbreviation
  RPwd :: "agent  key" where
  "RPwd == shrK"

 
(*FIXME: the four options should be represented by pairs of 0 or 1.
  Right now only BothAuth is modelled.*)
consts
  NoAuth   :: nat
  TTPAuth  :: nat
  SAuth    :: nat
  BothAuth :: nat

textWe formalize a fixed way of computing responses.  Could be better.
definition "response" :: "agent  agent  nat  msg" where
   "response S R q == Hash Agent S, Key (shrK R), Nonce q"


inductive_set certified_mail :: "event list set"
  where

  Nil: ― ‹The empty trace
     "[]  certified_mail"

| Fake: ― ‹The Spy may say anything he can say.  The sender field is correct,
          but agents don't use that information.
      "[| evsf  certified_mail; X  synth(analz(spies evsf))|] 
       ==> Says Spy B X # evsf  certified_mail"

| FakeSSL: ― ‹The Spy may open SSL sessions with TTP, who is the only agent
    equipped with the necessary credentials to serve as an SSL server.
         "[| evsfssl  certified_mail; X  synth(analz(spies evsfssl))|]
          ==> Notes TTP Agent Spy, Agent TTP, X # evsfssl  certified_mail"

| CM1: ― ‹The sender approaches the recipient.  The message is a number.
 "[|evs1  certified_mail;
    Key K  used evs1;
    K  symKeys;
    Nonce q  used evs1;
    hs = HashNumber cleartext, Nonce q, response S R q, Crypt K (Number m);
    S2TTP = Crypt(pubEK TTP) Agent S, Number BothAuth, Key K, Agent R, hs|]
  ==> Says S R Agent S, Agent TTP, Crypt K (Number m), Number BothAuth, 
                 Number cleartext, Nonce q, S2TTP # evs1 
         certified_mail"

| CM2: ― ‹The recipient records termS2TTP while transmitting it and her
     password to termTTP over an SSL channel.
 "[|evs2  certified_mail;
    Gets R Agent S, Agent TTP, em, Number BothAuth, Number cleartext, 
             Nonce q, S2TTP  set evs2;
    TTP  R;  
    hr = Hash Number cleartext, Nonce q, response S R q, em |]
  ==> 
   Notes TTP Agent R, Agent TTP, S2TTP, Key(RPwd R), hr # evs2
       certified_mail"

| CM3: ― ‹termTTP simultaneously reveals the key to the recipient and gives
         a receipt to the sender.  The SSL channel does not authenticate 
         the client (termR), but termTTP accepts the message only 
         if the given password is that of the claimed sender, termR.
         He replies over the established SSL channel.
 "[|evs3  certified_mail;
    Notes TTP Agent R, Agent TTP, S2TTP, Key(RPwd R), hr  set evs3;
    S2TTP = Crypt (pubEK TTP) 
                     Agent S, Number BothAuth, Key k, Agent R, hs;
    TTP  R;  hs = hr;  k  symKeys|]
  ==> 
   Notes R Agent TTP, Agent R, Key k, hr # 
   Gets S (Crypt (priSK TTP) S2TTP) # 
   Says TTP S (Crypt (priSK TTP) S2TTP) # evs3  certified_mail"

| Reception:
 "[|evsr  certified_mail; Says A B X  set evsr|]
  ==> Gets B X#evsr  certified_mail"


declare Says_imp_knows_Spy [THEN analz.Inj, dest]
declare analz_into_parts [dest]

(*A "possibility property": there are traces that reach the end*)
lemma "[| Key K  used []; K  symKeys |] ==> 
       S2TTP. evs  certified_mail.
           Says TTP S (Crypt (priSK TTP) S2TTP)  set evs"
apply (intro exI bexI)
apply (rule_tac [2] certified_mail.Nil
                    [THEN certified_mail.CM1, THEN certified_mail.Reception,
                     THEN certified_mail.CM2, 
                     THEN certified_mail.CM3]) 
apply (possibility, auto) 
done


lemma Gets_imp_Says:
 "[| Gets B X  set evs; evs  certified_mail |] ==> A. Says A B X  set evs"
apply (erule rev_mp)
apply (erule certified_mail.induct, auto)
done


lemma Gets_imp_parts_knows_Spy:
     "[|Gets A X  set evs; evs  certified_mail|] ==> X  parts(spies evs)"
apply (drule Gets_imp_Says, simp)
apply (blast dest: Says_imp_knows_Spy parts.Inj) 
done

lemma CM2_S2TTP_analz_knows_Spy:
 "[|Gets R Agent A, Agent B, em, Number AO, Number cleartext, 
              Nonce q, S2TTP  set evs;
    evs  certified_mail|] 
  ==> S2TTP  analz(spies evs)"
apply (drule Gets_imp_Says, simp) 
apply (blast dest: Says_imp_knows_Spy analz.Inj) 
done

lemmas CM2_S2TTP_parts_knows_Spy = 
    CM2_S2TTP_analz_knows_Spy [THEN analz_subset_parts [THEN subsetD]]

lemma hr_form_lemma [rule_format]:
 "evs  certified_mail
   hr  synth (analz (spies evs)) 
      (S2TTP. Notes TTP Agent R, Agent TTP, S2TTP, pwd, hr
           set evs 
      (clt q S em. hr = Hash Number clt, Nonce q, response S R q, em))"
apply (erule certified_mail.induct)
apply (synth_analz_mono_contra, simp_all, blast+)
done 

textCannot strengthen the first disjunct to termRSpy because
the fakessl rule allows Spy to spoof the sender's name.  Maybe can
strengthen the second disjunct with termRSpy.
lemma hr_form:
 "[|Notes TTP Agent R, Agent TTP, S2TTP, pwd, hr  set evs;
    evs  certified_mail|]
  ==> hr  synth (analz (spies evs)) | 
      (clt q S em. hr = Hash Number clt, Nonce q, response S R q, em)"
by (blast intro: hr_form_lemma) 

lemma Spy_dont_know_private_keys [dest!]:
    "[|Key (privateKey b A)  parts (spies evs); evs  certified_mail|]
     ==> A  bad"
apply (erule rev_mp) 
apply (erule certified_mail.induct, simp_all)
txtFake
apply (blast dest: Fake_parts_insert_in_Un) 
txtMessage 1
apply blast  
txtMessage 3
apply (frule_tac hr_form, assumption)
apply (elim disjE exE) 
apply (simp_all add: parts_insert2) 
 apply (force dest!: parts_insert_subset_Un [THEN [2] rev_subsetD] 
                     analz_subset_parts [THEN subsetD], blast) 
done

lemma Spy_know_private_keys_iff [simp]:
    "evs  certified_mail
     ==> (Key (privateKey b A)  parts (spies evs)) = (A  bad)"
by blast 

lemma Spy_dont_know_TTPKey_parts [simp]:
     "evs  certified_mail ==> Key (privateKey b TTP)  parts(spies evs)" 
by simp

lemma Spy_dont_know_TTPKey_analz [simp]:
     "evs  certified_mail ==> Key (privateKey b TTP)  analz(spies evs)"
by auto

textThus, prove any goal that assumes that termSpy knows a private key
belonging to termTTP
declare Spy_dont_know_TTPKey_parts [THEN [2] rev_notE, elim!]


lemma CM3_k_parts_knows_Spy:
 "[| evs  certified_mail;
     Notes TTP Agent A, Agent TTP,
                 Crypt (pubEK TTP) Agent S, Number AO, Key K, 
                 Agent R, hs, Key (RPwd R), hs  set evs|]
  ==> Key K  parts(spies evs)"
apply (rotate_tac 1)
apply (erule rev_mp)
apply (erule certified_mail.induct, simp_all)
   apply (blast  intro:parts_insertI)
txtFake SSL
apply (blast dest: parts.Body) 
txtMessage 2
apply (blast dest!: Gets_imp_Says elim!: knows_Spy_partsEs)
txtMessage 3
apply (metis parts_insertI)
done

lemma Spy_dont_know_RPwd [rule_format]:
    "evs  certified_mail ==> Key (RPwd A)  parts(spies evs)  A  bad"
apply (erule certified_mail.induct, simp_all) 
txtFake
apply (blast dest: Fake_parts_insert_in_Un) 
txtMessage 1
apply blast  
txtMessage 3
apply (frule CM3_k_parts_knows_Spy, assumption)
apply (frule_tac hr_form, assumption)
apply (elim disjE exE) 
apply (simp_all add: parts_insert2) 
apply (force dest!: parts_insert_subset_Un [THEN [2] rev_subsetD]
                    analz_subset_parts [THEN subsetD])
done


lemma Spy_know_RPwd_iff [simp]:
    "evs  certified_mail ==> (Key (RPwd A)  parts(spies evs)) = (Abad)"
by (auto simp add: Spy_dont_know_RPwd) 

lemma Spy_analz_RPwd_iff [simp]:
    "evs  certified_mail ==> (Key (RPwd A)  analz(spies evs)) = (Abad)"
by (metis Spy_know_RPwd_iff Spy_spies_bad_shrK analz.Inj analz_into_parts)

textUnused, but a guarantee of sorts
theorem CertAutenticity:
     "[|Crypt (priSK TTP) X  parts (spies evs); evs  certified_mail|] 
      ==> A. Says TTP A (Crypt (priSK TTP) X)  set evs"
apply (erule rev_mp)
apply (erule certified_mail.induct, simp_all) 
txtFake
apply (blast dest: Spy_dont_know_private_keys Fake_parts_insert_in_Un)
txtMessage 1
apply blast 
txtMessage 3
apply (frule_tac hr_form, assumption)
apply (elim disjE exE) 
apply (simp_all add: parts_insert2 parts_insert_knows_A) 
 apply (blast dest!: Fake_parts_sing_imp_Un, blast)
done


subsectionProving Confidentiality Results

lemma analz_image_freshK [rule_format]:
 "evs  certified_mail ==>
   K KK. invKey (pubEK TTP)  KK 
          (Key K  analz (Key`KK  (spies evs))) =
          (K  KK | Key K  analz (spies evs))"
apply (erule certified_mail.induct)
apply (drule_tac [6] A=TTP in symKey_neq_priEK) 
apply (erule_tac [6] disjE [OF hr_form]) 
apply (drule_tac [5] CM2_S2TTP_analz_knows_Spy) 
prefer 9
apply (elim exE)
apply (simp_all add: synth_analz_insert_eq
                     subset_trans [OF _ subset_insertI]
                     subset_trans [OF _ Un_upper2] 
                del: image_insert image_Un add: analz_image_freshK_simps)
done


lemma analz_insert_freshK:
  "[| evs  certified_mail;  KAB  invKey (pubEK TTP) |] ==>
      (Key K  analz (insert (Key KAB) (spies evs))) =
      (K = KAB | Key K  analz (spies evs))"
by (simp only: analz_image_freshK analz_image_freshK_simps)

texttermS2TTP must have originated from a valid sender
    provided termK is secure.  Proof is surprisingly hard.

lemma Notes_SSL_imp_used:
     "[|Notes B Agent A, Agent B, X  set evs|] ==> X  used evs"
by (blast dest!: Notes_imp_used)


(*The weaker version, replacing "used evs" by "parts (spies evs)", 
   isn't inductive: message 3 case can't be proved *)
lemma S2TTP_sender_lemma [rule_format]:
 "evs  certified_mail ==>
    Key K  analz (spies evs) 
    (AO. Crypt (pubEK TTP)
           Agent S, Number AO, Key K, Agent R, hs  used evs 
    (m ctxt q. 
        hs = HashNumber ctxt, Nonce q, response S R q, Crypt K (Number m) 
        Says S R
           Agent S, Agent TTP, Crypt K (Number m), Number AO,
             Number ctxt, Nonce q,
             Crypt (pubEK TTP)
              Agent S, Number AO, Key K, Agent R, hs   set evs))" 
apply (erule certified_mail.induct, analz_mono_contra)
apply (drule_tac [5] CM2_S2TTP_parts_knows_Spy, simp)
apply (simp add: used_Nil Crypt_notin_initState, simp_all)
txtFake
apply (blast dest: Fake_parts_sing [THEN subsetD]
             dest!: analz_subset_parts [THEN subsetD])  
txtFake SSL
apply (blast dest: Fake_parts_sing [THEN subsetD]
             dest: analz_subset_parts [THEN subsetD])  
txtMessage 1
apply (clarsimp, blast)
txtMessage 2
apply (simp add: parts_insert2, clarify) 
apply (metis parts_cut Un_empty_left usedI)
txtMessage 3 
apply (blast dest: Notes_SSL_imp_used used_parts_subset_parts) 
done 

lemma S2TTP_sender:
 "[|Crypt (pubEK TTP) Agent S, Number AO, Key K, Agent R, hs  used evs;
    Key K  analz (spies evs);
    evs  certified_mail|]
  ==> m ctxt q. 
        hs = HashNumber ctxt, Nonce q, response S R q, Crypt K (Number m) 
        Says S R
           Agent S, Agent TTP, Crypt K (Number m), Number AO,
             Number ctxt, Nonce q,
             Crypt (pubEK TTP)
              Agent S, Number AO, Key K, Agent R, hs  set evs" 
by (blast intro: S2TTP_sender_lemma) 


textNobody can have used non-existent keys!
lemma new_keys_not_used [simp]:
    "[|Key K  used evs; K  symKeys; evs  certified_mail|]
     ==> K  keysFor (parts (spies evs))"
apply (erule rev_mp) 
apply (erule certified_mail.induct, simp_all) 
txtFake
apply (force dest!: keysFor_parts_insert) 
txtMessage 1
apply blast 
txtMessage 3
apply (frule CM3_k_parts_knows_Spy, assumption)
apply (frule_tac hr_form, assumption) 
apply (force dest!: keysFor_parts_insert)
done


textLess easy to prove termm'=m.  Maybe needs a separate unicity
theorem for ciphertexts of the form termCrypt K (Number m), 
where termK is secure.
lemma Key_unique_lemma [rule_format]:
     "evs  certified_mail ==>
       Key K  analz (spies evs) 
       (m cleartext q hs.
        Says S R
           Agent S, Agent TTP, Crypt K (Number m), Number AO,
             Number cleartext, Nonce q,
             Crypt (pubEK TTP) Agent S, Number AO, Key K, Agent R, hs
           set evs 
       (m' cleartext' q' hs'.
       Says S' R'
           Agent S', Agent TTP, Crypt K (Number m'), Number AO',
             Number cleartext', Nonce q',
             Crypt (pubEK TTP) Agent S', Number AO', Key K, Agent R', hs'
           set evs  R' = R  S' = S  AO' = AO  hs' = hs))" 
apply (erule certified_mail.induct, analz_mono_contra, simp_all)
 prefer 2
 txtMessage 1
 apply (blast dest!: Says_imp_knows_Spy [THEN parts.Inj] new_keys_not_used Crypt_imp_keysFor)
txtFake
apply (auto dest!: usedI S2TTP_sender analz_subset_parts [THEN subsetD]) 
done

textThe key determines the sender, recipient and protocol options.
lemma Key_unique:
      "[|Says S R
           Agent S, Agent TTP, Crypt K (Number m), Number AO,
             Number cleartext, Nonce q,
             Crypt (pubEK TTP) Agent S, Number AO, Key K, Agent R, hs
           set evs;
         Says S' R'
           Agent S', Agent TTP, Crypt K (Number m'), Number AO',
             Number cleartext', Nonce q',
             Crypt (pubEK TTP) Agent S', Number AO', Key K, Agent R', hs'
           set evs;
         Key K  analz (spies evs);
         evs  certified_mail|]
       ==> R' = R  S' = S  AO' = AO  hs' = hs"
by (rule Key_unique_lemma, assumption+)


subsectionThe Guarantees for Sender and Recipient

textA Sender's guarantee:
      If Spy gets the key then termR is bad and termS moreover
      gets his return receipt (and therefore has no grounds for complaint).
theorem S_fairness_bad_R:
      "[|Says S R Agent S, Agent TTP, Crypt K (Number m), Number AO, 
                     Number cleartext, Nonce q, S2TTP  set evs;
         S2TTP = Crypt (pubEK TTP) Agent S, Number AO, Key K, Agent R, hs;
         Key K  analz (spies evs);
         evs  certified_mail;
         SSpy|]
      ==> R  bad  Gets S (Crypt (priSK TTP) S2TTP)  set evs"
apply (erule rev_mp)
apply (erule ssubst)
apply (erule rev_mp)
apply (erule certified_mail.induct, simp_all)
txtFake
apply spy_analz
txtFake SSL
apply spy_analz
txtMessage 3
apply (frule_tac hr_form, assumption)
apply (elim disjE exE) 
apply (simp_all add: synth_analz_insert_eq  
                     subset_trans [OF _ subset_insertI]
                     subset_trans [OF _ Un_upper2] 
                del: image_insert image_Un add: analz_image_freshK_simps) 
apply (simp_all add: symKey_neq_priEK analz_insert_freshK)
apply (blast dest: Notes_SSL_imp_used S2TTP_sender Key_unique)+
done

textConfidentially for the symmetric key
theorem Spy_not_see_encrypted_key:
      "[|Says S R Agent S, Agent TTP, Crypt K (Number m), Number AO, 
                     Number cleartext, Nonce q, S2TTP  set evs;
         S2TTP = Crypt (pubEK TTP) Agent S, Number AO, Key K, Agent R, hs;
         evs  certified_mail;
         SSpy; R  bad|]
      ==> Key K  analz(spies evs)"
by (blast dest: S_fairness_bad_R) 


textAgent termR, who may be the Spy, doesn't receive the key
 until termS has access to the return receipt. 
theorem S_guarantee:
     "[|Says S R Agent S, Agent TTP, Crypt K (Number m), Number AO, 
                    Number cleartext, Nonce q, S2TTP  set evs;
        S2TTP = Crypt (pubEK TTP) Agent S, Number AO, Key K, Agent R, hs;
        Notes R Agent TTP, Agent R, Key K, hs  set evs;
        SSpy;  evs  certified_mail|]
     ==> Gets S (Crypt (priSK TTP) S2TTP)  set evs"
apply (erule rev_mp)
apply (erule ssubst)
apply (erule rev_mp)
apply (erule certified_mail.induct, simp_all)
txtMessage 1
apply (blast dest: Notes_imp_used) 
txtMessage 3
apply (blast dest: Notes_SSL_imp_used S2TTP_sender Key_unique S_fairness_bad_R) 
done


textIf termR sends message 2, and a delivery certificate exists, 
 then termR receives the necessary key.  This result is also important
 to termS, as it confirms the validity of the return receipt.
theorem RR_validity:
  "[|Crypt (priSK TTP) S2TTP  used evs;
     S2TTP = Crypt (pubEK TTP)
               Agent S, Number AO, Key K, Agent R, 
                 Hash Number cleartext, Nonce q, r, em;
     hr = Hash Number cleartext, Nonce q, r, em;
     RSpy;  evs  certified_mail|]
  ==> Notes R Agent TTP, Agent R, Key K, hr  set evs"
apply (erule rev_mp)
apply (erule ssubst)
apply (erule ssubst)
apply (erule certified_mail.induct, simp_all)
txtFake 
apply (blast dest: Fake_parts_sing [THEN subsetD]
             dest!: analz_subset_parts [THEN subsetD])  
txtFake SSL
apply (blast dest: Fake_parts_sing [THEN subsetD]
            dest!: analz_subset_parts [THEN subsetD])  
txtMessage 2
apply (drule CM2_S2TTP_parts_knows_Spy, assumption)
apply (force dest: parts_cut)
txtMessage 3
apply (frule_tac hr_form, assumption)
apply (elim disjE exE, simp_all) 
apply (blast dest: Fake_parts_sing [THEN subsetD]
             dest!: analz_subset_parts [THEN subsetD]) 
done

end