(*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 🍋‹S2TTP›while transmitting it and her password to 🍋‹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: 🍋‹🍋‹TTP›simultaneously reveals the key to the recipient and gives a receipt to the sender. The SSL channel does not authenticate the client (🍋‹R›), but 🍋‹TTP› accepts the message only if the given password is that of the claimed sender, 🍋‹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"
(*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
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 🍋‹R≠Spy› because
the fakessl rule allows Spy to spoof the sender's name. Maybe can
strengthen the second disjunct with🍋‹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_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 🍋‹Spy› knows a private key
belonging to🍋‹TTP›\<close> declare Spy_dont_know_TTPKey_parts [THEN [2] rev_notE, elim!]
text‹🍋‹S2TTP›must have originated from a valid sender provided 🍋‹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 🍋‹m'=m›. Maybe needs a separate unicity theorem for ciphertexts of the form 🍋‹Crypt K (Number m)›, where 🍋‹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 🍋‹R›is bad and 🍋‹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 🍋‹R›, who may be the Spy, doesn't receive the key until 🍋‹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 🍋‹R›sends message 2, and a delivery certificate exists, then 🍋‹R›receives the necessary key. This result is also important to 🍋‹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
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.20 Sekunden
(vorverarbeitet am 2026-04-27)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
