--- a/src/HOL/Auth/CertifiedEmail.thy Fri Aug 08 15:05:11 2003 +0200
+++ b/src/HOL/Auth/CertifiedEmail.thy Tue Aug 12 13:35:03 2003 +0200
@@ -39,12 +39,12 @@
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))|]
+ "[| evsf \<in> certified_mail; X \<in> synth(analz(spies 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))|]
+ "[| evsfssl \<in> certified_mail; X \<in> synth(analz(spies evsfssl))|]
==> Notes TTP {|Agent Spy, Agent TTP, X|} # evsfssl \<in> certified_mail"
CM1: --{*The sender approaches the recipient. The message is a number.*}
@@ -89,6 +89,9 @@
==> Gets B X#evsr \<in> certified_mail"
+declare Says_imp_knows_Spy [THEN analz.Inj, dest]
+declare analz_into_parts [dest]
+
(*A "possibility property": there are traces that reach the end*)
lemma "\<exists>S2TTP. \<exists>evs \<in> certified_mail.
Says TTP S (Crypt (priSK TTP) S2TTP) \<in> set evs"
@@ -118,7 +121,7 @@
"[|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)"
+ ==> S2TTP \<in> analz(spies evs)"
apply (drule Gets_imp_Says, simp)
apply (blast dest: Says_imp_knows_Spy analz.Inj)
done
@@ -128,7 +131,7 @@
lemma hr_form_lemma [rule_format]:
"evs \<in> certified_mail
- ==> hr \<notin> synth (analz (knows Spy evs)) -->
+ ==> hr \<notin> synth (analz (spies 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|}))"
@@ -142,39 +145,39 @@
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)) |
+ ==> hr \<in> synth (analz (spies 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"
+lemma Spy_dont_know_private_keys [dest!]:
+ "[|Key (privateKey b A) \<in> parts (spies evs); evs \<in> certified_mail|]
+ ==> A \<in> bad"
+apply (erule rev_mp)
apply (erule certified_mail.induct, simp_all)
txt{*Fake*}
-apply (blast dest: Fake_parts_insert[THEN subsetD]
- analz_subset_parts[THEN subsetD])
+apply (blast dest: Fake_parts_insert_in_Un);
txt{*Message 1*}
apply blast
txt{*Message 3*}
apply (frule_tac hr_form, assumption)
apply (elim disjE exE)
apply (simp_all add: parts_insert2)
- apply (force dest!: parts_insert_subset_Un[THEN [2] rev_subsetD]
- analz_subset_parts[THEN subsetD], blast)
+ 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)
+by (blast intro: elim:);
lemma Spy_dont_know_TTPKey_parts [simp]:
- "evs \<in> certified_mail ==> Key (privateKey b TTP) \<notin> parts(knows Spy evs)"
+ "evs \<in> certified_mail ==> Key (privateKey b TTP) \<notin> parts(spies evs)"
by simp
lemma Spy_dont_know_TTPKey_analz [simp]:
- "evs \<in> certified_mail ==> Key (privateKey b TTP) \<notin> analz(knows Spy evs)"
-by (force dest!: analz_subset_parts[THEN subsetD])
+ "evs \<in> certified_mail ==> Key (privateKey b TTP) \<notin> analz(spies evs)"
+by auto
text{*Thus, prove any goal that assumes that @{term Spy} knows a private key
belonging to @{term TTP}*}
@@ -192,10 +195,9 @@
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)
+apply (blast dest: parts.Body)
txt{*Message 2*}
-apply (blast dest!: Says_imp_knows_Spy [THEN parts.Inj] Gets_imp_Says
- elim!: knows_Spy_partsEs)
+apply (blast dest!: Gets_imp_Says elim!: knows_Spy_partsEs)
txt{*Message 3*}
apply (frule_tac hr_form, assumption)
apply (elim disjE exE)
@@ -207,8 +209,7 @@
"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])
+apply (blast dest: Fake_parts_insert_in_Un);
txt{*Message 1*}
apply blast
txt{*Message 3*}
@@ -216,18 +217,18 @@
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])
+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)"
+ "evs \<in> certified_mail ==> (Key (RPwd A) \<in> parts(spies 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]])
+ "evs \<in> certified_mail ==> (Key (RPwd A) \<in> analz(spies 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*}
@@ -237,16 +238,15 @@
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])
+apply (blast dest: Spy_dont_know_private_keys Fake_parts_insert_in_Un)
txt{*Message 1*}
apply blast
txt{*Message 3*}
apply (frule_tac hr_form, assumption)
apply (elim disjE exE)
-apply (simp_all add: parts_insert2)
-apply (force dest!: parts_insert_subset_Un[THEN [2] rev_subsetD]
- analz_subset_parts[THEN subsetD], blast)
+apply (simp_all add: parts_insert2 parts_insert_knows_A)
+ apply (blast dest!: Fake_parts_sing_imp_Un)
+apply (blast intro: elim:);
done
@@ -255,8 +255,8 @@
lemma analz_image_freshK [rule_format]:
"evs \<in> certified_mail ==>
\<forall>K KK. invKey (pubEK TTP) \<notin> KK -->
- (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
- (K \<in> KK | Key K \<in> analz (knows Spy evs))"
+ (Key K \<in> analz (Key`KK Un (spies evs))) =
+ (K \<in> KK | Key K \<in> analz (spies evs))"
apply (erule certified_mail.induct)
apply (drule_tac [6] A=TTP in symKey_neq_priEK)
apply (erule_tac [6] disjE [OF hr_form])
@@ -272,8 +272,8 @@
lemma analz_insert_freshK:
"[| evs \<in> certified_mail; KAB \<noteq> invKey (pubEK TTP) |] ==>
- (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
- (K = KAB | Key K \<in> analz (knows Spy evs))"
+ (Key K \<in> analz (insert (Key KAB) (spies evs))) =
+ (K = KAB | Key K \<in> analz (spies evs))"
by (simp only: analz_image_freshK analz_image_freshK_simps)
text{*@{term S2TTP} must have originated from a valid sender
@@ -284,11 +284,11 @@
by (blast dest!: Notes_imp_used)
-(*The weaker version, replacing "used evs" by "parts (knows Spy evs)",
+(*The weaker version, replacing "used evs" by "parts (spies evs)",
isn't inductive: message 3 case can't be proved *)
lemma S2TTP_sender_lemma [rule_format]:
"evs \<in> certified_mail ==>
- Key K \<notin> analz (knows Spy evs) -->
+ Key K \<notin> analz (spies evs) -->
(\<forall>AO. Crypt (pubEK TTP)
{|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs -->
(\<exists>m ctxt q.
@@ -302,11 +302,11 @@
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])
+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])
+apply (blast dest: Fake_parts_sing [THEN subsetD]
+ dest: analz_subset_parts [THEN subsetD])
txt{*Message 1*}
apply (clarsimp, blast)
txt{*Message 2*}
@@ -319,7 +319,7 @@
lemma S2TTP_sender:
"[|Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs;
- Key K \<notin> analz (knows Spy evs);
+ Key K \<notin> analz (spies evs);
evs \<in> certified_mail|]
==> \<exists>m ctxt q.
hs = Hash{|Number ctxt, Nonce q, response S R q, Crypt K (Number m)|} &
@@ -353,7 +353,7 @@
where @{term K} is secure.*}
lemma Key_unique_lemma [rule_format]:
"evs \<in> certified_mail ==>
- Key K \<notin> analz (knows Spy evs) -->
+ Key K \<notin> analz (spies evs) -->
(\<forall>m cleartext q hs.
Says S R
{|Agent S, Agent TTP, Crypt K (Number m), Number AO,
@@ -367,10 +367,11 @@
Crypt (pubEK TTP) {|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)
+ prefer 2
+ txt{*Message 1*}
+ apply (blast dest!: Says_imp_knows_Spy [THEN parts.Inj] new_keys_not_used Crypt_imp_keysFor)
+txt{*Fake*}
+apply (auto dest!: usedI S2TTP_sender analz_subset_parts [THEN subsetD])
done
text{*The key determines the sender, recipient and protocol options.*}
@@ -385,7 +386,7 @@
Number cleartext', Nonce q',
Crypt (pubEK TTP) {|Agent S', Number AO', Key K, Agent R', hs'|}|}
\<in> set evs;
- Key K \<notin> analz (knows Spy evs);
+ Key K \<notin> analz (spies evs);
evs \<in> certified_mail|]
==> R' = R & S' = S & AO' = AO & hs' = hs"
by (rule Key_unique_lemma, assumption+)
@@ -400,7 +401,7 @@
"[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
Number cleartext, Nonce q, S2TTP|} \<in> set evs;
S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|};
- Key K \<in> analz(knows Spy evs);
+ Key K \<in> analz(spies evs);
evs \<in> certified_mail;
S\<noteq>Spy|]
==> R \<in> bad & Gets S (Crypt (priSK TTP) S2TTP) \<in> set evs"
@@ -430,7 +431,7 @@
S2TTP = Crypt (pubEK TTP) {|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)"
+ ==> Key K \<notin> analz(spies evs)"
by (blast dest: Spy_see_encrypted_key_imp)
@@ -471,19 +472,19 @@
apply (erule ssubst)
apply (erule certified_mail.induct, simp_all)
txt{*Fake*}
-apply (blast dest: Fake_parts_sing[THEN subsetD]
- dest!: analz_subset_parts[THEN subsetD])
+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])
+apply (blast dest: Fake_parts_sing [THEN subsetD]
+ dest!: analz_subset_parts [THEN subsetD])
txt{*Message 2*}
apply (drule CM2_S2TTP_parts_knows_Spy, assumption)
apply (force dest: parts_cut)
txt{*Message 3*}
apply (frule_tac hr_form, assumption)
apply (elim disjE exE, simp_all)
-apply (blast dest: Fake_parts_sing[THEN subsetD]
- dest!: analz_subset_parts[THEN subsetD])
+apply (blast dest: Fake_parts_sing [THEN subsetD]
+ dest!: analz_subset_parts [THEN subsetD])
done
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/ZhouGollmann.thy Tue Aug 12 13:35:03 2003 +0200
@@ -0,0 +1,463 @@
+(* Title: HOL/Auth/ZhouGollmann
+ ID: $Id$
+ Author: Giampaolo Bella and L C Paulson, Cambridge Univ Computer Lab
+ Copyright 2003 University of Cambridge
+
+The protocol of
+ Jianying Zhou and Dieter Gollmann,
+ A Fair Non-Repudiation Protocol,
+ Security and Privacy 1996 (Oakland)
+ 55-61
+*)
+
+theory ZhouGollmann = Public:
+
+syntax
+ TTP :: agent
+
+translations
+ "TTP" == "Server"
+
+syntax
+ f_sub :: nat
+ f_nro :: nat
+ f_nrr :: nat
+ f_con :: nat
+
+translations
+ "f_sub" == "5"
+ "f_nro" == "2"
+ "f_nrr" == "3"
+ "f_con" == "4"
+
+
+constdefs
+ broken :: "agent set"
+ --{*the compromised honest agents; TTP is included as it's not allowed to
+ use the protocol*}
+ "broken == insert TTP (bad - {Spy})"
+
+declare broken_def [simp]
+
+consts zg :: "event list set"
+
+inductive zg
+ intros
+
+ Nil: "[] \<in> zg"
+
+ Fake: "[| evsf \<in> zg; X \<in> synth (analz (spies evsf)) |]
+ ==> Says Spy B X # evsf \<in> zg"
+
+Reception: "[| evsr \<in> zg; A \<noteq> B; Says A B X \<in> set evsr |]
+ ==> Gets B X # evsr \<in> zg"
+
+ (*L is fresh for honest agents.
+ We don't require K to be fresh because we don't bother to prove secrecy!
+ We just assume that the protocol's objective is to deliver K fairly,
+ rather than to keep M secret.*)
+ ZG1: "[| evs1 \<in> zg; Nonce L \<notin> used evs1; C = Crypt K (Number m);
+ K \<in> symKeys;
+ NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|}|]
+ ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} # evs1 \<in> zg"
+
+ (*B must check that NRO is A's signature to learn the sender's name*)
+ ZG2: "[| evs2 \<in> zg;
+ Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs2;
+ NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
+ NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|}|]
+ ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} # evs2 \<in> zg"
+
+ (*K is symmetric must be repeated IF there's spy*)
+ (*A must check that NRR is B's signature to learn the sender's name*)
+ (*without spy, the matching label would be enough*)
+ ZG3: "[| evs3 \<in> zg; C = Crypt K M; K \<in> symKeys;
+ Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs3;
+ Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs3;
+ NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
+ sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|}|]
+ ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|}
+ # evs3 \<in> zg"
+
+ (*TTP checks that sub_K is A's signature to learn who issued K, then
+ gives credentials to A and B. The Notes event models the availability of
+ the credentials, but the act of fetching them is not modelled.*)
+ (*Also said TTP_prepare_ftp*)
+ ZG4: "[| evs4 \<in> zg; K \<in> symKeys;
+ Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|}
+ \<in> set evs4;
+ sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+ con_K = Crypt (priK TTP) {|Number f_con, Agent A, Agent B,
+ Nonce L, Key K|}|]
+ ==> Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
+ # evs4 \<in> zg"
+
+
+declare Says_imp_knows_Spy [THEN analz.Inj, dest]
+declare Fake_parts_insert_in_Un [dest]
+declare analz_into_parts [dest]
+
+declare symKey_neq_priEK [simp]
+declare symKey_neq_priEK [THEN not_sym, simp]
+
+
+subsection {*Basic Lemmas*}
+
+lemma Gets_imp_Says:
+ "[| Gets B X \<in> set evs; evs \<in> zg |] ==> \<exists>A. Says A B X \<in> set evs"
+apply (erule rev_mp)
+apply (erule zg.induct, auto)
+done
+
+lemma Gets_imp_knows_Spy:
+ "[| Gets B X \<in> set evs; evs \<in> zg |] ==> X \<in> spies evs"
+by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
+
+
+text{*Lets us replace proofs about @{term "used evs"} by simpler proofs
+about @{term "parts (spies evs)"}.*}
+lemma Crypt_used_imp_spies:
+ "[| Crypt K X \<in> used evs; K \<noteq> priK TTP; evs \<in> zg |]
+ ==> Crypt K X \<in> parts (spies evs)"
+apply (erule rev_mp)
+apply (erule zg.induct)
+apply (simp_all add: parts_insert_knows_A)
+done
+
+lemma Notes_TTP_imp_Gets:
+ "[|Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K |}
+ \<in> set evs;
+ sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+ evs \<in> zg|]
+ ==> Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
+apply (erule rev_mp)
+apply (erule zg.induct, auto)
+done
+
+text{*For reasoning about C, which is encrypted in message ZG2*}
+lemma ZG2_msg_in_parts_spies:
+ "[|Gets B {|F, B', L, C, X|} \<in> set evs; evs \<in> zg|]
+ ==> C \<in> parts (spies evs)"
+by (blast dest: Gets_imp_Says)
+
+(*classical regularity lemma on priK*)
+lemma Spy_see_priK [simp]:
+ "evs \<in> zg ==> (Key (priK A) \<in> parts (spies evs)) = (A \<in> bad)"
+apply (erule zg.induct)
+apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)
+done
+
+text{*So that blast can use it too*}
+declare Spy_see_priK [THEN [2] rev_iffD1, dest!]
+
+lemma Spy_analz_priK [simp]:
+ "evs \<in> zg ==> (Key (priK A) \<in> analz (spies evs)) = (A \<in> bad)"
+by auto
+
+
+subsection{*About NRO*}
+
+text{*Below we prove that if @{term NRO} exists then @{term A} definitely
+sent it, provided @{term A} is not broken. *}
+
+text{*Strong conclusion for a good agent*}
+lemma NRO_authenticity_good:
+ "[| NRO \<in> parts (spies evs);
+ NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
+ A \<notin> bad; evs \<in> zg |]
+ ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs"
+apply clarify
+apply (erule rev_mp)
+apply (erule zg.induct)
+apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)
+done
+
+text{*A compromised agent: we can't be sure whether A or the Spy sends the
+message or of the precise form of the message*}
+lemma NRO_authenticity_bad:
+ "[| NRO \<in> parts (spies evs);
+ NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
+ A \<in> bad; evs \<in> zg |]
+ ==> \<exists>A' \<in> {A,Spy}. \<exists>C Y. Says A' C Y \<in> set evs & NRO \<in> parts {Y}"
+apply clarify
+apply (erule rev_mp)
+apply (erule zg.induct)
+apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
+txt{*ZG3*}
+ prefer 4 apply blast
+txt{*ZG2*}
+ prefer 3 apply blast
+txt{*Fake*}
+apply (simp add: parts_insert_knows_A, blast)
+txt{*ZG1*}
+apply (auto intro!: exI)
+done
+
+theorem NRO_authenticity:
+ "[| NRO \<in> used evs;
+ NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
+ A \<notin> broken; evs \<in> zg |]
+ ==> \<exists>C Y. Says A C Y \<in> set evs & NRO \<in> parts {Y}"
+apply auto
+ apply (force dest!: Crypt_used_imp_spies NRO_authenticity_good)
+apply (force dest!: Crypt_used_imp_spies NRO_authenticity_bad)
+done
+
+
+subsection{*About NRR*}
+
+text{*Below we prove that if @{term NRR} exists then @{term B} definitely
+sent it, provided @{term B} is not broken.*}
+
+text{*Strong conclusion for a good agent*}
+lemma NRR_authenticity_good:
+ "[| NRR \<in> parts (spies evs);
+ NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
+ B \<notin> bad; evs \<in> zg |]
+ ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
+apply clarify
+apply (erule rev_mp)
+apply (erule zg.induct)
+apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)
+done
+
+lemma NRR_authenticity_bad:
+ "[| NRR \<in> parts (spies evs);
+ NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
+ B \<in> bad; evs \<in> zg |]
+ ==> \<exists>B' \<in> {B,Spy}. \<exists>C Y. Says B' C Y \<in> set evs & NRR \<in> parts {Y}"
+apply clarify
+apply (erule rev_mp)
+apply (erule zg.induct)
+apply (frule_tac [5] ZG2_msg_in_parts_spies)
+apply (simp_all del: bex_simps)
+txt{*ZG3*}
+ prefer 4 apply blast
+txt{*Fake*}
+apply (simp add: parts_insert_knows_A, blast)
+txt{*ZG1*}
+apply (auto simp del: bex_simps)
+txt{*ZG2*}
+apply (force intro!: exI)
+done
+
+theorem NRR_authenticity:
+ "[| NRR \<in> used evs;
+ NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
+ B \<notin> broken; evs \<in> zg |]
+ ==> \<exists>C Y. Says B C Y \<in> set evs & NRR \<in> parts {Y}"
+apply auto
+ apply (force dest!: Crypt_used_imp_spies NRR_authenticity_good)
+apply (force dest!: Crypt_used_imp_spies NRR_authenticity_bad)
+done
+
+
+subsection{*Proofs About @{term sub_K}*}
+
+text{*Below we prove that if @{term sub_K} exists then @{term A} definitely
+sent it, provided @{term A} is not broken. *}
+
+text{*Strong conclusion for a good agent*}
+lemma sub_K_authenticity_good:
+ "[| sub_K \<in> parts (spies evs);
+ sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+ A \<notin> bad; evs \<in> zg |]
+ ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
+apply (erule rev_mp)
+apply (erule zg.induct)
+apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
+txt{*Fake*}
+apply (blast dest!: Fake_parts_sing_imp_Un)
+done
+
+text{*A compromised agent: we can't be sure whether A or the Spy sends the
+message or of the precise form of the message*}
+lemma sub_K_authenticity_bad:
+ "[| sub_K \<in> parts (spies evs);
+ sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+ A \<in> bad; evs \<in> zg |]
+ ==> \<exists>A' \<in> {A,Spy}. \<exists>C Y. Says A' C Y \<in> set evs & sub_K \<in> parts {Y}"
+apply clarify
+apply (erule rev_mp)
+apply (erule zg.induct)
+apply (frule_tac [5] ZG2_msg_in_parts_spies)
+apply (simp_all del: bex_simps)
+txt{*Fake*}
+apply (simp add: parts_insert_knows_A, blast)
+txt{*ZG1*}
+apply (auto simp del: bex_simps)
+txt{*ZG3*}
+apply (force intro!: exI)
+done
+
+theorem sub_K_authenticity:
+ "[| sub_K \<in> used evs;
+ sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+ A \<notin> broken; evs \<in> zg |]
+ ==> \<exists>C Y. Says A C Y \<in> set evs & sub_K \<in> parts {Y}"
+apply auto
+ apply (force dest!: Crypt_used_imp_spies sub_K_authenticity_good)
+apply (force dest!: Crypt_used_imp_spies sub_K_authenticity_bad)
+done
+
+
+subsection{*Proofs About @{term con_K}*}
+
+text{*Below we prove that if @{term con_K} exists, then @{term TTP} has it,
+and therefore @{term A} and @{term B}) can get it too. Moreover, we know
+that @{term A} sent @{term sub_K}*}
+
+lemma con_K_authenticity:
+ "[|con_K \<in> used evs;
+ con_K = Crypt (priK TTP)
+ {|Number f_con, Agent A, Agent B, Nonce L, Key K|};
+ evs \<in> zg |]
+ ==> Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
+ \<in> set evs"
+apply clarify
+apply (erule rev_mp)
+apply (erule zg.induct)
+apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
+txt{*Fake*}
+apply (blast dest!: Fake_parts_sing_imp_Un)
+txt{*ZG2*}
+apply (blast dest: parts_cut)
+done
+
+text{*If @{term TTP} holds @{term con_K} then @{term A} sent
+ @{term sub_K}. We assume that @{term A} is not broken. Nothing needs to
+ be assumed about the form of @{term con_K}!*}
+lemma Notes_TTP_imp_Says_A:
+ "[|Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
+ \<in> set evs;
+ sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+ A \<notin> broken; evs \<in> zg|]
+ ==> \<exists>C Y. Says A C Y \<in> set evs & sub_K \<in> parts {Y}"
+by (blast dest!: Notes_TTP_imp_Gets [THEN Gets_imp_knows_Spy, THEN parts.Inj] intro: sub_K_authenticity)
+
+text{*If @{term con_K} exists, then @{term A} sent @{term sub_K}.*}
+theorem B_sub_K_authenticity:
+ "[|con_K \<in> used evs;
+ con_K = Crypt (priK TTP) {|Number f_con, Agent A, Agent B,
+ Nonce L, Key K|};
+ sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+ A \<notin> broken; B \<noteq> TTP; evs \<in> zg|]
+ ==> \<exists>C Y. Says A C Y \<in> set evs & sub_K \<in> parts {Y}"
+by (blast dest: con_K_authenticity Notes_TTP_imp_Says_A)
+
+
+subsection{*Proving fairness*}
+
+text{*Cannot prove that, if @{term B} has NRO, then @{term A} has her NRR.
+It would appear that @{term B} has a small advantage, though it is
+useless to win disputes: @{term B} needs to present @{term con_K} as well.*}
+
+text{*Strange: unicity of the label protects @{term A}?*}
+lemma A_unicity:
+ "[|NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
+ NRO \<in> parts (spies evs);
+ Says A B {|Number f_nro, Agent B, Nonce L, Crypt K M', NRO'|}
+ \<in> set evs;
+ A \<notin> bad; evs \<in> zg |]
+ ==> M'=M"
+apply clarify
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule zg.induct)
+apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)
+txt{*ZG1: freshness*}
+apply (blast dest: parts.Body)
+done
+
+
+text{*Fairness lemma: if @{term sub_K} exists, then @{term A} holds
+NRR. Relies on unicity of labels.*}
+lemma sub_K_implies_NRR:
+ "[| sub_K \<in> parts (spies evs);
+ NRO \<in> parts (spies evs);
+ sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+ NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
+ NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, Crypt K M|};
+ A \<notin> bad; evs \<in> zg |]
+ ==> Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
+apply clarify
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule zg.induct)
+apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
+txt{*Fake*}
+apply blast
+txt{*ZG1: freshness*}
+apply (blast dest: parts.Body)
+txt{*ZG3*}
+apply (blast dest: A_unicity [OF refl])
+done
+
+
+lemma Crypt_used_imp_L_used:
+ "[| Crypt (priK TTP) {|F, A, B, L, K|} \<in> used evs; evs \<in> zg |]
+ ==> L \<in> used evs"
+apply (erule rev_mp)
+apply (erule zg.induct, auto)
+txt{*Fake*}
+apply (blast dest!: Fake_parts_sing_imp_Un)
+txt{*ZG2: freshness*}
+apply (blast dest: parts.Body)
+done
+
+
+text{*Fairness for @{term A}: if @{term con_K} and @{term NRO} exist,
+then @{term A} holds NRR. @{term A} must be uncompromised, but there is no
+assumption about @{term B}.*}
+theorem A_fairness_NRO:
+ "[|con_K \<in> used evs;
+ NRO \<in> parts (spies evs);
+ con_K = Crypt (priK TTP)
+ {|Number f_con, Agent A, Agent B, Nonce L, Key K|};
+ NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
+ NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, Crypt K M|};
+ A \<notin> bad; evs \<in> zg |]
+ ==> Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
+apply clarify
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule zg.induct)
+apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
+ txt{*Fake*}
+ apply (simp add: parts_insert_knows_A)
+ apply (blast dest: Fake_parts_sing_imp_Un)
+ txt{*ZG1*}
+ apply (blast dest: Crypt_used_imp_L_used)
+ txt{*ZG2*}
+ apply (blast dest: parts_cut)
+txt{*ZG4*}
+apply (blast intro: sub_K_implies_NRR [OF _ _ refl]
+ dest: Gets_imp_knows_Spy [THEN parts.Inj])
+done
+
+text{*Fairness for @{term B}: NRR exists at all, then @{term B} holds NRO.
+@{term B} must be uncompromised, but there is no assumption about @{term
+A}. *}
+theorem B_fairness_NRR:
+ "[|NRR \<in> used evs;
+ NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
+ NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
+ B \<notin> bad; evs \<in> zg |]
+ ==> Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs"
+apply clarify
+apply (erule rev_mp)
+apply (erule zg.induct)
+apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
+txt{*Fake*}
+apply (blast dest!: Fake_parts_sing_imp_Un)
+txt{*ZG2*}
+apply (blast dest: parts_cut)
+done
+
+
+text{*If @{term con_K} exists at all, then @{term B} can get it, by @{text
+con_K_authenticity}. Cannot conclude that also NRO is available to @{term B},
+because if @{term A} were unfair, @{term A} could build message 3 without
+building message 1, which contains NRO. *}
+
+end