definition broken :: "agent set"where \<comment> \<open>the compromised honest agents; TTP is included as it's not allowed to use the protocol\<close> "broken == bad - {Spy}"
declare broken_def [simp]
inductive_set zg :: "event list set" where
Nil: "[] \ zg"
| Fake: "\evsf \ zg; X \ synth (analz (spies evsf))\ \<Longrightarrow> Says Spy B X # evsf \<in> zg"
| Reception: "\evsr \ zg; Says A B X \ set evsr\ \ Gets B X # evsr \ 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 \ zg; Nonce L \ used evs1; C = Crypt K (Number m);
K \<in> symKeys;
NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, C\<rbrace>\<rbrakk> \<Longrightarrow> Says A B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> # evs1 \<in> zg"
(*B must check that NRO is A's signature to learn the sender's name*)
| ZG2: "\evs2 \ zg;
Gets B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<in> set evs2;
NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, C\<rbrace>;
NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, C\<rbrace>\<rbrakk> \<Longrightarrow> Says B A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> # evs2 \<in> zg"
(*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 \ zg; C = Crypt K M; K \ symKeys;
Says A B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<in> set evs3;
Gets A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set evs3;
NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, C\<rbrace>;
sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrakk> \<Longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace>
# 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. We also give con_K to the Spy. This makes the threat model more dangerous, while also allowing lemma @{text Crypt_used_imp_spies} to omit the condition
@{term "K \<noteq> priK TTP"}. *)
| ZG4: "\evs4 \ zg; K \ symKeys;
Gets TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs4;
sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
con_K = Crypt (priK TTP) \<lbrace>Number f_con, Agent A, Agent B,
Nonce L, Key K\<rbrace>\<rbrakk> \<Longrightarrow> Says TTP Spy con_K
# Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace>
# evs4 \<in> zg"
text\<open>A "possibility property": there are traces that reach the end\<close> lemma"\A \ B; TTP \ A; TTP \ B; K \ symKeys\ \ \<exists>L. \<exists>evs \<in> zg. Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K,
Crypt (priK TTP) \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set evs" apply (intro exI bexI) apply (rule_tac [2] zg.Nil
[THEN zg.ZG1, THEN zg.Reception [of _ A B], THEN zg.ZG2, THEN zg.Reception [of _ B A], THEN zg.ZG3, THEN zg.Reception [of _ A TTP], THEN zg.ZG4]) apply (basic_possibility, auto) done
subsection \<open>Basic Lemmas\<close>
lemma Gets_imp_Says: "\Gets B X \ set evs; evs \ zg\ \ \A. Says A B X \ set evs" apply (erule rev_mp) apply (erule zg.induct, auto) done
lemma Gets_imp_knows_Spy: "\Gets B X \ set evs; evs \ zg\ \ X \ spies evs" by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
text\<open>Lets us replace proofs about \<^term>\<open>used evs\<close> by simpler proofs
about \<^term>\<open>parts (spies evs)\<close>.\<close> lemma Crypt_used_imp_spies: "\Crypt K X \ used evs; evs \ zg\ \<Longrightarrow> Crypt K X \<in> parts (spies evs)" apply (erule rev_mp) apply (erule zg.induct) apply (simp_all add: parts_insert_knows_A) done
text\<open>For reasoning about C, which is encrypted in message ZG2\<close> lemma ZG2_msg_in_parts_spies: "\Gets B \F, B', L, C, X\ \ set evs; evs \ zg\ \<Longrightarrow> C \<in> parts (spies evs)" by (blast dest: Gets_imp_Says)
(*classical regularity lemma on priK*) lemma Spy_see_priK [simp]: "evs \ zg \ (Key (priK A) \ parts (spies evs)) = (A \ bad)" apply (erule zg.induct) apply (frule_tac [5] ZG2_msg_in_parts_spies, auto) done
text\<open>So that blast can use it too\<close> declare Spy_see_priK [THEN [2] rev_iffD1, dest!]
lemma Spy_analz_priK [simp]: "evs \ zg \ (Key (priK A) \ analz (spies evs)) = (A \ bad)" by auto
subsection\<open>About NRO: Validity for \<^term>\<open>B\<close>\<close>
text\<open>Below we prove that if \<^term>\<open>NRO\<close> exists then \<^term>\<open>A\<close> definitely
sent it, provided \<^term>\<open>A\<close> is not broken.\<close>
text\<open>Strong conclusion for a good agent\<close> lemma NRO_validity_good: "\NRO = Crypt (priK A) \Number f_nro, Agent B, Nonce L, C\;
NRO \<in> parts (spies evs);
A \<notin> bad; evs \<in> zg\<rbrakk> \<Longrightarrow> Says A B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<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 NRO_sender: "\Says A' B \n, b, l, C, Crypt (priK A) X\ \ set evs; evs \ zg\ \<Longrightarrow> A' \<in> {A,Spy}" apply (erule rev_mp) apply (erule zg.induct, simp_all) done
text\<open>Holds also for \<^term>\<open>A = Spy\<close>!\<close> theorem NRO_validity: "\Gets B \Number f_nro, Agent B, Nonce L, C, NRO\ \ set evs;
NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, C\<rbrace>;
A \<notin> broken; evs \<in> zg\<rbrakk> \<Longrightarrow> Says A B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<in> set evs" apply (drule Gets_imp_Says, assumption) apply clarify apply (frule NRO_sender, auto) txt\<open>We are left with the case where the sender is \<^term>\<open>Spy\<close> and not
equal to\<^term>\<open>A\<close>, because \<^term>\<open>A \<notin> bad\<close>. Thustheorem\<open>NRO_validity_good\<close> applies.\<close> apply (blast dest: NRO_validity_good [OF refl]) done
subsection\<open>About NRR: Validity for \<^term>\<open>A\<close>\<close>
text\<open>Below we prove that if \<^term>\<open>NRR\<close> exists then \<^term>\<open>B\<close> definitely
sent it, provided \<^term>\<open>B\<close> is not broken.\<close>
text\<open>Strong conclusion for a good agent\<close> lemma NRR_validity_good: "\NRR = Crypt (priK B) \Number f_nrr, Agent A, Nonce L, C\;
NRR \<in> parts (spies evs);
B \<notin> bad; evs \<in> zg\<rbrakk> \<Longrightarrow> Says B A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<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_sender: "\Says B' A \n, a, l, Crypt (priK B) X\ \ set evs; evs \ zg\ \<Longrightarrow> B' \<in> {B,Spy}" apply (erule rev_mp) apply (erule zg.induct, simp_all) done
text\<open>Holds also for \<^term>\<open>B = Spy\<close>!\<close> theorem NRR_validity: "\Says B' A \Number f_nrr, Agent A, Nonce L, NRR\ \ set evs;
NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, C\<rbrace>;
B \<notin> broken; evs \<in> zg\<rbrakk> \<Longrightarrow> Says B A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set evs" apply clarify apply (frule NRR_sender, auto) txt\<open>We are left with the case where \<^term>\<open>B' = Spy\<close> and \<^term>\<open>B' \<noteq> B\<close>,
i.e. \<^term>\<open>B \<notin> bad\<close>, when we can apply \<open>NRR_validity_good\<close>.\<close> apply (blast dest: NRR_validity_good [OF refl]) done
subsection\<open>Proofs About \<^term>\<open>sub_K\<close>\<close>
text\<open>Below we prove that if \<^term>\<open>sub_K\<close> exists then \<^term>\<open>A\<close> definitely
sent it, provided \<^term>\<open>A\<close> is not broken.\<close>
text\<open>Strong conclusion for a good agent\<close> lemma sub_K_validity_good: "\sub_K = Crypt (priK A) \Number f_sub, Agent B, Nonce L, Key K\;
sub_K \<in> parts (spies evs);
A \<notin> bad; evs \<in> zg\<rbrakk> \<Longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<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\<open>Fake\<close> apply (blast dest!: Fake_parts_sing_imp_Un) done
lemma sub_K_sender: "\Says A' TTP \n, b, l, k, Crypt (priK A) X\ \ set evs; evs \ zg\ \<Longrightarrow> A' \<in> {A,Spy}" apply (erule rev_mp) apply (erule zg.induct, simp_all) done
text\<open>Holds also for \<^term>\<open>A = Spy\<close>!\<close> theorem sub_K_validity: "\Gets TTP \Number f_sub, Agent B, Nonce L, Key K, sub_K\ \ set evs;
sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
A \<notin> broken; evs \<in> zg\<rbrakk> \<Longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs" apply (drule Gets_imp_Says, assumption) apply clarify apply (frule sub_K_sender, auto) txt\<open>We are left with the case where the sender is \<^term>\<open>Spy\<close> and not
equal to\<^term>\<open>A\<close>, because \<^term>\<open>A \<notin> bad\<close>. Thustheorem\<open>sub_K_validity_good\<close> applies.\<close> apply (blast dest: sub_K_validity_good [OF refl]) done
subsection\<open>Proofs About \<^term>\<open>con_K\<close>\<close>
text\<open>Below we prove that if \<^term>\<open>con_K\<close> exists, then \<^term>\<open>TTP\<close> has it, and therefore \<^term>\<open>A\<close> and \<^term>\<open>B\<close>) can get it too. Moreover, we know
that \<^term>\<open>A\<close> sent \<^term>\<open>sub_K\<close>\<close>
text\<open>If \<^term>\<open>TTP\<close> holds \<^term>\<open>con_K\<close> then \<^term>\<open>A\<close> sent \<^term>\<open>sub_K\<close>. We assume that \<^term>\<open>A\<close> is not broken. Importantly, nothing
needs to be assumed about the form of \<^term>\<open>con_K\<close>!\<close> 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) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
A \<notin> broken; evs \<in> zg\<rbrakk> \<Longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<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\<open>ZG4\<close> apply clarify apply (rule sub_K_validity, auto) done
text\<open>If \<^term>\<open>con_K\<close> exists, then \<^term>\<open>A\<close> sent \<^term>\<open>sub_K\<close>. We again assume that \<^term>\<open>A\<close> is not broken.\<close> theorem B_sub_K_validity: "\con_K \ used evs;
con_K = Crypt (priK TTP) \<lbrace>Number f_con, Agent A, Agent B,
Nonce L, Key K\<rbrace>;
sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
A \<notin> broken; evs \<in> zg\<rbrakk> \<Longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs" by (blast dest: con_K_validity Notes_TTP_imp_Says_A)
subsection\<open>Proving fairness\<close>
text\<open>Cannot prove that, if \<^term>\<open>B\<close> has NRO, then \<^term>\<open>A\<close> has her NRR.
It would appear that \<^term>\<open>B\<close> has a small advantage, though it is
useless to win disputes: \<^term>\<open>B\<close> needs to present \<^term>\<open>con_K\<close> as well.\<close>
text\<open>Strange: unicity of the label protects \<^term>\<open>A\<close>?\<close> 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 \<lbrace>Number f_nro, Agent B, Nonce L, Crypt K M', NRO'\<rbrace> \<in> set evs;
A \<notin> bad; evs \<in> zg\<rbrakk> \<Longrightarrow> 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\<open>ZG1: freshness\<close> apply (blast dest: parts.Body) done
text\<open>Fairness lemma: if \<^term>\<open>sub_K\<close> exists, then \<^term>\<open>A\<close> holds
NRR. Relies on unicity of labels.\<close> lemma sub_K_implies_NRR: "\NRO = Crypt (priK A) \Number f_nro, Agent B, Nonce L, Crypt K M\;
NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, Crypt K M\<rbrace>;
sub_K \<in> parts (spies evs);
NRO \<in> parts (spies evs);
sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
A \<notin> bad; evs \<in> zg\<rbrakk> \<Longrightarrow> Gets A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set evs" apply clarify apply hypsubst_thin apply (erule rev_mp) apply (erule rev_mp) apply (erule zg.induct) apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all) txt\<open>Fake\<close> apply blast txt\<open>ZG1: freshness\<close> apply (blast dest: parts.Body) txt\<open>ZG3\<close> apply (blast dest: A_unicity [OF refl]) done
lemma Crypt_used_imp_L_used: "\Crypt (priK TTP) \F, A, B, L, K\ \ used evs; evs \ zg\ \<Longrightarrow> L \<in> used evs" apply (erule rev_mp) apply (erule zg.induct, auto) txt\<open>Fake\<close> apply (blast dest!: Fake_parts_sing_imp_Un) txt\<open>ZG2: freshness\<close> apply (blast dest: parts.Body) done
text\<open>Fairness for \<^term>\<open>A\<close>: if \<^term>\<open>con_K\<close> and \<^term>\<open>NRO\<close> exist, then\<^term>\<open>A\<close> holds NRR. \<^term>\<open>A\<close> must be uncompromised, but there is no
assumption about \<^term>\<open>B\<close>.\<close> theorem A_fairness_NRO: "\con_K \ used evs;
NRO \<in> parts (spies evs);
con_K = Crypt (priK TTP) \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K\<rbrace>;
NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, Crypt K M\<rbrace>;
NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, Crypt K M\<rbrace>;
A \<notin> bad; evs \<in> zg\<rbrakk> \<Longrightarrow> Gets A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<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\<open>Fake\<close> apply (simp add: parts_insert_knows_A) apply (blast dest: Fake_parts_sing_imp_Un) txt\<open>ZG1\<close> apply (blast dest: Crypt_used_imp_L_used) txt\<open>ZG2\<close> apply (blast dest: parts_cut) txt\<open>ZG4\<close> apply (blast intro: sub_K_implies_NRR [OF refl]
dest: Gets_imp_knows_Spy [THEN parts.Inj]) done
text\<open>Fairness for \<^term>\<open>B\<close>: NRR exists at all, then \<^term>\<open>B\<close> holds NRO. \<^term>\<open>B\<close> must be uncompromised, but there is no assumption about \<^term>\<open>A\<close>.\<close> theorem B_fairness_NRR: "\NRR \ used evs;
NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, C\<rbrace>;
NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, C\<rbrace>;
B \<notin> bad; evs \<in> zg\<rbrakk> \<Longrightarrow> Gets B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<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\<open>Fake\<close> apply (blast dest!: Fake_parts_sing_imp_Un) txt\<open>ZG2\<close> apply (blast dest: parts_cut) done
text\<open>If \<^term>\<open>con_K\<close> exists at all, then \<^term>\<open>B\<close> can get it, by \<open>con_K_validity\<close>. Cannot conclude that also NRO is available to \<^term>\<open>B\<close>,
because if\<^term>\<open>A\<close> were unfair, \<^term>\<open>A\<close> could build message 3 without
building message 1, which contains NRO.\<close>
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
