Theory CertifiedEmail

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

section‹The 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

text‹We 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 = Hash⦃Number 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 \<^term>‹S2TTP› while transmitting it and her
     password to \<^term>‹TTP› 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: ― ‹\<^term>‹TTP› simultaneously reveals the key to the recipient and gives
         a receipt to the sender.  The SSL channel does not authenticate 
         the client (\<^term>‹R›), but \<^term>‹TTP› accepts the message only 
         if the given password is that of the claimed sender, \<^term>‹R›.
         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 

text‹Cannot strengthen the first disjunct to \<^term>‹R≠Spy› because
the fakessl rule allows Spy to spoof the sender's name.  Maybe can
strengthen the second disjunct with \<^term>‹R≠Spy›.›
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)
txt‹Fake›
apply (blast dest: Fake_parts_insert_in_Un) 
txt‹Message 1›
apply blast  
txt‹Message 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

text‹Thus, prove any goal that assumes that \<^term>‹Spy› knows a private key
belonging to \<^term>‹TTP››
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)
txt‹Fake SSL›
apply (blast dest: parts.Body) 
txt‹Message 2›
apply (blast dest!: Gets_imp_Says elim!: knows_Spy_partsEs)
txt‹Message 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) 
txt‹Fake›
apply (blast dest: Fake_parts_insert_in_Un) 
txt‹Message 1›
apply blast  
txt‹Message 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)) = (A∈bad)"
by (auto simp add: Spy_dont_know_RPwd) 

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

text‹Unused, 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) 
txt‹Fake›
apply (blast dest: Spy_dont_know_private_keys Fake_parts_insert_in_Un)
txt‹Message 1›
apply blast 
txt‹Message 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


subsection‹Proving 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)

text‹\<^term>‹S2TTP› must have originated from a valid sender
    provided \<^term>‹K› 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 = Hash⦃Number 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)
txt‹Fake›
apply (blast dest: Fake_parts_sing [THEN subsetD]
             dest!: analz_subset_parts [THEN subsetD])  
txt‹Fake SSL›
apply (blast dest: Fake_parts_sing [THEN subsetD]
             dest: analz_subset_parts [THEN subsetD])  
txt‹Message 1›
apply (clarsimp, blast)
txt‹Message 2›
apply (simp add: parts_insert2, clarify) 
apply (metis parts_cut Un_empty_left usedI)
txt‹Message 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 = Hash⦃Number 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) 


text‹Nobody 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) 
txt‹Fake›
apply (force dest!: keysFor_parts_insert) 
txt‹Message 1›
apply blast 
txt‹Message 3›
apply (frule CM3_k_parts_knows_Spy, assumption)
apply (frule_tac hr_form, assumption) 
apply (force dest!: keysFor_parts_insert)
done


text‹Less easy to prove \<^term>‹m'=m›.  Maybe needs a separate unicity
theorem for ciphertexts of the form \<^term>‹Crypt K (Number m)›, 
where \<^term>‹K› 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
 txt‹Message 1›
 apply (blast dest!: Says_imp_knows_Spy [THEN parts.Inj] new_keys_not_used Crypt_imp_keysFor)
txt‹Fake›
apply (auto dest!: usedI S2TTP_sender analz_subset_parts [THEN subsetD]) 
done

text‹The 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+)


subsection‹The Guarantees for Sender and Recipient›

text‹A Sender's guarantee:
      If Spy gets the key then \<^term>‹R› is bad and \<^term>‹S› 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;
         S≠Spy⟧
      ⟹ 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)
txt‹Fake›
apply spy_analz
txt‹Fake SSL›
apply spy_analz
txt‹Message 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

text‹Confidentially 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;
         S≠Spy; R ∉ bad⟧
      ⟹ Key K ∉ analz(spies evs)"
by (blast dest: S_fairness_bad_R) 


text‹Agent \<^term>‹R›, who may be the Spy, doesn't receive the key
 until \<^term>‹S› 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;
        S≠Spy;  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)
txt‹Message 1›
apply (blast dest: Notes_imp_used) 
txt‹Message 3›
apply (blast dest: Notes_SSL_imp_used S2TTP_sender Key_unique S_fairness_bad_R) 
done


text‹If \<^term>‹R› sends message 2, and a delivery certificate exists, 
 then \<^term>‹R› receives the necessary key.  This result is also important
 to \<^term>‹S›, 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⦄;
     R≠Spy;  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)
txt‹Fake› 
apply (blast dest: Fake_parts_sing [THEN subsetD]
             dest!: analz_subset_parts [THEN subsetD])  
txt‹Fake SSL›
apply (blast dest: Fake_parts_sing [THEN subsetD]
            dest!: analz_subset_parts [THEN subsetD])  
txt‹Message 2›
apply (drule CM2_S2TTP_parts_knows_Spy, assumption)
apply (force dest: parts_cut)
txt‹Message 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