(* Title: HOL/Auth/CertifiedEmail ID: $Id: CertifiedEmail.thy,v 1.11 2005/09/28 09:15:33 paulson Exp $ Author: Giampaolo Bella, Christiano Longo and Lawrence C Paulson *) header{*The Certified Electronic Mail Protocol by Abadi et al.*} theory CertifiedEmail imports Public begin syntax TTP :: agent RPwd :: "agent => key" translations "TTP" == "Server " "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.*} constdefs "response" :: "agent => agent => nat => msg" "response S R q == Hash {|Agent S, Key (shrK R), Nonce q|}" consts certified_mail :: "event list set" inductive "certified_mail" intros 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 (frule_tac hr_form, assumption) apply (elim disjE exE) apply (simp_all add: parts_insert2) apply (blast intro: subsetD [OF parts_mono [OF Set.subset_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 (auto simp add: Spy_dont_know_RPwd [OF _ analz_subset_parts [THEN subsetD]]) 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 (drule parts_cut, assumption, simp) apply (blast intro: 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
lemma
[| Key K ∉ used []; K ∈ symKeys |] ==> ∃S2TTP. ∃evs∈certified_mail. Says TTP S (Crypt (priSK TTP) S2TTP) ∈ set evs
lemma Gets_imp_Says:
[| Gets B X ∈ set evs; evs ∈ certified_mail |] ==> ∃A. Says A B X ∈ set evs
lemma Gets_imp_parts_knows_Spy:
[| Gets A X ∈ set evs; evs ∈ certified_mail |] ==> X ∈ parts (knows Spy evs)
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 (knows Spy evs)
lemmas CM2_S2TTP_parts_knows_Spy:
[| Gets R2 {|Agent A2, Agent B2, em2, Number AO2, Number cleartext2, Nonce q2, c|} ∈ set evs2; evs2 ∈ certified_mail |] ==> c ∈ parts (knows Spy evs2)
lemmas CM2_S2TTP_parts_knows_Spy:
[| Gets R2 {|Agent A2, Agent B2, em2, Number AO2, Number cleartext2, Nonce q2, c|} ∈ set evs2; evs2 ∈ certified_mail |] ==> c ∈ parts (knows Spy evs2)
lemma hr_form_lemma:
[| evs ∈ certified_mail; hr ∉ synth (analz (knows Spy evs)); 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|}
lemma hr_form:
[| Notes TTP {|Agent R, Agent TTP, S2TTP, pwd, hr|} ∈ set evs; evs ∈ certified_mail |] ==> hr ∈ synth (analz (knows Spy evs)) ∨ (∃clt q S em. hr = Hash {|Number clt, Nonce q, response S R q, em|})
lemma Spy_dont_know_private_keys:
[| Key (privateKey b A) ∈ parts (knows Spy evs); evs ∈ certified_mail |] ==> A ∈ bad
lemma Spy_know_private_keys_iff:
evs ∈ certified_mail ==> (Key (privateKey b A) ∈ parts (knows Spy evs)) = (A ∈ bad)
lemma Spy_dont_know_TTPKey_parts:
evs ∈ certified_mail ==> Key (privateKey b TTP) ∉ parts (knows Spy evs)
lemma Spy_dont_know_TTPKey_analz:
evs ∈ certified_mail ==> Key (privateKey b TTP) ∉ analz (knows Spy evs)
lemma CM3_k_parts_knows_Spy:
[| evs ∈ certified_mail; Notes TTP {|Agent A, Agent TTP, Crypt (pubK TTP) {|Agent S, Number AO, Key K, Agent R, hs|}, Key (RPwd R), hs|} ∈ set evs |] ==> Key K ∈ parts (knows Spy evs)
lemma Spy_dont_know_RPwd:
[| evs ∈ certified_mail; Key (RPwd A) ∈ parts (knows Spy evs) |] ==> A ∈ bad
lemma Spy_know_RPwd_iff:
evs ∈ certified_mail ==> (Key (RPwd A) ∈ parts (knows Spy evs)) = (A ∈ bad)
lemma Spy_analz_RPwd_iff:
evs ∈ certified_mail ==> (Key (RPwd A) ∈ analz (knows Spy evs)) = (A ∈ bad)
theorem CertAutenticity:
[| Crypt (priSK TTP) X ∈ parts (knows Spy evs); evs ∈ certified_mail |] ==> ∃A. Says TTP A (Crypt (priSK TTP) X) ∈ set evs
lemma analz_image_freshK:
[| evs ∈ certified_mail; priEK TTP ∉ KK |] ==> (Key K ∈ analz (Key ` KK ∪ knows Spy evs)) = (K ∈ KK ∨ Key K ∈ analz (knows Spy evs))
lemma analz_insert_freshK:
[| evs ∈ certified_mail; KAB ≠ priEK TTP |] ==> (Key K ∈ analz (insert (Key KAB) (knows Spy evs))) = (K = KAB ∨ Key K ∈ analz (knows Spy evs))
lemma Notes_SSL_imp_used:
Notes B {|Agent A, Agent B, X|} ∈ set evs ==> X ∈ used evs
lemma S2TTP_sender_lemma:
[| evs ∈ certified_mail; Key K ∉ analz (knows Spy evs); Crypt (pubK 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 (pubK TTP) {|Agent S, Number AO, Key K, Agent R, hs|}|} ∈ set evs
lemma S2TTP_sender:
[| Crypt (pubK TTP) {|Agent S, Number AO, Key K, Agent R, hs|} ∈ used evs; Key K ∉ analz (knows Spy 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 (pubK TTP) {|Agent S, Number AO, Key K, Agent R, hs|}|} ∈ set evs
lemma new_keys_not_used:
[| Key K ∉ used evs; K ∈ symKeys; evs ∈ certified_mail |] ==> K ∉ keysFor (parts (knows Spy evs))
lemma Key_unique_lemma:
[| evs ∈ certified_mail; Key K ∉ analz (knows Spy evs); Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, Number cleartext, Nonce q, Crypt (pubK 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 (pubK TTP) {|Agent S', Number AO', Key K, Agent R', hs'|}|} ∈ set evs |] ==> R' = R ∧ S' = S ∧ AO' = AO ∧ hs' = hs
lemma Key_unique:
[| Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, Number cleartext, Nonce q, Crypt (pubK 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 (pubK TTP) {|Agent S', Number AO', Key K, Agent R', hs'|}|} ∈ set evs; Key K ∉ analz (knows Spy evs); evs ∈ certified_mail |] ==> R' = R ∧ S' = S ∧ AO' = AO ∧ hs' = hs
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 (pubK TTP) {|Agent S, Number AO, Key K, Agent R, hs|}; Key K ∈ analz (knows Spy evs); evs ∈ certified_mail; S ≠ Spy |] ==> R ∈ bad ∧ Gets S (Crypt (priSK TTP) S2TTP) ∈ set evs
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 (pubK TTP) {|Agent S, Number AO, Key K, Agent R, hs|}; evs ∈ certified_mail; S ≠ Spy; R ∉ bad |] ==> Key K ∉ analz (knows Spy evs)
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 (pubK 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
theorem RR_validity:
[| Crypt (priSK TTP) S2TTP ∈ used evs; S2TTP = Crypt (pubK 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