Changes required by the certified email protocol
Public-key model now provides separate signature/encryption keys and also
long-term symmetric keys.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/CertifiedEmail.thy Fri Apr 25 11:18:14 2003 +0200
@@ -0,0 +1,522 @@
+(* Title: HOL/Auth/CertifiedEmail
+ ID: $Id$
+ Author: Giampaolo Bella, Christiano Longo and Lawrence C Paulson
+
+The certified electronic mail protocol by Abadi et al.
+*)
+
+theory CertifiedEmail = Public:
+
+syntax
+ TTP :: agent
+ RPwd :: "agent => key"
+ TTPDecKey :: key
+ TTPEncKey :: key
+ TTPSigKey :: key
+ TTPVerKey :: key
+
+translations
+ "TTP" == "Server"
+ "RPwd" == "shrK"
+ "TTPDecKey" == "priEK Server"
+ "TTPEncKey" == "pubEK Server"
+ "TTPSigKey" == "priSK Server"
+ "TTPVerKey" == "pubSK Server"
+
+
+(*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*}
+ "[] \<in> certified_mail"
+
+Fake: --{*The Spy may say anything he can say. The sender field is correct,
+ but agents don't use that information.*}
+ "[| evsf \<in> certified_mail; X \<in> synth(analz(knows Spy evsf))|]
+ ==> Says Spy B X #evsf \<in> 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 \<in> certified_mail; X \<in> synth(analz(knows Spy evsfssl))|]
+ ==> Notes TTP {|Agent Spy, Agent TTP, X|} # evsfssl \<in> certified_mail"
+
+CM1: --{*The sender approaches the recipient. The message is a number.*}
+"[|evs1 \<in> certified_mail;
+ Key K \<notin> used evs1;
+ K \<in> symKeys;
+ Nonce q \<notin> used evs1;
+ hs = Hash {|Number cleartext, Nonce q, response S R q, Crypt K (Number m)|};
+ S2TTP = Crypt TTPEncKey {|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
+ \<in> certified_mail"
+
+CM2: --{*The recipient records @{term S2TTP'} while transmitting it and her
+ password to @{term TTP} over an SSL channel.*}
+"[|evs2 \<in> certified_mail;
+ Gets R {|Agent S, Agent TTP, em', Number BothAuth, Number cleartext',
+ Nonce q', S2TTP'|} \<in> set evs2;
+ TTP \<noteq> R;
+ hr = Hash {|Number cleartext', Nonce q', response S R q', em'|} |]
+ ==>
+ Notes TTP {|Agent R, Agent TTP, S2TTP', Key(RPwd R), hr|} # evs2
+ \<in> 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 \<in> certified_mail;
+ Notes TTP {|Agent R', Agent TTP, S2TTP'', Key(RPwd R'), hr'|} \<in> set evs3;
+ S2TTP'' = Crypt TTPEncKey
+ {|Agent S, Number BothAuth, Key k', Agent R', hs'|};
+ TTP \<noteq> R'; hs' = hr'; k' \<in> symKeys|]
+ ==>
+ Notes R' {|Agent TTP, Agent R', Key k', hr'|} #
+ Says TTP S (Crypt TTPSigKey S2TTP'') # evs3 \<in> certified_mail"
+
+Reception:
+ "[|evsr \<in> certified_mail; Says A B X \<in> set evsr|]
+ ==> Gets B X#evsr \<in> certified_mail"
+
+
+axioms
+ (*Unlike the corresponding property of nonces, this cannot be proved.
+ We have infinitely many agents and there is nothing to stop their
+ long-term keys from exhausting all the natural numbers. The axiom
+ assumes that their keys are dispersed so as to leave room for infinitely
+ many fresh session keys. We could, alternatively, restrict agents to
+ an unspecified finite number. TOO STRONG. REPLACE "used evs" BY
+ used []*)
+ Key_supply_ax: "finite KK ==> \<exists>K\<in>symKeys. K \<notin> KK & Key K \<notin> used evs"
+
+
+lemma Key_supply1: "\<exists>K\<in>symKeys. Key K \<notin> used evs"
+by (rule Finites.emptyI [THEN Key_supply_ax, THEN bexE], blast)
+
+(*A "possibility property": there are traces that reach the end*)
+lemma "\<exists>S2TTP. \<exists>evs \<in> certified_mail.
+ Says TTP S (Crypt TTPSigKey S2TTP) \<in> set evs"
+apply (rule bexE [OF Key_supply1])
+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], possibility, possibility)
+apply auto
+done
+
+
+lemma Gets_imp_Says:
+ "[| Gets B X \<in> set evs; evs \<in> certified_mail |] ==> \<exists>A. Says A B X \<in> set evs"
+apply (erule rev_mp)
+apply (erule certified_mail.induct, auto)
+done
+
+
+lemma Gets_imp_parts_knows_Spy:
+ "[|Gets A X \<in> set evs; evs \<in> certified_mail|] ==> X \<in> 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|} \<in> set evs;
+ evs \<in> certified_mail|]
+ ==> S2TTP \<in> analz(knows Spy 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 \<in> certified_mail
+ ==> hr \<notin> synth (analz (knows Spy evs)) -->
+ (\<forall>S2TTP. Notes TTP {|Agent R, Agent TTP, S2TTP, pwd, hr|}
+ \<in> set evs -->
+ (\<exists>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\<noteq>Spy"} because
+the fakessl rule allows Spy to spoof the sender's name. Maybe can
+strengthen the second disjunct with @{term "R\<noteq>Spy"}.*}
+lemma hr_form:
+ "[|Notes TTP {|Agent R, Agent TTP, S2TTP, pwd, hr|} \<in> set evs;
+ evs \<in> certified_mail|]
+ ==> hr \<in> synth (analz (knows Spy evs)) |
+ (\<exists>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 [rule_format]:
+ "evs \<in> certified_mail
+ ==> Key (privateKey b A) \<in> parts (spies evs) --> A \<in> bad"
+apply (erule certified_mail.induct, simp_all)
+txt{*Fake*}
+apply (blast dest: Fake_parts_insert[THEN subsetD]
+ analz_subset_parts[THEN subsetD])
+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 \<in> certified_mail
+ ==> (Key (privateKey b A) \<in> parts (spies evs)) = (A \<in> bad)"
+by (blast intro: Spy_dont_know_private_keys parts.Inj)
+
+
+lemma CM3_k_parts_knows_Spy:
+ "[| evs \<in> certified_mail;
+ Notes TTP {|Agent A, Agent TTP,
+ Crypt TTPEncKey {|Agent S, Number AO, Key K,
+ Agent R, hs|}, Key (RPwd R), hs|} \<in> set evs|]
+ ==> Key K \<in> 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: analz_subset_parts[THEN subsetD] parts.Body)
+txt{*Message 2*}
+apply (blast dest!: Says_imp_knows_Spy [THEN parts.Inj] 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 \<in> certified_mail ==> Key (RPwd A) \<in> parts(spies evs) --> A \<in> bad"
+apply (erule certified_mail.induct, simp_all)
+txt{*Fake*}
+apply (blast dest: Fake_parts_insert[THEN subsetD]
+ analz_subset_parts[THEN subsetD])
+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 \<in> certified_mail ==> (Key (RPwd A) \<in> parts(knows Spy evs)) = (A\<in>bad)"
+by (auto simp add: Spy_dont_know_RPwd)
+
+lemma Spy_analz_RPwd_iff [simp]:
+ "evs \<in> certified_mail ==> (Key (RPwd A) \<in> analz(knows Spy evs)) = (A\<in>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 TTPSigKey X \<in> parts (spies evs); evs \<in> certified_mail|]
+ ==> \<exists>A. Says TTP A (Crypt TTPSigKey X) \<in> 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[THEN subsetD]
+ analz_subset_parts[THEN subsetD])
+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_dont_know_TTPDecKey [simp]:
+ "evs \<in> certified_mail ==> Key TTPDecKey \<notin> parts(knows Spy evs)"
+by auto
+
+lemma Spy_dont_know_TTPDecKey_analz [simp]:
+ "evs \<in> certified_mail ==> Key TTPDecKey \<notin> analz(knows Spy evs)"
+by (force dest!: analz_subset_parts[THEN subsetD])
+
+
+lemma Spy_knows_TTPVerKey [simp]:
+ "Key (invKey TTPSigKey) \<in> analz(knows Spy evs)"
+by simp
+
+
+subsection{*Proving Confidentiality Results*}
+
+lemma analz_image_freshK [rule_format]:
+ "evs \<in> certified_mail ==>
+ \<forall>K KK. invKey TTPEncKey \<notin> KK -->
+ (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
+ (K \<in> KK | Key K \<in> analz (knows Spy 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 \<in> certified_mail; KAB \<noteq> invKey TTPEncKey |] ==>
+ (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
+ (K = KAB | Key K \<in> analz (knows Spy 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|} \<in> set evs|] ==> X \<in> used evs"
+by (blast dest!: Notes_imp_used)
+
+
+(*The weaker version, replacing "used evs" by "parts (knows Spy evs)",
+ isn't inductive: message 3 case can't be proved *)
+lemma S2TTP_sender_lemma [rule_format]:
+ "evs \<in> certified_mail ==>
+ Key K \<notin> analz (knows Spy evs) -->
+ (\<forall>AO. Crypt TTPEncKey
+ {|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs -->
+ (\<exists>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 TTPEncKey
+ {|Agent S, Number AO, Key K, Agent R, hs |}|} \<in> 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
+apply blast
+txt{*Message 2*}
+apply (simp add: parts_insert2, clarify)
+apply (drule parts_cut, assumption, simp)
+apply (blast dest: parts_knows_Spy_subset_used [THEN subsetD])
+txt{*Message 3*}
+apply (blast dest: Notes_SSL_imp_used used_parts_subset_parts)
+done
+
+lemma S2TTP_sender:
+ "[|Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs;
+ Key K \<notin> analz (knows Spy evs);
+ evs \<in> certified_mail|]
+ ==> \<exists>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 TTPEncKey
+ {|Agent S, Number AO, Key K, Agent R, hs |}|} \<in> set evs"
+by (blast intro: S2TTP_sender_lemma)
+
+
+text{*Nobody can have used non-existent keys!*}
+lemma new_keys_not_used [rule_format, simp]:
+ "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> certified_mail|]
+ ==> K \<notin> 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 fror ciphertexts of the form @{term "Crypt K (Number m)"},
+where @{term K} is secure.*}
+lemma Key_unique_lemma [rule_format]:
+ "evs \<in> certified_mail ==>
+ Key K \<notin> analz (knows Spy evs) -->
+ (\<forall>m cleartext q hs.
+ Says S R
+ {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
+ Number cleartext, Nonce q,
+ Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|}|}
+ \<in> set evs -->
+ (\<forall>m' cleartext' q' hs'.
+ Says S' R'
+ {|Agent S', Agent TTP, Crypt K (Number m'), Number AO',
+ Number cleartext', Nonce q',
+ Crypt TTPEncKey {|Agent S', Number AO', Key K, Agent R', hs'|}|}
+ \<in> set evs --> R' = R & S' = S & AO' = AO & hs' = hs))"
+apply (erule certified_mail.induct, analz_mono_contra, simp_all)
+txt{*Fake*}
+apply (blast dest!: usedI S2TTP_sender analz_subset_parts[THEN subsetD])
+txt{*Message 1*}
+apply (blast dest!: Says_imp_knows_Spy [THEN parts.Inj] new_keys_not_used Crypt_imp_keysFor)
+done
+
+text{*The key determines the sender, recipient and protocol options.*}
+theorem Key_unique:
+ "[|Says S R
+ {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
+ Number cleartext, Nonce q,
+ Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|}|}
+ \<in> set evs;
+ Says S' R'
+ {|Agent S', Agent TTP, Crypt K (Number m'), Number AO',
+ Number cleartext', Nonce q',
+ Crypt TTPEncKey {|Agent S', Number AO', Key K, Agent R', hs'|}|}
+ \<in> set evs;
+ Key K \<notin> analz (knows Spy evs);
+ evs \<in> certified_mail|]
+ ==> R' = R & S' = S & AO' = AO & hs' = hs"
+by (rule Key_unique_lemma, assumption+)
+
+text{*If Spy gets the key then @{term R} is bad and also @{term S} at least
+ gets his return receipt (and therefore has no grounds for complaint).*}
+lemma Spy_see_encrypted_key_imp:
+ "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
+ Number cleartext, Nonce q, S2TTP|} \<in> set evs;
+ Key K \<in> analz(knows Spy evs);
+ S2TTP = Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|};
+ evs \<in> certified_mail;
+ S\<noteq>Spy|]
+ ==> R \<in> bad & Says TTP S (Crypt TTPSigKey S2TTP) \<in> set evs"
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule ssubst)
+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|} \<in> set evs;
+ S2TTP = Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|};
+ evs \<in> certified_mail;
+ S\<noteq>Spy; R \<notin> bad|]
+ ==> Key K \<notin> analz(knows Spy evs)"
+by (blast dest: Spy_see_encrypted_key_imp)
+
+
+subsection{*The Guarantees for Sender and Recipient*}
+
+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:
+ "[|Notes R {|Agent TTP, Agent R, Key K, hs|} \<in> set evs;
+ Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
+ Number cleartext, Nonce q, S2TTP|} \<in> set evs;
+ S2TTP = Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|};
+ hs = Hash {|Number cleartext, Nonce q, response S R q,
+ Crypt K (Number m)|};
+ S\<noteq>Spy; evs \<in> certified_mail|]
+ ==> Says TTP S (Crypt TTPSigKey S2TTP) \<in> set evs"
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule ssubst)
+apply (erule ssubst)
+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
+ Spy_see_encrypted_key_imp)
+done
+
+
+lemma Says_TTP_imp_Notes:
+ "[|Says TTP S (Crypt TTPSigKey S2TTP) \<in> set evs;
+ S2TTP = Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R,
+ Hash {|Number cleartext, Nonce q, r, em|}|};
+ evs \<in> certified_mail|]
+ ==> Notes TTP
+ {|Agent R, Agent TTP, S2TTP, Key (RPwd R),
+ Hash {|Number cleartext, Nonce q, r, em|}|}
+ \<in> set evs"
+apply (erule rev_mp)
+apply (erule ssubst)
+apply (erule certified_mail.induct, simp_all)
+done
+
+
+
+text{*Recipient's guarantee: if @{term R} sends message 2, and
+ @{term S} gets a delivery certificate, then @{term R}
+ receives the necessary key.*}
+theorem R_guarantee:
+ "[|Notes TTP {|Agent R, Agent TTP, S2TTP, Key(RPwd R), hr|} \<in> set evs;
+ Says TTP S (Crypt TTPSigKey S2TTP) \<in> set evs;
+ S2TTP = Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R,
+ Hash {|Number cleartext, Nonce q, r, em|}|};
+ hr = Hash {|Number cleartext, Nonce q, r, em|};
+ R\<noteq>Spy; evs \<in> certified_mail|]
+ ==> Notes R {|Agent TTP, Agent R, Key K, hr|} \<in> set evs"
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule ssubst)
+apply (erule ssubst)
+apply (erule certified_mail.induct, simp_all)
+txt{*Message 2*}
+apply clarify
+apply (drule Says_TTP_imp_Notes [OF _ refl], assumption)
+apply simp
+done
+
+end
--- a/src/HOL/Auth/Event.thy Wed Apr 23 18:09:48 2003 +0200
+++ b/src/HOL/Auth/Event.thy Fri Apr 25 11:18:14 2003 +0200
@@ -37,8 +37,8 @@
axioms
(*Spy has access to his own key for spoof messages, but Server is secure*)
- Spy_in_bad [iff] : "Spy \\<in> bad"
- Server_not_bad [iff] : "Server \\<notin> bad"
+ Spy_in_bad [iff] : "Spy \<in> bad"
+ Server_not_bad [iff] : "Server \<notin> bad"
primrec
knows_Nil: "knows A [] = initState A"
@@ -49,7 +49,7 @@
Says A' B X => insert X (knows Spy evs)
| Gets A' X => knows Spy evs
| Notes A' X =>
- if A' \\<in> bad then insert X (knows Spy evs) else knows Spy evs)
+ if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs)
else
(case ev of
Says A' B X =>
@@ -97,9 +97,53 @@
use "Event_lemmas.ML"
+lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
+by (induct e, auto simp: knows_Cons)
+
+lemma initState_subset_knows: "initState A <= knows A evs"
+apply (induct_tac evs)
+apply (simp add: );
+apply (blast intro: knows_subset_knows_Cons [THEN subsetD])
+done
+
+
+(*For proving new_keys_not_used*)
+lemma keysFor_parts_insert:
+ "[| K \<in> keysFor (parts (insert X G)); X \<in> synth (analz H) |] \
+\ ==> K \<in> keysFor (parts (G Un H)) | Key (invKey K) \<in> parts H";
+by (force
+ dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
+ analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD]
+ intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD])
+
method_setup analz_mono_contra = {*
Method.no_args
(Method.METHOD (fn facts => REPEAT_FIRST analz_mono_contra_tac)) *}
- "for proving theorems of the form X \\<notin> analz (knows Spy evs) --> P"
+ "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
+
+subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
+
+ML
+{*
+val synth_analz_mono = thm "synth_analz_mono";
+
+val synth_analz_mono_contra_tac =
+ let val syan_impI = inst "P" "?Y ~: synth (analz (knows Spy ?evs))" impI
+ in
+ rtac syan_impI THEN'
+ REPEAT1 o
+ (dresolve_tac
+ [knows_Spy_subset_knows_Spy_Says RS synth_analz_mono RS contra_subsetD,
+ knows_Spy_subset_knows_Spy_Notes RS synth_analz_mono RS contra_subsetD,
+ knows_Spy_subset_knows_Spy_Gets RS synth_analz_mono RS contra_subsetD])
+ THEN'
+ mp_tac
+ end;
+*}
+
+method_setup synth_analz_mono_contra = {*
+ Method.no_args
+ (Method.METHOD (fn facts => REPEAT_FIRST synth_analz_mono_contra_tac)) *}
+ "for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P"
end
--- a/src/HOL/Auth/Message.thy Wed Apr 23 18:09:48 2003 +0200
+++ b/src/HOL/Auth/Message.thy Fri Apr 25 11:18:14 2003 +0200
@@ -135,6 +135,25 @@
use "Message_lemmas.ML"
+lemma Crypt_notin_image_Key [simp]: "Crypt K X \<notin> Key ` A"
+by auto
+
+lemma Hash_notin_image_Key [simp] :"Hash X \<notin> Key ` A"
+by auto
+
+lemma synth_analz_mono: "G<=H ==> synth (analz(G)) <= synth (analz(H))"
+by (simp add: synth_mono analz_mono)
+
+lemma Fake_analz_eq [simp]:
+ "X \<in> synth(analz H) ==> synth (analz (insert X H)) = synth (analz H)"
+apply (drule Fake_analz_insert[of _ _ "H"])
+apply (simp add: synth_increasing[THEN Un_absorb2])
+apply (drule synth_mono)
+apply (simp add: synth_idem)
+apply (blast intro: synth_analz_mono [THEN [2] rev_subsetD])
+done
+
+
lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
lemma Fake_parts_insert_in_Un:
@@ -142,6 +161,25 @@
==> Z \<in> synth (analz H) \<union> parts H";
by (blast dest: Fake_parts_insert [THEN subsetD, dest])
+text{*Two generalizations of @{text analz_insert_eq}*}
+lemma gen_analz_insert_eq [rule_format]:
+ "X \<in> analz H ==> ALL G. H \<subseteq> G --> analz (insert X G) = analz G";
+by (blast intro: analz_cut analz_insertI analz_mono [THEN [2] rev_subsetD])
+
+lemma synth_analz_insert_eq [rule_format]:
+ "X \<in> synth (analz H)
+ ==> ALL G. H \<subseteq> G --> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)";
+apply (erule synth.induct)
+apply (simp_all add: gen_analz_insert_eq subset_trans [OF _ subset_insertI])
+done
+
+lemma Fake_parts_sing:
+ "X \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) Un parts H";
+apply (rule subset_trans)
+ apply (erule_tac [2] Fake_parts_insert)
+apply (simp add: parts_mono)
+done
+
method_setup spy_analz = {*
Method.ctxt_args (fn ctxt =>
Method.METHOD (fn facts =>
--- a/src/HOL/Auth/NS_Public.thy Wed Apr 23 18:09:48 2003 +0200
+++ b/src/HOL/Auth/NS_Public.thy Fri Apr 25 11:18:14 2003 +0200
@@ -24,21 +24,21 @@
(*Alice initiates a protocol run, sending a nonce to Bob*)
NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk>
- \<Longrightarrow> Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
+ \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
# evs1 \<in> ns_public"
(*Bob responds to Alice's message with a further nonce*)
NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2;
- Says A' B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
- \<Longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>)
+ Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
+ \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>)
# evs2 \<in> ns_public"
(*Alice proves her existence by sending NB back to Bob.*)
NS3: "\<lbrakk>evs3 \<in> ns_public;
- Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
- Says B' A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>)
+ Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
+ Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>)
\<in> set evs3\<rbrakk>
- \<Longrightarrow> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 \<in> ns_public"
+ \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
declare knows_Spy_partsEs [elim]
declare analz_subset_parts [THEN subsetD, dest]
@@ -46,7 +46,7 @@
declare image_eq_UN [simp] (*accelerates proofs involving nested images*)
(*A "possibility property": there are traces that reach the end*)
-lemma "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubK B) (Nonce NB)) \<in> set evs"
+lemma "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2] ns_public.Nil [THEN ns_public.NS1, THEN ns_public.NS2,
THEN ns_public.NS3])
@@ -59,12 +59,12 @@
sends messages containing X! **)
(*Spy never sees another agent's private key! (unless it's bad at start)*)
-lemma Spy_see_priK [simp]:
- "evs \<in> ns_public \<Longrightarrow> (Key (priK A) \<in> parts (spies evs)) = (A \<in> bad)"
+lemma Spy_see_priEK [simp]:
+ "evs \<in> ns_public \<Longrightarrow> (Key (priEK A) \<in> parts (spies evs)) = (A \<in> bad)"
by (erule ns_public.induct, auto)
-lemma Spy_analz_priK [simp]:
- "evs \<in> ns_public \<Longrightarrow> (Key (priK A) \<in> analz (spies evs)) = (A \<in> bad)"
+lemma Spy_analz_priEK [simp]:
+ "evs \<in> ns_public \<Longrightarrow> (Key (priEK A) \<in> analz (spies evs)) = (A \<in> bad)"
by auto
@@ -75,8 +75,8 @@
is secret. (Honest users generate fresh nonces.)*)
lemma no_nonce_NS1_NS2 [rule_format]:
"evs \<in> ns_public
- \<Longrightarrow> Crypt (pubK C) \<lbrace>NA', Nonce NA, Agent D\<rbrace> \<in> parts (spies evs) \<longrightarrow>
- Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>
+ \<Longrightarrow> Crypt (pubEK C) \<lbrace>NA', Nonce NA, Agent D\<rbrace> \<in> parts (spies evs) \<longrightarrow>
+ Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>
Nonce NA \<in> analz (spies evs)"
apply (erule ns_public.induct, simp_all)
apply (blast intro: analz_insertI)+
@@ -84,8 +84,8 @@
(*Unicity for NS1: nonce NA identifies agents A and B*)
lemma unique_NA:
- "\<lbrakk>Crypt(pubK B) \<lbrace>Nonce NA, Agent A \<rbrace> \<in> parts(spies evs);
- Crypt(pubK B') \<lbrace>Nonce NA, Agent A'\<rbrace> \<in> parts(spies evs);
+ "\<lbrakk>Crypt(pubEK B) \<lbrace>Nonce NA, Agent A \<rbrace> \<in> parts(spies evs);
+ Crypt(pubEK B') \<lbrace>Nonce NA, Agent A'\<rbrace> \<in> parts(spies evs);
Nonce NA \<notin> analz (spies evs); evs \<in> ns_public\<rbrakk>
\<Longrightarrow> A=A' \<and> B=B'"
apply (erule rev_mp, erule rev_mp, erule rev_mp)
@@ -99,7 +99,7 @@
The major premise "Says A B ..." makes it a dest-rule, so we use
(erule rev_mp) rather than rule_format. *)
theorem Spy_not_see_NA:
- "\<lbrakk>Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs;
+ "\<lbrakk>Says A B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
\<Longrightarrow> Nonce NA \<notin> analz (spies evs)"
apply (erule rev_mp)
@@ -112,28 +112,28 @@
to start a run, then B has sent message 2.*)
lemma A_trusts_NS2_lemma [rule_format]:
"\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
- \<Longrightarrow> Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace> \<in> parts (spies evs) \<longrightarrow>
- Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs \<longrightarrow>
- Says B A (Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs"
+ \<Longrightarrow> Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace> \<in> parts (spies evs) \<longrightarrow>
+ Says A B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs \<longrightarrow>
+ Says B A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs"
apply (erule ns_public.induct, simp_all)
(*Fake, NS1*)
apply (blast dest: Spy_not_see_NA)+
done
theorem A_trusts_NS2:
- "\<lbrakk>Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs;
- Says B' A (Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs;
+ "\<lbrakk>Says A B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs;
+ Says B' A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
- \<Longrightarrow> Says B A (Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs"
+ \<Longrightarrow> Says B A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs"
by (blast intro: A_trusts_NS2_lemma)
(*If the encrypted message appears then it originated with Alice in NS1*)
lemma B_trusts_NS1 [rule_format]:
"evs \<in> ns_public
- \<Longrightarrow> Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>
+ \<Longrightarrow> Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>
Nonce NA \<notin> analz (spies evs) \<longrightarrow>
- Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs"
+ Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs"
apply (erule ns_public.induct, simp_all)
(*Fake*)
apply (blast intro!: analz_insertI)
@@ -148,8 +148,8 @@
[proof closely follows that for unique_NA] *)
lemma unique_NB [dest]:
- "\<lbrakk>Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace> \<in> parts(spies evs);
- Crypt(pubK A') \<lbrace>Nonce NA', Nonce NB, Agent B'\<rbrace> \<in> parts(spies evs);
+ "\<lbrakk>Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace> \<in> parts(spies evs);
+ Crypt(pubEK A') \<lbrace>Nonce NA', Nonce NB, Agent B'\<rbrace> \<in> parts(spies evs);
Nonce NB \<notin> analz (spies evs); evs \<in> ns_public\<rbrakk>
\<Longrightarrow> A=A' \<and> NA=NA' \<and> B=B'"
apply (erule rev_mp, erule rev_mp, erule rev_mp)
@@ -161,7 +161,7 @@
(*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*)
theorem Spy_not_see_NB [dest]:
- "\<lbrakk>Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs;
+ "\<lbrakk>Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
\<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
apply (erule rev_mp)
@@ -174,16 +174,16 @@
in message 2, then A has sent message 3.*)
lemma B_trusts_NS3_lemma [rule_format]:
"\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> \<Longrightarrow>
- Crypt (pubK B) (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
- Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs \<longrightarrow>
- Says A B (Crypt (pubK B) (Nonce NB)) \<in> set evs"
+ Crypt (pubEK B) (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
+ Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs \<longrightarrow>
+ Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs"
by (erule ns_public.induct, auto)
theorem B_trusts_NS3:
- "\<lbrakk>Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs;
- Says A' B (Crypt (pubK B) (Nonce NB)) \<in> set evs;
+ "\<lbrakk>Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs;
+ Says A' B (Crypt (pubEK B) (Nonce NB)) \<in> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
- \<Longrightarrow> Says A B (Crypt (pubK B) (Nonce NB)) \<in> set evs"
+ \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs"
by (blast intro: B_trusts_NS3_lemma)
(*** Overall guarantee for B ***)
@@ -193,9 +193,9 @@
NA, then A initiated the run using NA.*)
theorem B_trusts_protocol:
"\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> \<Longrightarrow>
- Crypt (pubK B) (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
- Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs \<longrightarrow>
- Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs"
+ Crypt (pubEK B) (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
+ Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs \<longrightarrow>
+ Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs"
by (erule ns_public.induct, auto)
end
--- a/src/HOL/Auth/NS_Public_Bad.thy Wed Apr 23 18:09:48 2003 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.thy Fri Apr 25 11:18:14 2003 +0200
@@ -28,20 +28,20 @@
(*Alice initiates a protocol run, sending a nonce to Bob*)
NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk>
- \<Longrightarrow> Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
+ \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
# evs1 \<in> ns_public"
(*Bob responds to Alice's message with a further nonce*)
NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2;
- Says A' B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
- \<Longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
+ Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
+ \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
# evs2 \<in> ns_public"
(*Alice proves her existence by sending NB back to Bob.*)
NS3: "\<lbrakk>evs3 \<in> ns_public;
- Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
- Says B' A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
- \<Longrightarrow> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 \<in> ns_public"
+ Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
+ Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
+ \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
declare knows_Spy_partsEs [elim]
declare analz_subset_parts [THEN subsetD, dest]
@@ -49,7 +49,7 @@
declare image_eq_UN [simp] (*accelerates proofs involving nested images*)
(*A "possibility property": there are traces that reach the end*)
-lemma "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubK B) (Nonce NB)) \<in> set evs"
+lemma "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2] ns_public.Nil [THEN ns_public.NS1, THEN ns_public.NS2,
THEN ns_public.NS3])
@@ -62,12 +62,12 @@
sends messages containing X! **)
(*Spy never sees another agent's private key! (unless it's bad at start)*)
-lemma Spy_see_priK [simp]:
- "evs \<in> ns_public \<Longrightarrow> (Key (priK A) \<in> parts (spies evs)) = (A \<in> bad)"
+lemma Spy_see_priEK [simp]:
+ "evs \<in> ns_public \<Longrightarrow> (Key (priEK A) \<in> parts (spies evs)) = (A \<in> bad)"
by (erule ns_public.induct, auto)
-lemma Spy_analz_priK [simp]:
- "evs \<in> ns_public \<Longrightarrow> (Key (priK A) \<in> analz (spies evs)) = (A \<in> bad)"
+lemma Spy_analz_priEK [simp]:
+ "evs \<in> ns_public \<Longrightarrow> (Key (priEK A) \<in> analz (spies evs)) = (A \<in> bad)"
by auto
@@ -77,8 +77,8 @@
is secret. (Honest users generate fresh nonces.)*)
lemma no_nonce_NS1_NS2 [rule_format]:
"evs \<in> ns_public
- \<Longrightarrow> Crypt (pubK C) \<lbrace>NA', Nonce NA\<rbrace> \<in> parts (spies evs) \<longrightarrow>
- Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>
+ \<Longrightarrow> Crypt (pubEK C) \<lbrace>NA', Nonce NA\<rbrace> \<in> parts (spies evs) \<longrightarrow>
+ Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>
Nonce NA \<in> analz (spies evs)"
apply (erule ns_public.induct, simp_all)
apply (blast intro: analz_insertI)+
@@ -87,8 +87,8 @@
(*Unicity for NS1: nonce NA identifies agents A and B*)
lemma unique_NA:
- "\<lbrakk>Crypt(pubK B) \<lbrace>Nonce NA, Agent A \<rbrace> \<in> parts(spies evs);
- Crypt(pubK B') \<lbrace>Nonce NA, Agent A'\<rbrace> \<in> parts(spies evs);
+ "\<lbrakk>Crypt(pubEK B) \<lbrace>Nonce NA, Agent A \<rbrace> \<in> parts(spies evs);
+ Crypt(pubEK B') \<lbrace>Nonce NA, Agent A'\<rbrace> \<in> parts(spies evs);
Nonce NA \<notin> analz (spies evs); evs \<in> ns_public\<rbrakk>
\<Longrightarrow> A=A' \<and> B=B'"
apply (erule rev_mp, erule rev_mp, erule rev_mp)
@@ -102,7 +102,7 @@
The major premise "Says A B ..." makes it a dest-rule, so we use
(erule rev_mp) rather than rule_format. *)
theorem Spy_not_see_NA:
- "\<lbrakk>Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs;
+ "\<lbrakk>Says A B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
\<Longrightarrow> Nonce NA \<notin> analz (spies evs)"
apply (erule rev_mp)
@@ -115,27 +115,27 @@
to start a run, then B has sent message 2.*)
lemma A_trusts_NS2_lemma [rule_format]:
"\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
- \<Longrightarrow> Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow>
- Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs \<longrightarrow>
- Says B A (Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs"
+ \<Longrightarrow> Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow>
+ Says A B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs \<longrightarrow>
+ Says B A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs"
apply (erule ns_public.induct)
apply (auto dest: Spy_not_see_NA unique_NA)
done
theorem A_trusts_NS2:
- "\<lbrakk>Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs;
- Says B' A (Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs;
+ "\<lbrakk>Says A B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs;
+ Says B' A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
- \<Longrightarrow> Says B A (Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs"
+ \<Longrightarrow> Says B A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs"
by (blast intro: A_trusts_NS2_lemma)
(*If the encrypted message appears then it originated with Alice in NS1*)
lemma B_trusts_NS1 [rule_format]:
"evs \<in> ns_public
- \<Longrightarrow> Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>
+ \<Longrightarrow> Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>
Nonce NA \<notin> analz (spies evs) \<longrightarrow>
- Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs"
+ Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs"
apply (erule ns_public.induct, simp_all)
(*Fake*)
apply (blast intro!: analz_insertI)
@@ -148,8 +148,8 @@
(*Unicity for NS2: nonce NB identifies nonce NA and agent A
[proof closely follows that for unique_NA] *)
lemma unique_NB [dest]:
- "\<lbrakk>Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace> \<in> parts(spies evs);
- Crypt(pubK A') \<lbrace>Nonce NA', Nonce NB\<rbrace> \<in> parts(spies evs);
+ "\<lbrakk>Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace> \<in> parts(spies evs);
+ Crypt(pubEK A') \<lbrace>Nonce NA', Nonce NB\<rbrace> \<in> parts(spies evs);
Nonce NB \<notin> analz (spies evs); evs \<in> ns_public\<rbrakk>
\<Longrightarrow> A=A' \<and> NA=NA'"
apply (erule rev_mp, erule rev_mp, erule rev_mp)
@@ -161,8 +161,8 @@
(*NB remains secret PROVIDED Alice never responds with round 3*)
theorem Spy_not_see_NB [dest]:
- "\<lbrakk>Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs;
- \<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs;
+ "\<lbrakk>Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs;
+ \<forall>C. Says A C (Crypt (pubEK C) (Nonce NB)) \<notin> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
\<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
apply (erule rev_mp, erule rev_mp)
@@ -177,23 +177,23 @@
lemma B_trusts_NS3_lemma [rule_format]:
"\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
- \<Longrightarrow> Crypt (pubK B) (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
- Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs \<longrightarrow>
- (\<exists>C. Says A C (Crypt (pubK C) (Nonce NB)) \<in> set evs)"
+ \<Longrightarrow> Crypt (pubEK B) (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
+ Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs \<longrightarrow>
+ (\<exists>C. Says A C (Crypt (pubEK C) (Nonce NB)) \<in> set evs)"
apply (erule ns_public.induct, auto)
by (blast intro: no_nonce_NS1_NS2)+
theorem B_trusts_NS3:
- "\<lbrakk>Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs;
- Says A' B (Crypt (pubK B) (Nonce NB)) \<in> set evs;
+ "\<lbrakk>Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs;
+ Says A' B (Crypt (pubEK B) (Nonce NB)) \<in> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
- \<Longrightarrow> \<exists>C. Says A C (Crypt (pubK C) (Nonce NB)) \<in> set evs"
+ \<Longrightarrow> \<exists>C. Says A C (Crypt (pubEK C) (Nonce NB)) \<in> set evs"
by (blast intro: B_trusts_NS3_lemma)
(*Can we strengthen the secrecy theorem Spy_not_see_NB? NO*)
lemma "\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
- \<Longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs
+ \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs
\<longrightarrow> Nonce NB \<notin> analz (spies evs)"
apply (erule ns_public.induct, simp_all, spy_analz)
(*NS1: by freshness*)
@@ -211,14 +211,14 @@
THIS IS THE ATTACK!
Level 8
!!evs. \<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
- \<Longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs \<longrightarrow>
+ \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs \<longrightarrow>
Nonce NB \<notin> analz (spies evs)
1. !!C B' evs3.
\<lbrakk>A \<notin> bad; B \<notin> bad; evs3 \<in> ns_public
- Says A C (Crypt (pubK C) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
- Says B' A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3;
+ Says A C (Crypt (pubEK C) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
+ Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3;
C \<in> bad;
- Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3;
+ Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3;
Nonce NB \<notin> analz (spies evs3)\<rbrakk>
\<Longrightarrow> False
*)
--- a/src/HOL/Auth/Public.thy Wed Apr 23 18:09:48 2003 +0200
+++ b/src/HOL/Auth/Public.thy Fri Apr 25 11:18:14 2003 +0200
@@ -8,39 +8,408 @@
Private and public keys; initial states of agents
*)
-theory Public = Event
-files ("Public_lemmas.ML"):
+theory Public = Event:
+
+subsection{*Asymmetric Keys*}
consts
- pubK :: "agent => key"
+ (*the bool is TRUE if a signing key*)
+ publicKey :: "[bool,agent] => key"
syntax
- priK :: "agent => key"
+ pubEK :: "agent => key"
+ pubSK :: "agent => key"
+
+ privateKey :: "[bool,agent] => key"
+ priEK :: "agent => key"
+ priSK :: "agent => key"
+
+translations
+ "pubEK" == "publicKey False"
+ "pubSK" == "publicKey True"
+
+ (*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*)
+ "privateKey b A" == "invKey (publicKey b A)"
+ "priEK A" == "privateKey False A"
+ "priSK A" == "privateKey True A"
+
+
+text{*These translations give backward compatibility. They represent the
+simple situation where the signature and encryption keys are the same.*}
+syntax
+ pubK :: "agent => key"
+ priK :: "agent => key"
+
+translations
+ "pubK A" == "pubEK A"
+ "priK A" == "invKey (pubEK A)"
+
+
+axioms
+ (*By freeness of agents, no two agents have the same key. Since true\<noteq>false,
+ no agent has identical signing and encryption keys*)
+ injective_publicKey:
+ "publicKey b A = publicKey c A' ==> b=c & A=A'"
+
+ (*No private key equals any public key (essential to ensure that private
+ keys are private!) *)
+ privateKey_neq_publicKey [iff]: "privateKey b A \<noteq> publicKey c A'"
+
+
+
+
+(*** Basic properties of pubK & priK ***)
+
+lemma [iff]: "(publicKey b A = publicKey c A') = (b=c & A=A')"
+by (blast dest!: injective_publicKey)
+
+lemma [iff]:
+ "(privateKey b A = privateKey c A') = (b=c & A=A')"
+apply (rule iffI)
+apply (drule_tac f = "invKey" in arg_cong)
+apply (auto );
+done
+
+declare privateKey_neq_publicKey [THEN not_sym, iff]
+
+lemma not_symKeys_pubK [iff]: "publicKey b A \<notin> symKeys"
+apply (simp add: symKeys_def)
+done
+
+lemma not_symKeys_priK [iff]: "privateKey b A \<notin> symKeys"
+apply (simp add: symKeys_def)
+done
+
+lemma symKey_neq_priEK: "K \<in> symKeys ==> K \<noteq> priEK A"
+by auto
+
+lemma symKeys_neq_imp_neq: "(K \<in> symKeys) \<noteq> (K' \<in> symKeys) ==> K \<noteq> K'"
+apply blast
+done
+
+lemma symKeys_invKey_iff [iff]: "(invKey K \<in> symKeys) = (K \<in> symKeys)"
+apply (unfold symKeys_def)
+apply auto
+done
-translations (*BEWARE! expressions like (inj priK) will NOT work!*)
- "priK x" == "invKey(pubK x)"
+lemma analz_symKeys_Decrypt:
+ "[| Crypt K X \<in> analz H; K \<in> symKeys; Key K \<in> analz H |]
+ ==> X \<in> analz H"
+by (auto simp add: symKeys_def)
+
+
+
+subsection{*"Image" equations that hold for injective functions*}
+
+lemma invKey_image_eq [simp]: "(invKey x \<in> invKey`A) = (x \<in> A)"
+apply auto
+done
+
+(*holds because invKey is injective*)
+lemma publicKey_image_eq [simp]:
+ "(publicKey b x \<in> publicKey c ` AA) = (b=c & x \<in> AA)"
+by auto
+
+lemma privateKey_notin_image_publicKey [simp]: "privateKey b x \<notin> publicKey c ` AA"
+apply auto
+done
+
+lemma privateKey_image_eq [simp]:
+ "(privateKey b A \<in> invKey ` publicKey c ` AS) = (b=c & A\<in>AS)"
+by auto
+
+lemma publicKey_notin_image_privateKey [simp]: "publicKey b A \<notin> invKey ` publicKey c ` AS"
+apply auto
+done
+
+
+subsection{*Symmetric Keys*}
+
+text{*For some protocols, it is convenient to equip agents with symmetric as
+well as asymmetric keys. The theory @{text Shared} assumes that all keys
+are symmetric.*}
+
+consts
+ shrK :: "agent => key" --{*long-term shared keys*}
+
+axioms
+ inj_shrK: "inj shrK" --{*No two agents have the same key*}
+ sym_shrK [iff]: "shrK X \<in> symKeys" --{*All shared keys are symmetric*}
+
+(*Injectiveness: Agents' long-term keys are distinct.*)
+declare inj_shrK [THEN inj_eq, iff]
+
+lemma priK_neq_shrK [iff]: "shrK A \<noteq> privateKey b C"
+apply (simp add: symKeys_neq_imp_neq)
+done
+
+declare priK_neq_shrK [THEN not_sym, simp]
+
+lemma pubK_neq_shrK [iff]: "shrK A \<noteq> publicKey b C"
+apply (simp add: symKeys_neq_imp_neq)
+done
+
+declare pubK_neq_shrK [THEN not_sym, simp]
+
+lemma priEK_noteq_shrK [simp]: "priEK A \<noteq> shrK B"
+by auto
+
+lemma publicKey_notin_image_shrK [simp]: "publicKey b x \<notin> shrK ` AA"
+by auto
+
+lemma privateKey_notin_image_shrK [simp]: "privateKey b x \<notin> shrK ` AA"
+by auto
+
+lemma shrK_notin_image_publicKey [simp]: "shrK x \<notin> publicKey b ` AA"
+by auto
+
+lemma shrK_notin_image_privateKey [simp]: "shrK x \<notin> invKey ` publicKey b ` AA"
+by auto
+
+lemma shrK_image_eq [simp]: "(shrK x \<in> shrK ` AA) = (x \<in> AA)"
+by auto
+
+
+subsection{*Initial States of Agents*}
+
+text{*Note: for all practical purposes, all that matters is the initial
+knowledge of the Spy. All other agents are automata, merely following the
+protocol.*}
primrec
(*Agents know their private key and all public keys*)
- initState_Server: "initState Server =
- insert (Key (priK Server)) (Key ` range pubK)"
- initState_Friend: "initState (Friend i) =
- insert (Key (priK (Friend i))) (Key ` range pubK)"
- initState_Spy: "initState Spy =
- (Key`invKey`pubK`bad) Un (Key ` range pubK)"
+ initState_Server:
+ "initState Server =
+ {Key (priEK Server), Key (priSK Server)} \<union>
+ (Key ` range pubEK) \<union> (Key ` range pubSK) \<union> (Key ` range shrK)"
+
+ initState_Friend:
+ "initState (Friend i) =
+ {Key (priEK(Friend i)), Key (priSK(Friend i)), Key (shrK(Friend i))} \<union>
+ (Key ` range pubEK) \<union> (Key ` range pubSK)"
+
+ initState_Spy:
+ "initState Spy =
+ (Key ` invKey ` pubEK ` bad) \<union> (Key ` invKey ` pubSK ` bad) \<union>
+ (Key ` shrK ` bad) \<union>
+ (Key ` range pubEK) \<union> (Key ` range pubSK)"
+
+
+
+text{*These lemmas allow reasoning about @{term "used evs"} rather than
+ @{term "knows Spy evs"}, which is useful when there are private Notes. *}
+
+lemma used_parts_subset_parts [rule_format]:
+ "\<forall>X \<in> used evs. parts {X} \<subseteq> used evs"
+apply (induct evs)
+ prefer 2
+ apply (simp add: used_Cons)
+ apply (rule ballI)
+ apply (case_tac a, auto)
+ apply (drule parts_cut, assumption, simp)
+ apply (drule parts_cut, assumption, simp)
+txt{*Base case*}
+apply (simp add: used_Nil, clarify)
+apply (rename_tac B)
+apply (rule_tac x=B in exI)
+apply (case_tac B, auto)
+done
+
+lemma MPair_used_D: "{|X,Y|} \<in> used H ==> X \<in> used H & Y \<in> used H"
+by (drule used_parts_subset_parts, simp, blast)
+
+lemma MPair_used [elim!]:
+ "[| {|X,Y|} \<in> used H;
+ [| X \<in> used H; Y \<in> used H |] ==> P |]
+ ==> P"
+by (blast dest: MPair_used_D)
+
+
+text{*Rewrites should not refer to @{term "initState(Friend i)"} because
+ that expression is not in normal form.*}
+
+lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}"
+apply (unfold keysFor_def)
+apply (induct_tac "C")
+apply (auto intro: range_eqI)
+done
+
+lemma Crypt_notin_initState: "Crypt K X \<notin> parts (initState B)"
+by (induct B, auto)
+
+
+(*** Basic properties of shrK ***)
+
+(*Agents see their own shared keys!*)
+lemma shrK_in_initState [iff]: "Key (shrK A) \<in> initState A"
+apply (induct_tac "A")
+apply auto
+done
+
+lemma shrK_in_knows [iff]: "Key (shrK A) \<in> knows A evs"
+by (simp add: initState_subset_knows [THEN subsetD])
+
+lemma shrK_in_used [iff]: "Key (shrK A) \<in> used evs"
+apply (rule initState_into_used)
+apply blast
+done
+
+(** Fresh keys never clash with long-term shared keys **)
+
+(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
+ from long-term shared keys*)
+lemma Key_not_used: "Key K \<notin> used evs ==> K \<notin> range shrK"
+apply blast
+done
+
+lemma shrK_neq: "Key K \<notin> used evs ==> shrK B \<noteq> K"
+apply blast
+done
+
-axioms
- (*Public keys are disjoint, and never clash with private keys*)
- inj_pubK: "inj pubK"
- priK_neq_pubK: "priK A ~= pubK B"
+subsection{*Function @{term spies} *}
+
+text{*Agents see their own private keys!*}
+lemma priK_in_initState [iff]: "Key (privateKey b A) \<in> initState A"
+apply (induct_tac "A")
+apply auto
+done
+
+text{*Agents see all public keys!*}
+lemma publicKey_in_initState [iff]: "Key (publicKey b A) \<in> initState B"
+apply (case_tac "B")
+apply auto
+done
+
+text{*All public keys are visible*}
+lemma spies_pubK [iff]: "Key (publicKey b A) \<in> spies evs"
+apply (induct_tac "evs")
+apply (simp_all add: imageI knows_Cons split add: event.split)
+done
+
+declare spies_pubK [THEN analz.Inj, iff]
+
+text{*Spy sees private keys of bad agents!*}
+lemma Spy_spies_bad_privateKey [intro!]:
+ "A \<in> bad ==> Key (privateKey b A) \<in> spies evs"
+apply (induct_tac "evs")
+apply (simp_all add: imageI knows_Cons split add: event.split)
+done
+
+text{*Spy sees long-term shared keys of bad agents!*}
+lemma Spy_spies_bad_shrK [intro!]:
+ "A \<in> bad ==> Key (shrK A) \<in> spies evs"
+apply (induct_tac "evs")
+apply (simp_all add: imageI knows_Cons split add: event.split)
+done
+
+lemma publicKey_into_used [iff] :"Key (publicKey b A) \<in> used evs"
+apply (rule initState_into_used)
+apply (rule publicKey_in_initState [THEN parts.Inj])
+done
+
+lemma privateKey_into_used [iff]: "Key (privateKey b A) \<in> used evs"
+apply(rule initState_into_used)
+apply(rule priK_in_initState [THEN parts.Inj])
+done
+
+
+subsection{*Fresh Nonces*}
+
+lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState B)"
+apply (induct_tac "B")
+apply auto
+done
+
+lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []"
+apply (simp add: used_Nil)
+done
+
-use "Public_lemmas.ML"
+subsection{*Supply fresh nonces for possibility theorems*}
+
+text{*In any trace, there is an upper bound N on the greatest nonce in use*}
+lemma Nonce_supply_lemma: "EX N. ALL n. N<=n --> Nonce n \<notin> used evs"
+apply (induct_tac "evs")
+apply (rule_tac x = "0" in exI)
+apply (simp_all (no_asm_simp) add: used_Cons split add: event.split)
+apply safe
+apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
+done
+
+lemma Nonce_supply1: "EX N. Nonce N \<notin> used evs"
+apply (rule Nonce_supply_lemma [THEN exE])
+apply blast
+done
+
+lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs"
+apply (rule Nonce_supply_lemma [THEN exE])
+apply (rule someI)
+apply fast
+done
+
+subsection{*Specialized rewriting for the analz_image_... theorems*}
+
+lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} Un H"
+apply blast
+done
-lemma [simp]: "K \\<in> symKeys ==> invKey K = K"
+lemma insert_Key_image: "insert (Key K) (Key`KK \<union> C) = Key ` (insert K KK) \<union> C"
+apply blast
+done
+
+ML
+{*
+val Key_not_used = thm "Key_not_used";
+val insert_Key_singleton = thm "insert_Key_singleton";
+val insert_Key_image = thm "insert_Key_image";
+*}
+
+(*
+val not_symKeys_pubK = thm "not_symKeys_pubK";
+val not_symKeys_priK = thm "not_symKeys_priK";
+val symKeys_neq_imp_neq = thm "symKeys_neq_imp_neq";
+val analz_symKeys_Decrypt = thm "analz_symKeys_Decrypt";
+val invKey_image_eq = thm "invKey_image_eq";
+val pubK_image_eq = thm "pubK_image_eq";
+val priK_pubK_image_eq = thm "priK_pubK_image_eq";
+val keysFor_parts_initState = thm "keysFor_parts_initState";
+val priK_in_initState = thm "priK_in_initState";
+val spies_pubK = thm "spies_pubK";
+val Spy_spies_bad = thm "Spy_spies_bad";
+val Nonce_notin_initState = thm "Nonce_notin_initState";
+val Nonce_notin_used_empty = thm "Nonce_notin_used_empty";
+
+*)
+
+
+lemma invKey_K [simp]: "K \<in> symKeys ==> invKey K = K"
by (simp add: symKeys_def)
-(*Specialized methods*)
+lemma Crypt_imp_keysFor :"[|K \<in> symKeys; Crypt K X \<in> H|] ==> K \<in> keysFor H"
+apply (drule Crypt_imp_invKey_keysFor, simp)
+done
+
+
+subsection{*Specialized Methods for Possibility Theorems*}
+
+ML
+{*
+val Nonce_supply1 = thm "Nonce_supply1";
+val Nonce_supply = thm "Nonce_supply";
+
+(*Tactic for possibility theorems (Isar interface)*)
+fun gen_possibility_tac ss state = state |>
+ REPEAT (*omit used_Says so that Nonces start from different traces!*)
+ (ALLGOALS (simp_tac (ss delsimps [used_Says]))
+ THEN
+ REPEAT_FIRST (eq_assume_tac ORELSE'
+ resolve_tac [refl, conjI, Nonce_supply]))
+
+(*Tactic for possibility theorems (ML script version)*)
+fun possibility_tac state = gen_possibility_tac (simpset()) state
+*}
method_setup possibility = {*
Method.ctxt_args (fn ctxt =>
@@ -48,4 +417,22 @@
gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *}
"for proving possibility theorems"
+
+
+ML
+{*
+bind_thms ("analz_image_freshK_simps",
+ simp_thms @ mem_simps @ (*these two allow its use with only:*)
+ disj_comms @
+ [image_insert RS sym, image_Un RS sym, empty_subsetI, insert_subset,
+ analz_insert_eq, impOfSubs (Un_upper2 RS analz_mono),
+ insert_Key_singleton,
+ Key_not_used, insert_Key_image, Un_assoc RS sym]);
+
+val analz_image_freshK_ss =
+ simpset() delsimps [image_insert, image_Un]
+ delsimps [imp_disjL] (*reduces blow-up*)
+ addsimps analz_image_freshK_simps;
+*}
+
end
--- a/src/HOL/Auth/Public_lemmas.ML Wed Apr 23 18:09:48 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,172 +0,0 @@
-(* Title: HOL/Auth/Public_lemmas
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-
-Theory of Public Keys (common to all symmetric-key protocols)
-
-Server keys; initial states of agents; new nonces and keys; function "sees"
-*)
-
-val inj_pubK = thm "inj_pubK";
-val priK_neq_pubK = thm "priK_neq_pubK";
-
-(*** Basic properties of pubK & priK ***)
-
-AddIffs [inj_pubK RS inj_eq];
-
-Goal "(priK A = priK B) = (A=B)";
-by Safe_tac;
-by (dres_inst_tac [("f","invKey")] arg_cong 1);
-by (Full_simp_tac 1);
-qed "priK_inj_eq";
-
-AddIffs [priK_inj_eq];
-AddIffs [priK_neq_pubK, priK_neq_pubK RS not_sym];
-
-Goalw [symKeys_def] "pubK A \\<notin> symKeys";
-by (Simp_tac 1);
-qed "not_symKeys_pubK";
-
-Goalw [symKeys_def] "priK A \\<notin> symKeys";
-by (Simp_tac 1);
-qed "not_symKeys_priK";
-
-AddIffs [not_symKeys_pubK, not_symKeys_priK];
-
-Goal "(K \\<in> symKeys) \\<noteq> (K' \\<in> symKeys) ==> K \\<noteq> K'";
-by (Blast_tac 1);
-qed "symKeys_neq_imp_neq";
-
-Goal "[| Crypt K X \\<in> analz H; K \\<in> symKeys; Key K \\<in> analz H |] \
-\ ==> X \\<in> analz H";
-by (auto_tac(claset(), simpset() addsimps [symKeys_def]));
-qed "analz_symKeys_Decrypt";
-
-
-(** "Image" equations that hold for injective functions **)
-
-Goal "(invKey x : invKey`A) = (x:A)";
-by Auto_tac;
-qed "invKey_image_eq";
-
-(*holds because invKey is injective*)
-Goal "(pubK x : pubK`A) = (x:A)";
-by Auto_tac;
-qed "pubK_image_eq";
-
-Goal "(priK x ~: pubK`A)";
-by Auto_tac;
-qed "priK_pubK_image_eq";
-Addsimps [invKey_image_eq, pubK_image_eq, priK_pubK_image_eq];
-
-
-(** Rewrites should not refer to initState(Friend i)
- -- not in normal form! **)
-
-Goalw [keysFor_def] "keysFor (parts (initState C)) = {}";
-by (induct_tac "C" 1);
-by (auto_tac (claset() addIs [range_eqI], simpset()));
-qed "keysFor_parts_initState";
-Addsimps [keysFor_parts_initState];
-
-
-(*** Function "spies" ***)
-
-(*Agents see their own private keys!*)
-Goal "Key (priK A) : initState A";
-by (induct_tac "A" 1);
-by Auto_tac;
-qed "priK_in_initState";
-AddIffs [priK_in_initState];
-
-(*All public keys are visible*)
-Goal "Key (pubK A) : spies evs";
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac
- (simpset() addsimps [imageI, knows_Cons]
- addsplits [expand_event_case])));
-qed_spec_mp "spies_pubK";
-
-(*Spy sees private keys of bad agents!*)
-Goal "A: bad ==> Key (priK A) : spies evs";
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac
- (simpset() addsimps [imageI, knows_Cons]
- addsplits [expand_event_case])));
-qed "Spy_spies_bad";
-
-AddIffs [spies_pubK, spies_pubK RS analz.Inj];
-AddSIs [Spy_spies_bad];
-
-
-(*** Fresh nonces ***)
-
-Goal "Nonce N ~: parts (initState B)";
-by (induct_tac "B" 1);
-by Auto_tac;
-qed "Nonce_notin_initState";
-AddIffs [Nonce_notin_initState];
-
-Goal "Nonce N ~: used []";
-by (simp_tac (simpset() addsimps [used_Nil]) 1);
-qed "Nonce_notin_used_empty";
-Addsimps [Nonce_notin_used_empty];
-
-
-(*** Supply fresh nonces for possibility theorems. ***)
-
-(*In any trace, there is an upper bound N on the greatest nonce in use.*)
-Goal "EX N. ALL n. N<=n --> Nonce n ~: used evs";
-by (induct_tac "evs" 1);
-by (res_inst_tac [("x","0")] exI 1);
-by (ALLGOALS (asm_simp_tac
- (simpset() addsimps [used_Cons]
- addsplits [expand_event_case])));
-by Safe_tac;
-by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
-by (ALLGOALS (blast_tac (claset() addSEs [add_leE])));
-val lemma = result();
-
-Goal "EX N. Nonce N ~: used evs";
-by (rtac (lemma RS exE) 1);
-by (Blast_tac 1);
-qed "Nonce_supply1";
-
-Goal "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
-by (rtac (lemma RS exE) 1);
-by (rtac someI 1);
-by (Fast_tac 1);
-qed "Nonce_supply";
-
-(*Tactic for possibility theorems (Isar interface)*)
-fun gen_possibility_tac ss state = state |>
- REPEAT (*omit used_Says so that Nonces start from different traces!*)
- (ALLGOALS (simp_tac (ss delsimps [used_Says]))
- THEN
- REPEAT_FIRST (eq_assume_tac ORELSE'
- resolve_tac [refl, conjI, Nonce_supply]));
-
-(*Tactic for possibility theorems (ML script version)*)
-fun possibility_tac state = gen_possibility_tac (simpset()) state;
-
-(*** Specialized rewriting for the analz_image_... theorems ***)
-
-Goal "insert (Key K) H = Key ` {K} Un H";
-by (Blast_tac 1);
-qed "insert_Key_singleton";
-
-Goal "insert (Key K) (Key`KK Un C) = Key ` (insert K KK) Un C";
-by (Blast_tac 1);
-qed "insert_Key_image";
-
-(*Reverse the normal simplification of "image" to build up (not break down)
- the set of keys. Based on analz_image_freshK_ss, but simpler.*)
-val analz_image_keys_ss =
- simpset() delsimps [image_insert, image_Un]
- delsimps [imp_disjL] (*reduces blow-up*)
- addsimps [image_insert RS sym, image_Un RS sym,
- rangeI,
- insert_Key_singleton,
- insert_Key_image, Un_assoc RS sym];
-
--- a/src/HOL/Auth/ROOT.ML Wed Apr 23 18:09:48 2003 +0200
+++ b/src/HOL/Auth/ROOT.ML Fri Apr 25 11:18:14 2003 +0200
@@ -26,6 +26,7 @@
time_use_thy "NS_Public_Bad";
time_use_thy "NS_Public";
time_use_thy "TLS";
+time_use_thy "CertifiedEmail";
(*Blanqui's "guard" concept: protocol-independent secrecy*)
time_use_thy "Guard/P1";
--- a/src/HOL/Auth/Recur.thy Wed Apr 23 18:09:48 2003 +0200
+++ b/src/HOL/Auth/Recur.thy Fri Apr 25 11:18:14 2003 +0200
@@ -8,7 +8,7 @@
theory Recur = Shared:
-(*End marker for message bundles*)
+text{*End marker for message bundles*}
syntax END :: "msg"
translations "END" == "Number 0"
@@ -116,17 +116,17 @@
**)
-(*Simplest case: Alice goes directly to the server*)
+text{*Simplest case: Alice goes directly to the server*}
lemma "\<exists>K NA. \<exists>evs \<in> recur.
Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|},
END|} \<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2] recur.Nil [THEN recur.RA1,
- THEN recur.RA3 [OF _ _ respond.One]], possibility)
+ THEN recur.RA3 [OF _ _ respond.One]], possibility)
done
-(*Case two: Alice, Bob and the server*)
+text{*Case two: Alice, Bob and the server*}
lemma "\<exists>K. \<exists>NA. \<exists>evs \<in> recur.
Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
END|} \<in> set evs"
@@ -174,7 +174,7 @@
apply (auto dest: Key_not_used respond_imp_not_used)
done
-(*Simple inductive reasoning about responses*)
+text{*Simple inductive reasoning about responses*}
lemma respond_imp_responses:
"(PA,RB,KAB) \<in> respond evs ==> RB \<in> responses evs"
apply (erule respond.induct)
@@ -208,7 +208,7 @@
lemma Spy_see_shrK [simp]:
"evs \<in> recur ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
apply (erule recur.induct, auto)
-(*RA3. It's ugly to call auto twice, but it seems necessary.*)
+txt{*RA3. It's ugly to call auto twice, but it seems necessary.*}
apply (auto dest: Key_in_parts_respond simp add: parts_insert_spies)
done
@@ -241,7 +241,7 @@
add: analz_image_freshK_simps)
-(*Version for the protocol. Proof is almost trivial, thanks to the lemma.*)
+text{*Version for the protocol. Proof is almost trivial, thanks to the lemma.*}
lemma raw_analz_image_freshK:
"evs \<in> recur ==>
\<forall>K KK. KK \<subseteq> - (range shrK) -->
@@ -251,7 +251,7 @@
apply (drule_tac [4] RA2_analz_spies,
drule_tac [5] respond_imp_responses,
drule_tac [6] RA4_analz_spies, analz_freshK, spy_analz)
-(*RA3*)
+txt{*RA3*}
apply (simp_all add: resp_analz_image_freshK_lemma)
done
@@ -273,7 +273,7 @@
add: analz_image_freshK_simps raw_analz_image_freshK)
-(*Everything that's hashed is already in past traffic. *)
+text{*Everything that's hashed is already in past traffic. *}
lemma Hash_imp_body:
"[| Hash {|Key(shrK A), X|} \<in> parts (spies evs);
evs \<in> recur; A \<notin> bad |] ==> X \<in> parts (spies evs)"
@@ -282,11 +282,9 @@
drule_tac [6] RA4_parts_spies,
drule_tac [5] respond_imp_responses,
drule_tac [4] RA2_parts_spies)
-(*RA3 requires a further induction*)
+txt{*RA3 requires a further induction*}
apply (erule_tac [5] responses.induct, simp_all)
-(*Nil*)
-apply force
-(*Fake*)
+txt{*Fake*}
apply (blast intro: parts_insertI)
done
@@ -306,10 +304,10 @@
apply (erule recur.induct,
drule_tac [5] respond_imp_responses)
apply (force, simp_all)
-(*Fake*)
+txt{*Fake*}
apply blast
apply (erule_tac [3] responses.induct)
-(*RA1,2: creation of new Nonce*)
+txt{*RA1,2: creation of new Nonce*}
apply simp_all
apply (blast dest!: Hash_imp_body)+
done
@@ -337,14 +335,14 @@
apply (erule rev_mp, erule responses.induct)
apply (simp_all del: image_insert
add: analz_image_freshK_simps resp_analz_image_freshK_lemma)
-(*Simplification using two distinct treatments of "image"*)
+txt{*Simplification using two distinct treatments of "image"*}
apply (simp add: parts_insert2, blast)
done
lemmas resp_analz_insert =
resp_analz_insert_lemma [OF _ raw_analz_image_freshK]
-(*The last key returned by respond indeed appears in a certificate*)
+text{*The last key returned by respond indeed appears in a certificate*}
lemma respond_certificate:
"(Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) \<in> respond evs
==> Crypt (shrK A) {|Key K, B, NA|} \<in> parts {RA}"
@@ -390,13 +388,11 @@
apply (simp_all del: image_insert
add: analz_image_freshK_simps split_ifs shrK_in_analz_respond
resp_analz_image_freshK parts_insert2)
-apply (simp_all add: ex_disj_distrib)
-(** LEVEL 5 **)
-(*Base case of respond*)
+txt{*Base case of respond*}
apply blast
-(*Inductive step of respond*)
+txt{*Inductive step of respond*}
apply (intro allI conjI impI, simp_all)
-(*by unicity, either B=Aa or B=A', a contradiction if B \<in> bad*)
+txt{*by unicity, either B=Aa or B=A', a contradiction if B \<in> bad*}
apply (blast dest: unique_session_keys [OF _ respond_certificate])
apply (blast dest!: respond_certificate)
apply (blast dest!: resp_analz_insert)
@@ -413,28 +409,26 @@
frule_tac [5] respond_imp_responses,
drule_tac [6] RA4_analz_spies,
simp_all add: split_ifs analz_insert_eq analz_insert_freshK)
-(*Base*)
-apply force
-(*Fake*)
+txt{*Fake*}
apply spy_analz
-(*RA2*)
+txt{*RA2*}
apply blast
-(*RA3 remains*)
+txt{*RA3 remains*}
apply (simp add: parts_insert_spies)
-(*Now we split into two cases. A single blast could do it, but it would take
- a CPU minute.*)
+txt{*Now we split into two cases. A single blast could do it, but it would take
+ a CPU minute.*}
apply (safe del: impCE)
-(*RA3, case 1: use lemma previously proved by induction*)
+txt{*RA3, case 1: use lemma previously proved by induction*}
apply (blast elim: rev_notE [OF _ respond_Spy_not_see_session_key])
-(*RA3, case 2: K is an old key*)
+txt{*RA3, case 2: K is an old key*}
apply (blast dest: resp_analz_insert dest: Key_in_parts_respond)
-(*RA4*)
+txt{*RA4*}
apply blast
done
(**** Authenticity properties for Agents ****)
-(*The response never contains Hashes*)
+text{*The response never contains Hashes*}
lemma Hash_in_parts_respond:
"[| Hash {|Key (shrK B), M|} \<in> parts (insert RB H);
(PB,RB,K) \<in> respond evs |]
@@ -443,10 +437,10 @@
apply (erule respond_imp_responses [THEN responses.induct], auto)
done
-(*Only RA1 or RA2 can have caused such a part of a message to appear.
+text{*Only RA1 or RA2 can have caused such a part of a message to appear.
This result is of no use to B, who cannot verify the Hash. Moreover,
it can say nothing about how recent A's message is. It might later be
- used to prove B's presence to A at the run's conclusion.*)
+ used to prove B's presence to A at the run's conclusion.*}
lemma Hash_auth_sender [rule_format]:
"[| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} \<in> parts(spies evs);
A \<notin> bad; evs \<in> recur |]
@@ -457,9 +451,9 @@
drule_tac [6] RA4_parts_spies,
drule_tac [4] RA2_parts_spies,
simp_all)
-(*Nil*)
+txt{*Nil*}
apply force
-(*Fake, RA3*)
+txt{*Fake, RA3*}
apply (blast dest: Hash_in_parts_respond)+
done
@@ -468,25 +462,23 @@
**)
-(*Certificates can only originate with the Server.*)
+text{*Certificates can only originate with the Server.*}
lemma Cert_imp_Server_msg:
"[| Crypt (shrK A) Y \<in> parts (spies evs);
A \<notin> bad; evs \<in> recur |]
==> \<exists>C RC. Says Server C RC \<in> set evs &
Crypt (shrK A) Y \<in> parts {RC}"
apply (erule rev_mp, erule recur.induct, simp_all)
-(*Nil*)
-apply force
-(*Fake*)
+txt{*Fake*}
apply blast
-(*RA1*)
+txt{*RA1*}
apply blast
-(*RA2: it cannot be a new Nonce, contradiction.*)
+txt{*RA2: it cannot be a new Nonce, contradiction.*}
apply blast
-(*RA3*) (*Pity that the proof is so brittle: this step requires the rewriting,
- which however would break all other steps.*)
+txt{*RA3. Pity that the proof is so brittle: this step requires the rewriting,
+ which however would break all other steps.*}
apply (simp add: parts_insert_spies, blast)
-(*RA4*)
+txt{*RA4*}
apply blast
done
--- a/src/HOL/Auth/TLS.thy Wed Apr 23 18:09:48 2003 +0200
+++ b/src/HOL/Auth/TLS.thy Fri Apr 25 11:18:14 2003 +0200
@@ -43,7 +43,11 @@
constdefs
certificate :: "[agent,key] => msg"
- "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"
+ "certificate A KA == Crypt (priSK Server) {|Agent A, Key KA|}"
+
+text{*TLS apparently does not require separate keypairs for encryption and
+signature. Therefore, we formalize signature as encryption using the
+private encryption key.*}
datatype role = ClientRole | ServerRole
@@ -66,67 +70,72 @@
"serverK X" == "sessionK(X, ServerRole)"
axioms
- (*the pseudo-random function is collision-free*)
+ --{*the pseudo-random function is collision-free*}
inj_PRF: "inj PRF"
- (*sessionK is collision-free; also, no clientK clashes with any serverK.*)
+ --{*sessionK is collision-free; also, no clientK clashes with any serverK.*}
inj_sessionK: "inj sessionK"
- (*sessionK makes symmetric keys*)
+ --{*sessionK makes symmetric keys*}
isSym_sessionK: "sessionK nonces \<in> symKeys"
+ --{*sessionK never clashes with a long-term symmetric key
+ (they don't exist in TLS anyway)*}
+ sessionK_neq_shrK [iff]: "sessionK nonces \<noteq> shrK A"
+
consts tls :: "event list set"
inductive tls
intros
- Nil: (*Initial trace is empty*)
+ Nil: --{*The initial, empty trace*}
"[] \<in> tls"
- Fake: (*The spy, an active attacker, MAY say anything he CAN say.*)
+ Fake: --{*The Spy may say anything he can say. The sender field is correct,
+ but agents don't use that information.*}
"[| evsf \<in> tls; X \<in> synth (analz (spies evsf)) |]
==> Says Spy B X # evsf \<in> tls"
- SpyKeys: (*The spy may apply PRF & sessionK to available nonces*)
+ SpyKeys: --{*The spy may apply PRF & sessionK to available nonces*}
"[| evsSK \<in> tls;
{Nonce NA, Nonce NB, Nonce M} <= analz (spies evsSK) |]
==> Notes Spy {| Nonce (PRF(M,NA,NB)),
Key (sessionK((NA,NB,M),role)) |} # evsSK \<in> tls"
ClientHello:
- (*(7.4.1.2)
+ --{*(7.4.1.2)
PA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
It is uninterpreted but will be confirmed in the FINISHED messages.
NA is CLIENT RANDOM, while SID is SESSION_ID.
UNIX TIME is omitted because the protocol doesn't use it.
May assume NA \<notin> range PRF because CLIENT RANDOM is 28 bytes
- while MASTER SECRET is 48 bytes*)
+ while MASTER SECRET is 48 bytes*}
"[| evsCH \<in> tls; Nonce NA \<notin> used evsCH; NA \<notin> range PRF |]
==> Says A B {|Agent A, Nonce NA, Number SID, Number PA|}
# evsCH \<in> tls"
ServerHello:
- (*7.4.1.3 of the TLS Internet-Draft
+ --{*7.4.1.3 of the TLS Internet-Draft
PB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
SERVER CERTIFICATE (7.4.2) is always present.
- CERTIFICATE_REQUEST (7.4.4) is implied.*)
+ CERTIFICATE_REQUEST (7.4.4) is implied.*}
"[| evsSH \<in> tls; Nonce NB \<notin> used evsSH; NB \<notin> range PRF;
Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
\<in> set evsSH |]
==> Says B A {|Nonce NB, Number SID, Number PB|} # evsSH \<in> tls"
Certificate:
- (*SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.*)
+ --{*SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.*}
"evsC \<in> tls ==> Says B A (certificate B (pubK B)) # evsC \<in> tls"
ClientKeyExch:
- (*CLIENT KEY EXCHANGE (7.4.7).
+ --{*CLIENT KEY EXCHANGE (7.4.7).
The client, A, chooses PMS, the PREMASTER SECRET.
She encrypts PMS using the supplied KB, which ought to be pubK B.
We assume PMS \<notin> range PRF because a clash betweem the PMS
and another MASTER SECRET is highly unlikely (even though
both items have the same length, 48 bytes).
The Note event records in the trace that she knows PMS
- (see REMARK at top). *)
+ (see REMARK at top). *}
"[| evsCX \<in> tls; Nonce PMS \<notin> used evsCX; PMS \<notin> range PRF;
Says B' A (certificate B KB) \<in> set evsCX |]
==> Says A B (Crypt KB (Nonce PMS))
@@ -134,28 +143,28 @@
# evsCX \<in> tls"
CertVerify:
- (*The optional Certificate Verify (7.4.8) message contains the
+ --{*The optional Certificate Verify (7.4.8) message contains the
specific components listed in the security analysis, F.1.1.2.
It adds the pre-master-secret, which is also essential!
Checking the signature, which is the only use of A's certificate,
- assures B of A's presence*)
+ assures B of A's presence*}
"[| evsCV \<in> tls;
Says B' A {|Nonce NB, Number SID, Number PB|} \<in> set evsCV;
Notes A {|Agent B, Nonce PMS|} \<in> set evsCV |]
==> Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}))
# evsCV \<in> tls"
- (*Finally come the FINISHED messages (7.4.8), confirming PA and PB
+ --{*Finally come the FINISHED messages (7.4.8), confirming PA and PB
among other things. The master-secret is PRF(PMS,NA,NB).
- Either party may send its message first.*)
+ Either party may send its message first.*}
ClientFinished:
- (*The occurrence of Notes A {|Agent B, Nonce PMS|} stops the
+ --{*The occurrence of Notes A {|Agent B, Nonce PMS|} stops the
rule's applying when the Spy has satisfied the "Says A B" by
repaying messages sent by the true client; in that case, the
Spy does not know PMS and could not send ClientFinished. One
could simply put A\<noteq>Spy into the rule, but one should not
- expect the spy to be well-behaved.*)
+ expect the spy to be well-behaved.*}
"[| evsCF \<in> tls;
Says A B {|Agent A, Nonce NA, Number SID, Number PA|}
\<in> set evsCF;
@@ -169,8 +178,8 @@
# evsCF \<in> tls"
ServerFinished:
- (*Keeping A' and A'' distinct means B cannot even check that the
- two messages originate from the same source. *)
+ --{*Keeping A' and A'' distinct means B cannot even check that the
+ two messages originate from the same source. *}
"[| evsSF \<in> tls;
Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
\<in> set evsSF;
@@ -184,10 +193,10 @@
# evsSF \<in> tls"
ClientAccepts:
- (*Having transmitted ClientFinished and received an identical
+ --{*Having transmitted ClientFinished and received an identical
message encrypted with serverK, the client stores the parameters
needed to resume this session. The "Notes A ..." premise is
- used to prove Notes_master_imp_Crypt_PMS.*)
+ used to prove Notes_master_imp_Crypt_PMS.*}
"[| evsCA \<in> tls;
Notes A {|Agent B, Nonce PMS|} \<in> set evsCA;
M = PRF(PMS,NA,NB);
@@ -200,10 +209,10 @@
Notes A {|Number SID, Agent A, Agent B, Nonce M|} # evsCA \<in> tls"
ServerAccepts:
- (*Having transmitted ServerFinished and received an identical
+ --{*Having transmitted ServerFinished and received an identical
message encrypted with clientK, the server stores the parameters
needed to resume this session. The "Says A'' B ..." premise is
- used to prove Notes_master_imp_Crypt_PMS.*)
+ used to prove Notes_master_imp_Crypt_PMS.*}
"[| evsSA \<in> tls;
A \<noteq> B;
Says A'' B (Crypt (pubK B) (Nonce PMS)) \<in> set evsSA;
@@ -217,8 +226,8 @@
Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA \<in> tls"
ClientResume:
- (*If A recalls the SESSION_ID, then she sends a FINISHED message
- using the new nonces and stored MASTER SECRET.*)
+ --{*If A recalls the SESSION_ID, then she sends a FINISHED message
+ using the new nonces and stored MASTER SECRET.*}
"[| evsCR \<in> tls;
Says A B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsCR;
Says B' A {|Nonce NB, Number SID, Number PB|} \<in> set evsCR;
@@ -230,8 +239,8 @@
# evsCR \<in> tls"
ServerResume:
- (*Resumption (7.3): If B finds the SESSION_ID then he can send
- a FINISHED message using the recovered MASTER SECRET*)
+ --{*Resumption (7.3): If B finds the SESSION_ID then he can send
+ a FINISHED message using the recovered MASTER SECRET*}
"[| evsSR \<in> tls;
Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsSR;
Says B A {|Nonce NB, Number SID, Number PB|} \<in> set evsSR;
@@ -243,10 +252,10 @@
\<in> tls"
Oops:
- (*The most plausible compromise is of an old session key. Losing
+ --{*The most plausible compromise is of an old session key. Losing
the MASTER SECRET or PREMASTER SECRET is more serious but
rather unlikely. The assumption A \<noteq> Spy is essential: otherwise
- the Spy could learn session keys merely by replaying messages!*)
+ the Spy could learn session keys merely by replaying messages!*}
"[| evso \<in> tls; A \<noteq> Spy;
Says A B (Crypt (sessionK((NA,NB,M),role)) X) \<in> set evso |]
==> Says A Spy (Key (sessionK((NA,NB,M),role))) # evso \<in> tls"
@@ -272,10 +281,10 @@
declare Fake_parts_insert_in_Un [dest]
-(*Automatically unfold the definition of "certificate"*)
+text{*Automatically unfold the definition of "certificate"*}
declare certificate_def [simp]
-(*Injectiveness of key-generating functions*)
+text{*Injectiveness of key-generating functions*}
declare inj_PRF [THEN inj_eq, iff]
declare inj_sessionK [THEN inj_eq, iff]
declare isSym_sessionK [simp]
@@ -283,12 +292,12 @@
(*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***)
-lemma pubK_neq_sessionK [iff]: "pubK A \<noteq> sessionK arg"
+lemma pubK_neq_sessionK [iff]: "publicKey b A \<noteq> sessionK arg"
by (simp add: symKeys_neq_imp_neq)
declare pubK_neq_sessionK [THEN not_sym, iff]
-lemma priK_neq_sessionK [iff]: "priK A \<noteq> sessionK arg"
+lemma priK_neq_sessionK [iff]: "invKey (publicKey b A) \<noteq> sessionK arg"
by (simp add: symKeys_neq_imp_neq)
declare priK_neq_sessionK [THEN not_sym, iff]
@@ -296,10 +305,10 @@
lemmas keys_distinct = pubK_neq_sessionK priK_neq_sessionK
-(**** Protocol Proofs ****)
+subsection{*Protocol Proofs*}
-(*Possibility properties state that some traces run the protocol to the end.
- Four paths and 12 rules are considered.*)
+text{*Possibility properties state that some traces run the protocol to the
+end. Four paths and 12 rules are considered.*}
(** These proofs assume that the Nonce_supply nonces
@@ -309,7 +318,7 @@
**)
-(*Possibility property ending with ClientAccepts.*)
+text{*Possibility property ending with ClientAccepts.*}
lemma "[| \<forall>evs. (@ N. Nonce N \<notin> used evs) \<notin> range PRF; A \<noteq> B |]
==> \<exists>SID M. \<exists>evs \<in> tls.
Notes A {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evs"
@@ -322,7 +331,7 @@
done
-(*And one for ServerAccepts. Either FINISHED message may come first.*)
+text{*And one for ServerAccepts. Either FINISHED message may come first.*}
lemma "[| \<forall>evs. (@ N. Nonce N \<notin> used evs) \<notin> range PRF; A \<noteq> B |]
==> \<exists>SID NA PA NB PB M. \<exists>evs \<in> tls.
Notes B {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evs"
@@ -335,7 +344,7 @@
done
-(*Another one, for CertVerify (which is optional)*)
+text{*Another one, for CertVerify (which is optional)*}
lemma "[| \<forall>evs. (@ N. Nonce N \<notin> used evs) \<notin> range PRF; A \<noteq> B |]
==> \<exists>NB PMS. \<exists>evs \<in> tls.
Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}))
@@ -348,8 +357,8 @@
done
-(*Another one, for session resumption (both ServerResume and ClientResume).
- NO tls.Nil here: we refer to a previous session, not the empty trace.*)
+text{*Another one, for session resumption (both ServerResume and ClientResume).
+ NO tls.Nil here: we refer to a previous session, not the empty trace.*}
lemma "[| evs0 \<in> tls;
Notes A {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evs0;
Notes B {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evs0;
@@ -368,41 +377,30 @@
done
-(**** Inductive proofs about tls ****)
-
+subsection{*Inductive proofs about tls*}
-(*Induction for regularity theorems. If induction formula has the form
- X \<notin> analz (spies evs) --> ... then it shortens the proof by discarding
- needless information about analz (insert X (spies evs))
-fun parts_induct_tac i =
- etac tls.induct i
- THEN REPEAT (FIRSTGOAL analz_mono_contra_tac)
- THEN Force_tac i THEN
- ALLGOALS Asm_simp_tac
-*)
(** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
sends messages containing X! **)
-(*Spy never sees a good agent's private key!*)
+text{*Spy never sees a good agent's private key!*}
lemma Spy_see_priK [simp]:
- "evs \<in> tls ==> (Key (priK A) \<in> parts (spies evs)) = (A \<in> bad)"
-apply (erule tls.induct, force, simp_all, blast)
-done
+ "evs \<in> tls ==> (Key (privateKey b A) \<in> parts (spies evs)) = (A \<in> bad)"
+by (erule tls.induct, force, simp_all, blast)
lemma Spy_analz_priK [simp]:
- "evs \<in> tls ==> (Key (priK A) \<in> analz (spies evs)) = (A \<in> bad)"
+ "evs \<in> tls ==> (Key (privateKey b A) \<in> analz (spies evs)) = (A \<in> bad)"
by auto
lemma Spy_see_priK_D [dest!]:
- "[|Key (priK A) \<in> parts (knows Spy evs); evs \<in> tls|] ==> A \<in> bad"
+ "[|Key (privateKey b A) \<in> parts (knows Spy evs); evs \<in> tls|] ==> A \<in> bad"
by (blast dest: Spy_see_priK)
-(*This lemma says that no false certificates exist. One might extend the
+text{*This lemma says that no false certificates exist. One might extend the
model to include bogus certificates for the agents, but there seems
little point in doing so: the loss of their private keys is a worse
- breach of security.*)
+ breach of security.*}
lemma certificate_valid:
"[| certificate B KB \<in> parts (spies evs); evs \<in> tls |] ==> KB = pubK B"
apply (erule rev_mp)
@@ -412,7 +410,7 @@
lemmas CX_KB_is_pubKB = Says_imp_spies [THEN parts.Inj, THEN certificate_valid]
-(*** Properties of items found in Notes ***)
+subsubsection{*Properties of items found in Notes*}
lemma Notes_Crypt_parts_spies:
"[| Notes A {|Agent B, X|} \<in> set evs; evs \<in> tls |]
@@ -423,34 +421,34 @@
apply (blast intro: parts_insertI)
done
-(*C may be either A or B*)
+text{*C may be either A or B*}
lemma Notes_master_imp_Crypt_PMS:
"[| Notes C {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} \<in> set evs;
evs \<in> tls |]
==> Crypt (pubK B) (Nonce PMS) \<in> parts (spies evs)"
apply (erule rev_mp)
apply (erule tls.induct, force, simp_all)
-(*Fake*)
+txt{*Fake*}
apply (blast intro: parts_insertI)
-(*Client, Server Accept*)
+txt{*Client, Server Accept*}
apply (blast dest!: Notes_Crypt_parts_spies)+
done
-(*Compared with the theorem above, both premise and conclusion are stronger*)
+text{*Compared with the theorem above, both premise and conclusion are stronger*}
lemma Notes_master_imp_Notes_PMS:
"[| Notes A {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} \<in> set evs;
evs \<in> tls |]
==> Notes A {|Agent B, Nonce PMS|} \<in> set evs"
apply (erule rev_mp)
apply (erule tls.induct, force, simp_all)
-(*ServerAccepts*)
+txt{*ServerAccepts*}
apply blast
done
-(*** Protocol goal: if B receives CertVerify, then A sent it ***)
+subsubsection{*Protocol goal: if B receives CertVerify, then A sent it*}
-(*B can check A's signature if he has received A's certificate.*)
+text{*B can check A's signature if he has received A's certificate.*}
lemma TrustCertVerify_lemma:
"[| X \<in> parts (spies evs);
X = Crypt (priK A) (Hash{|nb, Agent B, pms|});
@@ -460,7 +458,7 @@
apply (erule tls.induct, force, simp_all, blast)
done
-(*Final version: B checks X using the distributed KA instead of priK A*)
+text{*Final version: B checks X using the distributed KA instead of priK A*}
lemma TrustCertVerify:
"[| X \<in> parts (spies evs);
X = Crypt (invKey KA) (Hash{|nb, Agent B, pms|});
@@ -470,7 +468,7 @@
by (blast dest!: certificate_valid intro!: TrustCertVerify_lemma)
-(*If CertVerify is present then A has chosen PMS.*)
+text{*If CertVerify is present then A has chosen PMS.*}
lemma UseCertVerify_lemma:
"[| Crypt (priK A) (Hash{|nb, Agent B, Nonce PMS|}) \<in> parts (spies evs);
evs \<in> tls; A \<notin> bad |]
@@ -479,7 +477,7 @@
apply (erule tls.induct, force, simp_all, blast)
done
-(*Final version using the distributed KA instead of priK A*)
+text{*Final version using the distributed KA instead of priK A*}
lemma UseCertVerify:
"[| Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|})
\<in> parts (spies evs);
@@ -492,7 +490,7 @@
lemma no_Notes_A_PRF [simp]:
"evs \<in> tls ==> Notes A {|Agent B, Nonce (PRF x)|} \<notin> set evs"
apply (erule tls.induct, force, simp_all)
-(*ClientKeyExch: PMS is assumed to differ from any PRF.*)
+txt{*ClientKeyExch: PMS is assumed to differ from any PRF.*}
apply blast
done
@@ -502,18 +500,18 @@
==> Nonce PMS \<in> parts (spies evs)"
apply (erule rev_mp)
apply (erule tls.induct, force, simp_all)
-(*Fake*)
+txt{*Fake*}
apply (blast intro: parts_insertI)
-(*Easy, e.g. by freshness*)
+txt{*Easy, e.g. by freshness*}
apply (blast dest: Notes_Crypt_parts_spies)+
done
-(*** Unicity results for PMS, the pre-master-secret ***)
+subsubsection{*Unicity results for PMS, the pre-master-secret*}
-(*PMS determines B.*)
+text{*PMS determines B.*}
lemma Crypt_unique_PMS:
"[| Crypt(pubK B) (Nonce PMS) \<in> parts (spies evs);
Crypt(pubK B') (Nonce PMS) \<in> parts (spies evs);
@@ -522,7 +520,7 @@
==> B=B'"
apply (erule rev_mp, erule rev_mp, erule rev_mp)
apply (erule tls.induct, analz_mono_contra, force, simp_all (no_asm_simp))
-(*Fake, ClientKeyExch*)
+txt{*Fake, ClientKeyExch*}
apply blast+
done
@@ -533,7 +531,7 @@
determines B alone, and only if PMS is secret.
**)
-(*In A's internal Note, PMS determines A and B.*)
+text{*In A's internal Note, PMS determines A and B.*}
lemma Notes_unique_PMS:
"[| Notes A {|Agent B, Nonce PMS|} \<in> set evs;
Notes A' {|Agent B', Nonce PMS|} \<in> set evs;
@@ -541,15 +539,15 @@
==> A=A' & B=B'"
apply (erule rev_mp, erule rev_mp)
apply (erule tls.induct, force, simp_all)
-(*ClientKeyExch*)
+txt{*ClientKeyExch*}
apply (blast dest!: Notes_Crypt_parts_spies)
done
-(**** Secrecy Theorems ****)
+subsection{*Secrecy Theorems*}
-(*Key compromise lemma needed to prove analz_image_keys.
- No collection of keys can help the spy get new private keys.*)
+text{*Key compromise lemma needed to prove analz_image_keys.
+ No collection of keys can help the spy get new private keys.*}
lemma analz_image_priK [rule_format]:
"evs \<in> tls
==> \<forall>KK. (Key(priK B) \<in> analz (Key`KK Un (spies evs))) =
@@ -559,18 +557,18 @@
del: image_insert
add: image_Un [THEN sym]
insert_Key_image Un_assoc [THEN sym])
-(*Fake*)
+txt{*Fake*}
apply spy_analz
done
-(*slightly speeds up the big simplification below*)
+text{*slightly speeds up the big simplification below*}
lemma range_sessionkeys_not_priK:
"KK <= range sessionK ==> priK B \<notin> KK"
by blast
-(*Lemma for the trivial direction of the if-and-only-if*)
+text{*Lemma for the trivial direction of the if-and-only-if*}
lemma analz_image_keys_lemma:
"(X \<in> analz (G Un H)) --> (X \<in> analz H) ==>
(X \<in> analz (G Un H)) = (X \<in> analz H)"
@@ -595,11 +593,11 @@
insert_Key_singleton
range_sessionkeys_not_priK analz_image_priK)
apply (simp_all add: insert_absorb)
-(*Fake*)
+txt{*Fake*}
apply spy_analz
done
-(*Knowing some session keys is no help in getting new nonces*)
+text{*Knowing some session keys is no help in getting new nonces*}
lemma analz_insert_key [simp]:
"evs \<in> tls ==>
(Nonce N \<in> analz (insert (Key (sessionK z)) (spies evs))) =
@@ -608,28 +606,28 @@
add: insert_Key_singleton analz_image_keys)
-(*** Protocol goal: serverK(Na,Nb,M) and clientK(Na,Nb,M) remain secure ***)
+subsubsection{*Protocol goal: serverK(Na,Nb,M) and clientK(Na,Nb,M) remain secure*}
(** Some lemmas about session keys, comprising clientK and serverK **)
-(*Lemma: session keys are never used if PMS is fresh.
+text{*Lemma: session keys are never used if PMS is fresh.
Nonces don't have to agree, allowing session resumption.
Converse doesn't hold; revealing PMS doesn't force the keys to be sent.
- THEY ARE NOT SUITABLE AS SAFE ELIM RULES.*)
+ THEY ARE NOT SUITABLE AS SAFE ELIM RULES.*}
lemma PMS_lemma:
"[| Nonce PMS \<notin> parts (spies evs);
K = sessionK((Na, Nb, PRF(PMS,NA,NB)), role);
evs \<in> tls |]
==> Key K \<notin> parts (spies evs) & (\<forall>Y. Crypt K Y \<notin> parts (spies evs))"
apply (erule rev_mp, erule ssubst)
-apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
+apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (force, simp_all (no_asm_simp))
-(*Fake*)
+txt{*Fake*}
apply (blast intro: parts_insertI)
-(*SpyKeys*)
+txt{*SpyKeys*}
apply blast
-(*Many others*)
+txt{*Many others*}
apply (force dest!: Notes_Crypt_parts_spies Notes_master_imp_Crypt_PMS)+
done
@@ -645,11 +643,11 @@
==> Nonce PMS \<in> parts (spies evs)"
by (blast dest: PMS_lemma)
-(*Write keys are never sent if M (MASTER SECRET) is secure.
+text{*Write keys are never sent if M (MASTER SECRET) is secure.
Converse fails; betraying M doesn't force the keys to be sent!
The strong Oops condition can be weakened later by unicity reasoning,
with some effort.
- NO LONGER USED: see clientK_not_spied and serverK_not_spied*)
+ NO LONGER USED: see clientK_not_spied and serverK_not_spied*}
lemma sessionK_not_spied:
"[| \<forall>A. Says A Spy (Key (sessionK((NA,NB,M),role))) \<notin> set evs;
Nonce M \<notin> analz (spies evs); evs \<in> tls |]
@@ -657,57 +655,57 @@
apply (erule rev_mp, erule rev_mp)
apply (erule tls.induct, analz_mono_contra)
apply (force, simp_all (no_asm_simp))
-(*Fake, SpyKeys*)
+txt{*Fake, SpyKeys*}
apply blast+
done
-(*If A sends ClientKeyExch to an honest B, then the PMS will stay secret.*)
+text{*If A sends ClientKeyExch to an honest B, then the PMS will stay secret.*}
lemma Spy_not_see_PMS:
"[| Notes A {|Agent B, Nonce PMS|} \<in> set evs;
evs \<in> tls; A \<notin> bad; B \<notin> bad |]
==> Nonce PMS \<notin> analz (spies evs)"
apply (erule rev_mp, erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (force, simp_all (no_asm_simp))
-(*Fake*)
+txt{*Fake*}
apply spy_analz
-(*SpyKeys*)
+txt{*SpyKeys*}
apply force
apply (simp_all add: insert_absorb)
-(*ClientHello, ServerHello, ClientKeyExch: mostly freshness reasoning*)
+txt{*ClientHello, ServerHello, ClientKeyExch: mostly freshness reasoning*}
apply (blast dest: Notes_Crypt_parts_spies)
apply (blast dest: Notes_Crypt_parts_spies)
apply (blast dest: Notes_Crypt_parts_spies)
-(*ClientAccepts and ServerAccepts: because PMS \<notin> range PRF*)
+txt{*ClientAccepts and ServerAccepts: because PMS \<notin> range PRF*}
apply force+
done
-(*If A sends ClientKeyExch to an honest B, then the MASTER SECRET
- will stay secret.*)
+text{*If A sends ClientKeyExch to an honest B, then the MASTER SECRET
+ will stay secret.*}
lemma Spy_not_see_MS:
"[| Notes A {|Agent B, Nonce PMS|} \<in> set evs;
evs \<in> tls; A \<notin> bad; B \<notin> bad |]
==> Nonce (PRF(PMS,NA,NB)) \<notin> analz (spies evs)"
apply (erule rev_mp, erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (force, simp_all (no_asm_simp))
-(*Fake*)
+txt{*Fake*}
apply spy_analz
-(*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)
+txt{*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*}
apply (blast dest!: Spy_not_see_PMS)
apply (simp_all add: insert_absorb)
-(*ClientAccepts and ServerAccepts: because PMS was already visible;
- others, freshness etc.*)
+txt{*ClientAccepts and ServerAccepts: because PMS was already visible;
+ others, freshness etc.*}
apply (blast dest: Notes_Crypt_parts_spies Spy_not_see_PMS
Notes_imp_knows_Spy [THEN analz.Inj])+
done
-(*** Weakening the Oops conditions for leakage of clientK ***)
+subsubsection{*Weakening the Oops conditions for leakage of clientK*}
-(*If A created PMS then nobody else (except the Spy in replays)
- would send a message using a clientK generated from that PMS.*)
+text{*If A created PMS then nobody else (except the Spy in replays)
+ would send a message using a clientK generated from that PMS.*}
lemma Says_clientK_unique:
"[| Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) \<in> set evs;
Notes A {|Agent B, Nonce PMS|} \<in> set evs;
@@ -716,16 +714,16 @@
apply (erule rev_mp, erule rev_mp)
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (force, simp_all)
-(*ClientKeyExch*)
+txt{*ClientKeyExch*}
apply (blast dest!: PMS_Crypt_sessionK_not_spied)
-(*ClientFinished, ClientResume: by unicity of PMS*)
+txt{*ClientFinished, ClientResume: by unicity of PMS*}
apply (blast dest!: Notes_master_imp_Notes_PMS
intro: Notes_unique_PMS [THEN conjunct1])+
done
-(*If A created PMS and has not leaked her clientK to the Spy,
- then it is completely secure: not even in parts!*)
+text{*If A created PMS and has not leaked her clientK to the Spy,
+ then it is completely secure: not even in parts!*}
lemma clientK_not_spied:
"[| Notes A {|Agent B, Nonce PMS|} \<in> set evs;
Says A Spy (Key (clientK(Na,Nb,PRF(PMS,NA,NB)))) \<notin> set evs;
@@ -735,21 +733,21 @@
apply (erule rev_mp, erule rev_mp)
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (force, simp_all (no_asm_simp))
-(*ClientKeyExch*)
+txt{*ClientKeyExch*}
apply blast
-(*SpyKeys*)
+txt{*SpyKeys*}
apply (blast dest!: Spy_not_see_MS)
-(*ClientKeyExch*)
+txt{*ClientKeyExch*}
apply (blast dest!: PMS_sessionK_not_spied)
-(*Oops*)
+txt{*Oops*}
apply (blast intro: Says_clientK_unique)
done
-(*** Weakening the Oops conditions for leakage of serverK ***)
+subsubsection{*Weakening the Oops conditions for leakage of serverK*}
-(*If A created PMS for B, then nobody other than B or the Spy would
- send a message using a serverK generated from that PMS.*)
+text{*If A created PMS for B, then nobody other than B or the Spy would
+ send a message using a serverK generated from that PMS.*}
lemma Says_serverK_unique:
"[| Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) \<in> set evs;
Notes A {|Agent B, Nonce PMS|} \<in> set evs;
@@ -758,16 +756,16 @@
apply (erule rev_mp, erule rev_mp)
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (force, simp_all)
-(*ClientKeyExch*)
+txt{*ClientKeyExch*}
apply (blast dest!: PMS_Crypt_sessionK_not_spied)
-(*ServerResume, ServerFinished: by unicity of PMS*)
+txt{*ServerResume, ServerFinished: by unicity of PMS*}
apply (blast dest!: Notes_master_imp_Crypt_PMS
dest: Spy_not_see_PMS Notes_Crypt_parts_spies Crypt_unique_PMS)+
done
-(*If A created PMS for B, and B has not leaked his serverK to the Spy,
- then it is completely secure: not even in parts!*)
+text{*If A created PMS for B, and B has not leaked his serverK to the Spy,
+ then it is completely secure: not even in parts!*}
lemma serverK_not_spied:
"[| Notes A {|Agent B, Nonce PMS|} \<in> set evs;
Says B Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) \<notin> set evs;
@@ -776,23 +774,23 @@
apply (erule rev_mp, erule rev_mp)
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (force, simp_all (no_asm_simp))
-(*Fake*)
+txt{*Fake*}
apply blast
-(*SpyKeys*)
+txt{*SpyKeys*}
apply (blast dest!: Spy_not_see_MS)
-(*ClientKeyExch*)
+txt{*ClientKeyExch*}
apply (blast dest!: PMS_sessionK_not_spied)
-(*Oops*)
+txt{*Oops*}
apply (blast intro: Says_serverK_unique)
done
-(*** Protocol goals: if A receives ServerFinished, then B is present
+subsubsection{*Protocol goals: if A receives ServerFinished, then B is present
and has used the quoted values PA, PB, etc. Note that it is up to A
to compare PA with what she originally sent.
***)
-(*The mention of her name (A) in X assures A that B knows who she is.*)
+text{*The mention of her name (A) in X assures A that B knows who she is.*}
lemma TrustServerFinished [rule_format]:
"[| X = Crypt (serverK(Na,Nb,M))
(Hash{|Number SID, Nonce M,
@@ -806,17 +804,17 @@
apply (erule ssubst)+
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (force, simp_all (no_asm_simp))
-(*Fake: the Spy doesn't have the critical session key!*)
+txt{*Fake: the Spy doesn't have the critical session key!*}
apply (blast dest: serverK_not_spied)
-(*ClientKeyExch*)
+txt{*ClientKeyExch*}
apply (blast dest!: PMS_Crypt_sessionK_not_spied)
done
-(*This version refers not to ServerFinished but to any message from B.
+text{*This version refers not to ServerFinished but to any message from B.
We don't assume B has received CertVerify, and an intruder could
have changed A's identity in all other messages, so we can't be sure
that B sends his message to A. If CLIENT KEY EXCHANGE were augmented
- to bind A's identity with PMS, then we could replace A' by A below.*)
+ to bind A's identity with PMS, then we could replace A' by A below.*}
lemma TrustServerMsg [rule_format]:
"[| M = PRF(PMS,NA,NB); evs \<in> tls; A \<notin> bad; B \<notin> bad |]
==> Says B Spy (Key(serverK(Na,Nb,M))) \<notin> set evs -->
@@ -826,21 +824,22 @@
apply (erule ssubst)
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (force, simp_all (no_asm_simp) add: ex_disj_distrib)
-(*Fake: the Spy doesn't have the critical session key!*)
+txt{*Fake: the Spy doesn't have the critical session key!*}
apply (blast dest: serverK_not_spied)
-(*ClientKeyExch*)
+txt{*ClientKeyExch*}
apply (clarify, blast dest!: PMS_Crypt_sessionK_not_spied)
-(*ServerResume, ServerFinished: by unicity of PMS*)
+txt{*ServerResume, ServerFinished: by unicity of PMS*}
apply (blast dest!: Notes_master_imp_Crypt_PMS
dest: Spy_not_see_PMS Notes_Crypt_parts_spies Crypt_unique_PMS)+
done
-(*** Protocol goal: if B receives any message encrypted with clientK
- then A has sent it, ASSUMING that A chose PMS. Authentication is
+subsubsection{*Protocol goal: if B receives any message encrypted with clientK
+ then A has sent it*}
+
+text{*ASSUMING that A chose PMS. Authentication is
assumed here; B cannot verify it. But if the message is
- ClientFinished, then B can then check the quoted values PA, PB, etc.
-***)
+ ClientFinished, then B can then check the quoted values PA, PB, etc.*}
lemma TrustClientMsg [rule_format]:
"[| M = PRF(PMS,NA,NB); evs \<in> tls; A \<notin> bad; B \<notin> bad |]
@@ -851,19 +850,19 @@
apply (erule ssubst)
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (force, simp_all (no_asm_simp))
-(*Fake: the Spy doesn't have the critical session key!*)
+txt{*Fake: the Spy doesn't have the critical session key!*}
apply (blast dest: clientK_not_spied)
-(*ClientKeyExch*)
+txt{*ClientKeyExch*}
apply (blast dest!: PMS_Crypt_sessionK_not_spied)
-(*ClientFinished, ClientResume: by unicity of PMS*)
+txt{*ClientFinished, ClientResume: by unicity of PMS*}
apply (blast dest!: Notes_master_imp_Notes_PMS dest: Notes_unique_PMS)+
done
-(*** Protocol goal: if B receives ClientFinished, and if B is able to
+subsubsection{*Protocol goal: if B receives ClientFinished, and if B is able to
check a CertVerify from A, then A has used the quoted
values PA, PB, etc. Even this one requires A to be uncompromised.
- ***)
+*}
lemma AuthClientFinished:
"[| M = PRF(PMS,NA,NB);
Says A Spy (Key(clientK(Na,Nb,M))) \<notin> set evs;