--- a/src/HOL/Auth/ZhouGollmann.thy Thu Oct 13 14:49:15 2022 +0200
+++ b/src/HOL/Auth/ZhouGollmann.thy Thu Oct 13 15:38:32 2022 +0100
@@ -32,35 +32,35 @@
Nil: "[] \<in> zg"
-| Fake: "[| evsf \<in> zg; X \<in> synth (analz (spies evsf)) |]
- ==> Says Spy B X # evsf \<in> zg"
+| Fake: "\<lbrakk>evsf \<in> zg; X \<in> synth (analz (spies evsf))\<rbrakk>
+ \<Longrightarrow> Says Spy B X # evsf \<in> zg"
-| Reception: "[| evsr \<in> zg; Says A B X \<in> set evsr |] ==> Gets B X # evsr \<in> zg"
+| Reception: "\<lbrakk>evsr \<in> zg; Says A B X \<in> set evsr\<rbrakk> \<Longrightarrow> 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);
+| ZG1: "\<lbrakk>evs1 \<in> zg; Nonce L \<notin> used evs1; C = Crypt K (Number m);
K \<in> symKeys;
- NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, C\<rbrace>|]
- ==> Says A B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> # evs1 \<in> zg"
+ 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 \<in> zg;
+| ZG2: "\<lbrakk>evs2 \<in> 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>|]
- ==> Says B A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> # evs2 \<in> zg"
+ 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 \<in> zg; C = Crypt K M; K \<in> symKeys;
+| ZG3: "\<lbrakk>evs3 \<in> zg; C = Crypt K M; K \<in> 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>|]
- ==> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<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
@@ -69,13 +69,13 @@
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 \<in> zg; K \<in> symKeys;
+| ZG4: "\<lbrakk>evs4 \<in> zg; K \<in> 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>|]
- ==> Says TTP Spy con_K
+ 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"
@@ -90,7 +90,7 @@
text\<open>A "possibility property": there are traces that reach the end\<close>
-lemma "[|A \<noteq> B; TTP \<noteq> A; TTP \<noteq> B; K \<in> symKeys|] ==>
+lemma "\<lbrakk>A \<noteq> B; TTP \<noteq> A; TTP \<noteq> B; K \<in> symKeys\<rbrakk> \<Longrightarrow>
\<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>
@@ -107,45 +107,45 @@
subsection \<open>Basic Lemmas\<close>
lemma Gets_imp_Says:
- "[| Gets B X \<in> set evs; evs \<in> zg |] ==> \<exists>A. Says A B X \<in> set evs"
+ "\<lbrakk>Gets B X \<in> set evs; evs \<in> zg\<rbrakk> \<Longrightarrow> \<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"
+ "\<lbrakk>Gets B X \<in> set evs; evs \<in> zg\<rbrakk> \<Longrightarrow> X \<in> 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 \<in> used evs; evs \<in> zg |]
- ==> Crypt K X \<in> parts (spies evs)"
+ "\<lbrakk>Crypt K X \<in> used evs; evs \<in> zg\<rbrakk>
+ \<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
lemma Notes_TTP_imp_Gets:
- "[|Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace>
+ "\<lbrakk>Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace>
\<in> set evs;
sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
- evs \<in> zg|]
- ==> Gets TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs"
+ evs \<in> zg\<rbrakk>
+ \<Longrightarrow> Gets TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs"
apply (erule rev_mp)
apply (erule zg.induct, auto)
done
text\<open>For reasoning about C, which is encrypted in message ZG2\<close>
lemma ZG2_msg_in_parts_spies:
- "[|Gets B \<lbrace>F, B', L, C, X\<rbrace> \<in> set evs; evs \<in> zg|]
- ==> C \<in> parts (spies evs)"
+ "\<lbrakk>Gets B \<lbrace>F, B', L, C, X\<rbrace> \<in> set evs; evs \<in> zg\<rbrakk>
+ \<Longrightarrow> 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)"
+ "evs \<in> zg \<Longrightarrow> (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
@@ -154,7 +154,7 @@
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)"
+ "evs \<in> zg \<Longrightarrow> (Key (priK A) \<in> analz (spies evs)) = (A \<in> bad)"
by auto
@@ -165,10 +165,10 @@
text\<open>Strong conclusion for a good agent\<close>
lemma NRO_validity_good:
- "[|NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, C\<rbrace>;
+ "\<lbrakk>NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, C\<rbrace>;
NRO \<in> parts (spies evs);
- A \<notin> bad; evs \<in> zg |]
- ==> Says A B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<in> set 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)
@@ -176,18 +176,18 @@
done
lemma NRO_sender:
- "[|Says A' B \<lbrace>n, b, l, C, Crypt (priK A) X\<rbrace> \<in> set evs; evs \<in> zg|]
- ==> A' \<in> {A,Spy}"
+ "\<lbrakk>Says A' B \<lbrace>n, b, l, C, Crypt (priK A) X\<rbrace> \<in> set evs; evs \<in> zg\<rbrakk>
+ \<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 \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<in> set evs;
+ "\<lbrakk>Gets B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<in> set evs;
NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, C\<rbrace>;
- A \<notin> broken; evs \<in> zg |]
- ==> Says A B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<in> set evs"
+ 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)
@@ -205,10 +205,10 @@
text\<open>Strong conclusion for a good agent\<close>
lemma NRR_validity_good:
- "[|NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, C\<rbrace>;
+ "\<lbrakk>NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, C\<rbrace>;
NRR \<in> parts (spies evs);
- B \<notin> bad; evs \<in> zg |]
- ==> Says B A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set 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)
@@ -216,18 +216,18 @@
done
lemma NRR_sender:
- "[|Says B' A \<lbrace>n, a, l, Crypt (priK B) X\<rbrace> \<in> set evs; evs \<in> zg|]
- ==> B' \<in> {B,Spy}"
+ "\<lbrakk>Says B' A \<lbrace>n, a, l, Crypt (priK B) X\<rbrace> \<in> set evs; evs \<in> zg\<rbrakk>
+ \<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 \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set evs;
+ "\<lbrakk>Says B' A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set evs;
NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, C\<rbrace>;
- B \<notin> broken; evs \<in> zg|]
- ==> Says B A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set evs"
+ 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>,
@@ -243,10 +243,10 @@
text\<open>Strong conclusion for a good agent\<close>
lemma sub_K_validity_good:
- "[|sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
+ "\<lbrakk>sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
sub_K \<in> parts (spies evs);
- A \<notin> bad; evs \<in> zg |]
- ==> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set 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)
@@ -256,18 +256,18 @@
done
lemma sub_K_sender:
- "[|Says A' TTP \<lbrace>n, b, l, k, Crypt (priK A) X\<rbrace> \<in> set evs; evs \<in> zg|]
- ==> A' \<in> {A,Spy}"
+ "\<lbrakk>Says A' TTP \<lbrace>n, b, l, k, Crypt (priK A) X\<rbrace> \<in> set evs; evs \<in> zg\<rbrakk>
+ \<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 \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs;
+ "\<lbrakk>Gets TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<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 |]
- ==> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs"
+ 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)
@@ -286,11 +286,11 @@
that \<^term>\<open>A\<close> sent \<^term>\<open>sub_K\<close>\<close>
lemma con_K_validity:
- "[|con_K \<in> used evs;
+ "\<lbrakk>con_K \<in> used evs;
con_K = Crypt (priK TTP)
\<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K\<rbrace>;
- evs \<in> zg |]
- ==> Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace>
+ evs \<in> zg\<rbrakk>
+ \<Longrightarrow> Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace>
\<in> set evs"
apply clarify
apply (erule rev_mp)
@@ -306,11 +306,11 @@
\<^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 \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace>
+ "\<lbrakk>Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace>
\<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|]
- ==> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs"
+ 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)
@@ -323,12 +323,12 @@
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 \<in> used evs;
+ "\<lbrakk>con_K \<in> 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|]
- ==> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs"
+ 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)
@@ -340,12 +340,12 @@
text\<open>Strange: unicity of the label protects \<^term>\<open>A\<close>?\<close>
lemma A_unicity:
- "[|NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, Crypt K M\<rbrace>;
+ "\<lbrakk>NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, Crypt K M\<rbrace>;
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 |]
- ==> M'=M"
+ A \<notin> bad; evs \<in> zg\<rbrakk>
+ \<Longrightarrow> M'=M"
apply clarify
apply (erule rev_mp)
apply (erule rev_mp)
@@ -359,13 +359,13 @@
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) \<lbrace>Number f_nro, Agent B, Nonce L, Crypt K M\<rbrace>;
+ "\<lbrakk>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>;
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 |]
- ==> Gets A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set evs"
+ 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)
@@ -382,8 +382,8 @@
lemma Crypt_used_imp_L_used:
- "[| Crypt (priK TTP) \<lbrace>F, A, B, L, K\<rbrace> \<in> used evs; evs \<in> zg |]
- ==> L \<in> used evs"
+ "\<lbrakk>Crypt (priK TTP) \<lbrace>F, A, B, L, K\<rbrace> \<in> used evs; evs \<in> zg\<rbrakk>
+ \<Longrightarrow> L \<in> used evs"
apply (erule rev_mp)
apply (erule zg.induct, auto)
txt\<open>Fake\<close>
@@ -397,14 +397,14 @@
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 \<in> used evs;
+ "\<lbrakk>con_K \<in> 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 |]
- ==> Gets A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set evs"
+ 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)
@@ -425,11 +425,11 @@
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 \<in> used evs;
+ "\<lbrakk>NRR \<in> 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 |]
- ==> Gets B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<in> set evs"
+ 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)