Theory CertifiedEmail

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


header{*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 Un (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