Quelle  CertifiedEmail.thy

(*  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
  fakessl rule allows Spy to spoof the sender's name. Maybe can
  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
  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
  for ciphertexts of the form term‹Crypt K (Number m)›,
  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