--- a/src/HOL/Auth/OtwayRees.thy Fri Sep 30 15:51:43 2016 +0200
+++ b/src/HOL/Auth/OtwayRees.thy Fri Sep 30 17:12:50 2016 +0100
@@ -21,62 +21,62 @@
(*The spy MAY say anything he CAN say. We do not expect him to
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
- | Fake: "[| evsf \<in> otway; X \<in> synth (analz (knows Spy evsf)) |]
- ==> Says Spy B X # evsf \<in> otway"
+ | Fake: "\<lbrakk>evsf \<in> otway; X \<in> synth (analz (knows Spy evsf)) \<rbrakk>
+ \<Longrightarrow> Says Spy B X # evsf \<in> otway"
(*A message that has been sent can be received by the
intended recipient.*)
- | Reception: "[| evsr \<in> otway; Says A B X \<in>set evsr |]
- ==> Gets B X # evsr \<in> otway"
+ | Reception: "\<lbrakk>evsr \<in> otway; Says A B X \<in>set evsr\<rbrakk>
+ \<Longrightarrow> Gets B X # evsr \<in> otway"
(*Alice initiates a protocol run*)
- | OR1: "[| evs1 \<in> otway; Nonce NA \<notin> used evs1 |]
- ==> Says A B \<lbrace>Nonce NA, Agent A, Agent B,
+ | OR1: "\<lbrakk>evs1 \<in> otway; Nonce NA \<notin> used evs1\<rbrakk>
+ \<Longrightarrow> Says A B \<lbrace>Nonce NA, Agent A, Agent B,
Crypt (shrK A) \<lbrace>Nonce NA, Agent A, Agent B\<rbrace> \<rbrace>
- # evs1 : otway"
+ # evs1 \<in> otway"
(*Bob's response to Alice's message. Note that NB is encrypted.*)
- | OR2: "[| evs2 \<in> otway; Nonce NB \<notin> used evs2;
- Gets B \<lbrace>Nonce NA, Agent A, Agent B, X\<rbrace> : set evs2 |]
- ==> Says B Server
+ | OR2: "\<lbrakk>evs2 \<in> otway; Nonce NB \<notin> used evs2;
+ Gets B \<lbrace>Nonce NA, Agent A, Agent B, X\<rbrace> : set evs2\<rbrakk>
+ \<Longrightarrow> Says B Server
\<lbrace>Nonce NA, Agent A, Agent B, X,
Crypt (shrK B)
\<lbrace>Nonce NA, Nonce NB, Agent A, Agent B\<rbrace>\<rbrace>
- # evs2 : otway"
+ # evs2 \<in> otway"
(*The Server receives Bob's message and checks that the three NAs
match. Then he sends a new session key to Bob with a packet for
forwarding to Alice.*)
- | OR3: "[| evs3 \<in> otway; Key KAB \<notin> used evs3;
+ | OR3: "\<lbrakk>evs3 \<in> otway; Key KAB \<notin> used evs3;
Gets Server
\<lbrace>Nonce NA, Agent A, Agent B,
Crypt (shrK A) \<lbrace>Nonce NA, Agent A, Agent B\<rbrace>,
Crypt (shrK B) \<lbrace>Nonce NA, Nonce NB, Agent A, Agent B\<rbrace>\<rbrace>
- : set evs3 |]
- ==> Says Server B
+ : set evs3\<rbrakk>
+ \<Longrightarrow> Says Server B
\<lbrace>Nonce NA,
Crypt (shrK A) \<lbrace>Nonce NA, Key KAB\<rbrace>,
Crypt (shrK B) \<lbrace>Nonce NB, Key KAB\<rbrace>\<rbrace>
- # evs3 : otway"
+ # evs3 \<in> otway"
(*Bob receives the Server's (?) message and compares the Nonces with
those in the message he previously sent the Server.
Need B \<noteq> Server because we allow messages to self.*)
- | OR4: "[| evs4 \<in> otway; B \<noteq> Server;
+ | OR4: "\<lbrakk>evs4 \<in> otway; B \<noteq> Server;
Says B Server \<lbrace>Nonce NA, Agent A, Agent B, X',
Crypt (shrK B)
\<lbrace>Nonce NA, Nonce NB, Agent A, Agent B\<rbrace>\<rbrace>
: set evs4;
Gets B \<lbrace>Nonce NA, X, Crypt (shrK B) \<lbrace>Nonce NB, Key K\<rbrace>\<rbrace>
- : set evs4 |]
- ==> Says B A \<lbrace>Nonce NA, X\<rbrace> # evs4 : otway"
+ : set evs4\<rbrakk>
+ \<Longrightarrow> Says B A \<lbrace>Nonce NA, X\<rbrace> # evs4 \<in> otway"
(*This message models possible leaks of session keys. The nonces
identify the protocol run.*)
- | Oops: "[| evso \<in> otway;
+ | Oops: "\<lbrakk>evso \<in> otway;
Says Server B \<lbrace>Nonce NA, X, Crypt (shrK B) \<lbrace>Nonce NB, Key K\<rbrace>\<rbrace>
- : set evso |]
- ==> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso : otway"
+ : set evso\<rbrakk>
+ \<Longrightarrow> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> otway"
declare Says_imp_analz_Spy [dest]
@@ -86,8 +86,8 @@
text\<open>A "possibility property": there are traces that reach the end\<close>
-lemma "[| B \<noteq> Server; Key K \<notin> used [] |]
- ==> \<exists>evs \<in> otway.
+lemma "\<lbrakk>B \<noteq> Server; Key K \<notin> used []\<rbrakk>
+ \<Longrightarrow> \<exists>evs \<in> otway.
Says B A \<lbrace>Nonce NA, Crypt (shrK A) \<lbrace>Nonce NA, Key K\<rbrace>\<rbrace>
\<in> set evs"
apply (intro exI bexI)
@@ -99,7 +99,7 @@
done
lemma Gets_imp_Says [dest!]:
- "[| Gets B X \<in> set evs; evs \<in> otway |] ==> \<exists>A. Says A B X \<in> set evs"
+ "\<lbrakk>Gets B X \<in> set evs; evs \<in> otway\<rbrakk> \<Longrightarrow> \<exists>A. Says A B X \<in> set evs"
apply (erule rev_mp)
apply (erule otway.induct, auto)
done
@@ -108,13 +108,13 @@
(** For reasoning about the encrypted portion of messages **)
lemma OR2_analz_knows_Spy:
- "[| Gets B \<lbrace>N, Agent A, Agent B, X\<rbrace> \<in> set evs; evs \<in> otway |]
- ==> X \<in> analz (knows Spy evs)"
+ "\<lbrakk>Gets B \<lbrace>N, Agent A, Agent B, X\<rbrace> \<in> set evs; evs \<in> otway\<rbrakk>
+ \<Longrightarrow> X \<in> analz (knows Spy evs)"
by blast
lemma OR4_analz_knows_Spy:
- "[| Gets B \<lbrace>N, X, Crypt (shrK B) X'\<rbrace> \<in> set evs; evs \<in> otway |]
- ==> X \<in> analz (knows Spy evs)"
+ "\<lbrakk>Gets B \<lbrace>N, X, Crypt (shrK B) X'\<rbrace> \<in> set evs; evs \<in> otway\<rbrakk>
+ \<Longrightarrow> X \<in> analz (knows Spy evs)"
by blast
(*These lemmas assist simplification by removing forwarded X-variables.
@@ -132,17 +132,17 @@
text\<open>Spy never sees a good agent's shared key!\<close>
lemma Spy_see_shrK [simp]:
- "evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
+ "evs \<in> otway \<Longrightarrow> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
by (erule otway.induct, force,
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
lemma Spy_analz_shrK [simp]:
- "evs \<in> otway ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
+ "evs \<in> otway \<Longrightarrow> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
by auto
lemma Spy_see_shrK_D [dest!]:
- "[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> otway|] ==> A \<in> bad"
+ "\<lbrakk>Key (shrK A) \<in> parts (knows Spy evs); evs \<in> otway\<rbrakk> \<Longrightarrow> A \<in> bad"
by (blast dest: Spy_see_shrK)
@@ -151,16 +151,16 @@
(*Describes the form of K and NA when the Server sends this message. Also
for Oops case.*)
lemma Says_Server_message_form:
- "[| Says Server B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs;
- evs \<in> otway |]
- ==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
+ "\<lbrakk>Says Server B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs;
+ evs \<in> otway\<rbrakk>
+ \<Longrightarrow> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
by (erule rev_mp, erule otway.induct, simp_all)
(****
The following is to prove theorems of the form
- Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==>
+ Key K \<in> analz (insert (Key KAB) (knows Spy evs)) \<Longrightarrow>
Key K \<in> analz (knows Spy evs)
A more general formula must be proved inductively.
@@ -171,7 +171,7 @@
text\<open>The equality makes the induction hypothesis easier to apply\<close>
lemma analz_image_freshK [rule_format]:
- "evs \<in> otway ==>
+ "evs \<in> otway \<Longrightarrow>
\<forall>K KK. KK <= -(range shrK) -->
(Key K \<in> analz (Key`KK Un (knows Spy evs))) =
(K \<in> KK | Key K \<in> analz (knows Spy evs))"
@@ -182,7 +182,7 @@
done
lemma analz_insert_freshK:
- "[| evs \<in> otway; KAB \<notin> range shrK |] ==>
+ "\<lbrakk>evs \<in> otway; KAB \<notin> range shrK\<rbrakk> \<Longrightarrow>
(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)
@@ -190,9 +190,9 @@
text\<open>The Key K uniquely identifies the Server's message.\<close>
lemma unique_session_keys:
- "[| Says Server B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, K\<rbrace>\<rbrace> \<in> set evs;
+ "\<lbrakk>Says Server B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, K\<rbrace>\<rbrace> \<in> set evs;
Says Server B' \<lbrace>NA',X',Crypt (shrK B') \<lbrace>NB',K\<rbrace>\<rbrace> \<in> set evs;
- evs \<in> otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'"
+ evs \<in> otway\<rbrakk> \<Longrightarrow> X=X' & B=B' & NA=NA' & NB=NB'"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule otway.induct, simp_all)
@@ -204,8 +204,8 @@
text\<open>Only OR1 can have caused such a part of a message to appear.\<close>
lemma Crypt_imp_OR1 [rule_format]:
- "[| A \<notin> bad; evs \<in> otway |]
- ==> Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs) -->
+ "\<lbrakk>A \<notin> bad; evs \<in> otway\<rbrakk>
+ \<Longrightarrow> Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs) -->
Says A B \<lbrace>NA, Agent A, Agent B,
Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace>
\<in> set evs"
@@ -213,10 +213,10 @@
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
lemma Crypt_imp_OR1_Gets:
- "[| Gets B \<lbrace>NA, Agent A, Agent B,
+ "\<lbrakk>Gets B \<lbrace>NA, Agent A, Agent B,
Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs;
- A \<notin> bad; evs \<in> otway |]
- ==> Says A B \<lbrace>NA, Agent A, Agent B,
+ A \<notin> bad; evs \<in> otway\<rbrakk>
+ \<Longrightarrow> Says A B \<lbrace>NA, Agent A, Agent B,
Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace>
\<in> set evs"
by (blast dest: Crypt_imp_OR1)
@@ -224,10 +224,10 @@
text\<open>The Nonce NA uniquely identifies A's message\<close>
lemma unique_NA:
- "[| Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs);
+ "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs);
Crypt (shrK A) \<lbrace>NA, Agent A, Agent C\<rbrace> \<in> parts (knows Spy evs);
- evs \<in> otway; A \<notin> bad |]
- ==> B = C"
+ evs \<in> otway; A \<notin> bad\<rbrakk>
+ \<Longrightarrow> B = C"
apply (erule rev_mp, erule rev_mp)
apply (erule otway.induct, force,
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
@@ -238,9 +238,9 @@
OR2 encrypts Nonce NB. It prevents the attack that can occur in the
over-simplified version of this protocol: see \<open>OtwayRees_Bad\<close>.\<close>
lemma no_nonce_OR1_OR2:
- "[| Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs);
- A \<notin> bad; evs \<in> otway |]
- ==> Crypt (shrK A) \<lbrace>NA', NA, Agent A', Agent A\<rbrace> \<notin> parts (knows Spy evs)"
+ "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs);
+ A \<notin> bad; evs \<in> otway\<rbrakk>
+ \<Longrightarrow> Crypt (shrK A) \<lbrace>NA', NA, Agent A', Agent A\<rbrace> \<notin> parts (knows Spy evs)"
apply (erule rev_mp)
apply (erule otway.induct, force,
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
@@ -249,8 +249,8 @@
text\<open>Crucial property: If the encrypted message appears, and A has used NA
to start a run, then it originated with the Server!\<close>
lemma NA_Crypt_imp_Server_msg [rule_format]:
- "[| A \<notin> bad; evs \<in> otway |]
- ==> Says A B \<lbrace>NA, Agent A, Agent B,
+ "\<lbrakk>A \<notin> bad; evs \<in> otway\<rbrakk>
+ \<Longrightarrow> Says A B \<lbrace>NA, Agent A, Agent B,
Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs -->
Crypt (shrK A) \<lbrace>NA, Key K\<rbrace> \<in> parts (knows Spy evs)
--> (\<exists>NB. Says Server B
@@ -259,9 +259,12 @@
Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs)"
apply (erule otway.induct, force,
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast)
-apply blast \<comment>\<open>OR1: by freshness\<close>
-apply (blast dest!: no_nonce_OR1_OR2 intro: unique_NA) \<comment>\<open>OR3\<close>
-apply (blast intro!: Crypt_imp_OR1) \<comment>\<open>OR4\<close>
+ subgoal \<comment>\<open>OR1: by freshness\<close>
+ by blast
+ subgoal \<comment>\<open>OR3\<close>
+ by (blast dest!: no_nonce_OR1_OR2 intro: unique_NA)
+ subgoal \<comment>\<open>OR4\<close>
+ by (blast intro!: Crypt_imp_OR1)
done
@@ -270,11 +273,11 @@
bad form of this protocol, even though we can prove
\<open>Spy_not_see_encrypted_key\<close>\<close>
lemma A_trusts_OR4:
- "[| Says A B \<lbrace>NA, Agent A, Agent B,
+ "\<lbrakk>Says A B \<lbrace>NA, Agent A, Agent B,
Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs;
Says B' A \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>\<rbrace> \<in> set evs;
- A \<notin> bad; evs \<in> otway |]
- ==> \<exists>NB. Says Server B
+ A \<notin> bad; evs \<in> otway\<rbrakk>
+ \<Longrightarrow> \<exists>NB. Says Server B
\<lbrace>NA,
Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace>
@@ -286,28 +289,32 @@
Does not in itself guarantee security: an attack could violate
the premises, e.g. by having @{term "A=Spy"}\<close>
lemma secrecy_lemma:
- "[| A \<notin> bad; B \<notin> bad; evs \<in> otway |]
- ==> Says Server B
+ "\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> otway\<rbrakk>
+ \<Longrightarrow> Says Server B
\<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs -->
Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs -->
Key K \<notin> analz (knows Spy evs)"
-apply (erule otway.induct, force)
-apply (frule_tac [7] Says_Server_message_form)
-apply (drule_tac [6] OR4_analz_knows_Spy)
-apply (drule_tac [4] OR2_analz_knows_Spy)
-apply (simp_all add: analz_insert_eq analz_insert_freshK pushes)
-apply spy_analz \<comment>\<open>Fake\<close>
-apply (blast dest: unique_session_keys)+ \<comment>\<open>OR3, OR4, Oops\<close>
-done
+ apply (erule otway.induct, force, simp_all)
+ subgoal \<comment>\<open>Fake\<close>
+ by spy_analz
+ subgoal \<comment>\<open>OR2\<close>
+ by (drule OR2_analz_knows_Spy) (auto simp: analz_insert_eq)
+ subgoal \<comment>\<open>OR3\<close>
+ by (auto simp add: analz_insert_freshK pushes)
+ subgoal \<comment>\<open>OR4\<close>
+ by (drule OR4_analz_knows_Spy) (auto simp: analz_insert_eq)
+ subgoal \<comment>\<open>Oops\<close>
+ by (auto simp add: Says_Server_message_form analz_insert_freshK unique_session_keys)
+ done
theorem Spy_not_see_encrypted_key:
- "[| Says Server B
+ "\<lbrakk>Says Server B
\<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs;
Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
- A \<notin> bad; B \<notin> bad; evs \<in> otway |]
- ==> Key K \<notin> analz (knows Spy evs)"
+ A \<notin> bad; B \<notin> bad; evs \<in> otway\<rbrakk>
+ \<Longrightarrow> Key K \<notin> analz (knows Spy evs)"
by (blast dest: Says_Server_message_form secrecy_lemma)
text\<open>This form is an immediate consequence of the previous result. It is
@@ -318,24 +325,24 @@
other than Fake are trivial, while Fake requires
@{term "Key K \<notin> analz (knows Spy evs)"}.\<close>
lemma Spy_not_know_encrypted_key:
- "[| Says Server B
+ "\<lbrakk>Says Server B
\<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs;
Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
- A \<notin> bad; B \<notin> bad; evs \<in> otway |]
- ==> Key K \<notin> knows Spy evs"
+ A \<notin> bad; B \<notin> bad; evs \<in> otway\<rbrakk>
+ \<Longrightarrow> Key K \<notin> knows Spy evs"
by (blast dest: Spy_not_see_encrypted_key)
text\<open>A's guarantee. The Oops premise quantifies over NB because A cannot know
what it is.\<close>
lemma A_gets_good_key:
- "[| Says A B \<lbrace>NA, Agent A, Agent B,
+ "\<lbrakk>Says A B \<lbrace>NA, Agent A, Agent B,
Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs;
Says B' A \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>\<rbrace> \<in> set evs;
\<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
- A \<notin> bad; B \<notin> bad; evs \<in> otway |]
- ==> Key K \<notin> analz (knows Spy evs)"
+ A \<notin> bad; B \<notin> bad; evs \<in> otway\<rbrakk>
+ \<Longrightarrow> Key K \<notin> analz (knows Spy evs)"
by (blast dest!: A_trusts_OR4 Spy_not_see_encrypted_key)
@@ -344,9 +351,9 @@
text\<open>Only OR2 can have caused such a part of a message to appear. We do not
know anything about X: it does NOT have to have the right form.\<close>
lemma Crypt_imp_OR2:
- "[| Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs);
- B \<notin> bad; evs \<in> otway |]
- ==> \<exists>X. Says B Server
+ "\<lbrakk>Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs);
+ B \<notin> bad; evs \<in> otway\<rbrakk>
+ \<Longrightarrow> \<exists>X. Says B Server
\<lbrace>NA, Agent A, Agent B, X,
Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace>
\<in> set evs"
@@ -358,10 +365,10 @@
text\<open>The Nonce NB uniquely identifies B's message\<close>
lemma unique_NB:
- "[| Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace> \<in> parts(knows Spy evs);
+ "\<lbrakk>Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace> \<in> parts(knows Spy evs);
Crypt (shrK B) \<lbrace>NC, NB, Agent C, Agent B\<rbrace> \<in> parts(knows Spy evs);
- evs \<in> otway; B \<notin> bad |]
- ==> NC = NA & C = A"
+ evs \<in> otway; B \<notin> bad\<rbrakk>
+ \<Longrightarrow> NC = NA & C = A"
apply (erule rev_mp, erule rev_mp)
apply (erule otway.induct, force,
drule_tac [4] OR2_parts_knows_Spy, simp_all)
@@ -371,8 +378,8 @@
text\<open>If the encrypted message appears, and B has used Nonce NB,
then it originated with the Server! Quite messy proof.\<close>
lemma NB_Crypt_imp_Server_msg [rule_format]:
- "[| B \<notin> bad; evs \<in> otway |]
- ==> Crypt (shrK B) \<lbrace>NB, Key K\<rbrace> \<in> parts (knows Spy evs)
+ "\<lbrakk>B \<notin> bad; evs \<in> otway\<rbrakk>
+ \<Longrightarrow> Crypt (shrK B) \<lbrace>NB, Key K\<rbrace> \<in> parts (knows Spy evs)
--> (\<forall>X'. Says B Server
\<lbrace>NA, Agent A, Agent B, X',
Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace>
@@ -382,24 +389,27 @@
Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace>
\<in> set evs)"
apply simp
-apply (erule otway.induct, force,
- drule_tac [4] OR2_parts_knows_Spy, simp_all)
-apply blast \<comment>\<open>Fake\<close>
-apply blast \<comment>\<open>OR2\<close>
-apply (blast dest: unique_NB dest!: no_nonce_OR1_OR2) \<comment>\<open>OR3\<close>
-apply (blast dest!: Crypt_imp_OR2) \<comment>\<open>OR4\<close>
+apply (erule otway.induct, force, simp_all)
+ subgoal \<comment>\<open>Fake\<close>
+ by blast
+ subgoal \<comment>\<open>OR2\<close>
+ by (force dest!: OR2_parts_knows_Spy)
+ subgoal \<comment>\<open>OR3\<close>
+ by (blast dest: unique_NB dest!: no_nonce_OR1_OR2) \<comment>\<open>OR3\<close>
+ subgoal \<comment>\<open>OR4\<close>
+ by (blast dest!: Crypt_imp_OR2)
done
text\<open>Guarantee for B: if it gets a message with matching NB then the Server
has sent the correct message.\<close>
theorem B_trusts_OR3:
- "[| Says B Server \<lbrace>NA, Agent A, Agent B, X',
+ "\<lbrakk>Says B Server \<lbrace>NA, Agent A, Agent B, X',
Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace>
\<in> set evs;
Gets B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs;
- B \<notin> bad; evs \<in> otway |]
- ==> Says Server B
+ B \<notin> bad; evs \<in> otway\<rbrakk>
+ \<Longrightarrow> Says Server B
\<lbrace>NA,
Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace>
@@ -410,22 +420,22 @@
text\<open>The obvious combination of \<open>B_trusts_OR3\<close> with
\<open>Spy_not_see_encrypted_key\<close>\<close>
lemma B_gets_good_key:
- "[| Says B Server \<lbrace>NA, Agent A, Agent B, X',
+ "\<lbrakk>Says B Server \<lbrace>NA, Agent A, Agent B, X',
Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace>
\<in> set evs;
Gets B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs;
Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
- A \<notin> bad; B \<notin> bad; evs \<in> otway |]
- ==> Key K \<notin> analz (knows Spy evs)"
+ A \<notin> bad; B \<notin> bad; evs \<in> otway\<rbrakk>
+ \<Longrightarrow> Key K \<notin> analz (knows Spy evs)"
by (blast dest!: B_trusts_OR3 Spy_not_see_encrypted_key)
lemma OR3_imp_OR2:
- "[| Says Server B
+ "\<lbrakk>Says Server B
\<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs;
- B \<notin> bad; evs \<in> otway |]
- ==> \<exists>X. Says B Server \<lbrace>NA, Agent A, Agent B, X,
+ B \<notin> bad; evs \<in> otway\<rbrakk>
+ \<Longrightarrow> \<exists>X. Says B Server \<lbrace>NA, Agent A, Agent B, X,
Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace>
\<in> set evs"
apply (erule rev_mp)
@@ -438,11 +448,11 @@
We could probably prove that X has the expected form, but that is not
strictly necessary for authentication.\<close>
theorem A_auths_B:
- "[| Says B' A \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>\<rbrace> \<in> set evs;
+ "\<lbrakk>Says B' A \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>\<rbrace> \<in> set evs;
Says A B \<lbrace>NA, Agent A, Agent B,
Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs;
- A \<notin> bad; B \<notin> bad; evs \<in> otway |]
- ==> \<exists>NB X. Says B Server \<lbrace>NA, Agent A, Agent B, X,
+ A \<notin> bad; B \<notin> bad; evs \<in> otway\<rbrakk>
+ \<Longrightarrow> \<exists>NB X. Says B Server \<lbrace>NA, Agent A, Agent B, X,
Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace>
\<in> set evs"
by (blast dest!: A_trusts_OR4 OR3_imp_OR2)