--- a/src/HOL/Auth/NS_Shared.ML Thu Jan 08 18:09:47 1998 +0100
+++ b/src/HOL/Auth/NS_Shared.ML Thu Jan 08 18:10:34 1998 +0100
@@ -258,7 +258,7 @@
\ (Crypt (shrK A) {|NA, Agent B, Key K, \
\ Crypt (shrK B) {|Key K, Agent A|}|}) \
\ : set evs --> \
-\ (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs) --> \
+\ (ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs) --> \
\ Key K ~: analz (spies evs)";
by (etac ns_shared.induct 1);
by analz_spies_tac;
@@ -288,7 +288,7 @@
goal thy
"!!evs. [| Says Server A \
\ (Crypt K' {|NA, Agent B, Key K, X|}) : set evs; \
-\ ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs; \
+\ ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs; \
\ A ~: bad; B ~: bad; evs : ns_shared \
\ |] ==> Key K ~: analz (spies evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
@@ -345,7 +345,7 @@
goal thy
"!!evs. [| Crypt K (Nonce NB) : parts (spies evs); \
\ Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
-\ ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs; \
+\ ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs; \
\ A ~: bad; B ~: bad; evs : ns_shared |] \
\ ==> Says B A (Crypt K (Nonce NB)) : set evs";
by (blast_tac (claset() addSIs [A_trusts_NS2, A_trusts_NS4_lemma]
@@ -415,7 +415,7 @@
"!!evs. [| Crypt K {|Nonce NB, Nonce NB|} : parts (spies evs); \
\ Says B A (Crypt K (Nonce NB)) : set evs; \
\ Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs); \
-\ ALL NA NB. Says A Spy {|NA, NB, Key K|} ~: set evs; \
+\ ALL NA NB. Notes Spy {|NA, NB, Key K|} ~: set evs; \
\ A ~: bad; B ~: bad; evs : ns_shared |] \
\ ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) : set evs";
by (dtac B_trusts_NS3 1);
--- a/src/HOL/Auth/NS_Shared.thy Thu Jan 08 18:09:47 1998 +0100
+++ b/src/HOL/Auth/NS_Shared.thy Thu Jan 08 18:10:34 1998 +0100
@@ -75,6 +75,6 @@
Says B A (Crypt K (Nonce NB)) : set evso;
Says Server A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
: set evso |]
- ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evso : ns_shared"
+ ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : ns_shared"
end
--- a/src/HOL/Auth/OtwayRees.ML Thu Jan 08 18:09:47 1998 +0100
+++ b/src/HOL/Auth/OtwayRees.ML Thu Jan 08 18:10:34 1998 +0100
@@ -60,15 +60,10 @@
qed "OR4_analz_spies";
goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
-\ ==> K : parts (spies evs)";
+\ ==> K : parts (spies evs)";
by (Blast_tac 1);
qed "Oops_parts_spies";
-(*OR2_analz... and OR4_analz... let us treat those cases using the same
- argument as for the Fake case. This is possible for most, but not all,
- proofs: Fake does not invent new nonces (as in OR2), and of course Fake
- messages originate from the Spy. *)
-
bind_thm ("OR2_parts_spies",
OR2_analz_spies RS (impOfSubs analz_subset_parts));
bind_thm ("OR4_parts_spies",
@@ -86,8 +81,7 @@
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
sends messages containing X! **)
-
-(*Spy never sees another agent's shared key! (unless it's bad at start)*)
+(*Spy never sees a good agent's shared key!*)
goal thy
"!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
by (parts_induct_tac 1);
@@ -111,6 +105,7 @@
by (parts_induct_tac 1);
(*Fake*)
by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
+(*OR2, OR3*)
by (ALLGOALS Blast_tac);
qed_spec_mp "new_keys_not_used";
@@ -141,8 +136,7 @@
val analz_spies_tac =
dtac OR2_analz_spies 4 THEN
dtac OR4_analz_spies 6 THEN
- forward_tac [Says_Server_message_form] 7 THEN
- assume_tac 7 THEN
+ forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN
REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
@@ -194,7 +188,7 @@
by (ALLGOALS Clarify_tac);
(*Remaining cases: OR3 and OR4*)
by (ex_strip_tac 2);
-by (Best_tac 2);
+by (Best_tac 2); (*Blast_tac's too slow (in reconstruction)*)
by (expand_case_tac "K = ?y" 1);
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
(*...we assume X is a recent message, and handle this case by contradiction*)
@@ -315,11 +309,11 @@
the premises, e.g. by having A=Spy **)
goal thy
- "!!evs. [| A ~: bad; B ~: bad; evs : otway |] \
+ "!!evs. [| A ~: bad; B ~: bad; evs : otway |] \
\ ==> Says Server B \
\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
\ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \
-\ Says B Spy {|NA, NB, Key K|} ~: set evs --> \
+\ Notes Spy {|NA, NB, Key K|} ~: set evs --> \
\ Key K ~: analz (spies evs)";
by (etac otway.induct 1);
by analz_spies_tac;
@@ -341,8 +335,8 @@
"!!evs. [| Says Server B \
\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
\ Crypt (shrK B) {|NB, Key K|}|} : set evs; \
-\ Says B Spy {|NA, NB, Key K|} ~: set evs; \
-\ A ~: bad; B ~: bad; evs : otway |] \
+\ Notes Spy {|NA, NB, Key K|} ~: set evs; \
+\ A ~: bad; B ~: bad; evs : otway |] \
\ ==> Key K ~: analz (spies evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
by (blast_tac (claset() addSEs [lemma]) 1);
--- a/src/HOL/Auth/OtwayRees.thy Thu Jan 08 18:09:47 1998 +0100
+++ b/src/HOL/Auth/OtwayRees.thy Thu Jan 08 18:10:34 1998 +0100
@@ -75,6 +75,6 @@
Oops "[| evso: otway; B ~= Spy;
Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
: set evso |]
- ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
+ ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
end
--- a/src/HOL/Auth/OtwayRees_AN.ML Thu Jan 08 18:09:47 1998 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML Thu Jan 08 18:10:34 1998 +0100
@@ -58,10 +58,6 @@
by (Blast_tac 1);
qed "Oops_parts_spies";
-(*OR4_analz_spies lets us treat those cases using the same
- argument as for the Fake case. This is possible for most, but not all,
- proofs, since Fake messages originate from the Spy. *)
-
bind_thm ("OR4_parts_spies",
OR4_analz_spies RS (impOfSubs analz_subset_parts));
@@ -76,7 +72,7 @@
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
sends messages containing X! **)
-(*Spy never sees another agent's shared key! (unless it's bad at start)*)
+(*Spy never sees a good agent's shared key!*)
goal thy
"!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
by (parts_induct_tac 1);
@@ -248,12 +244,12 @@
the premises, e.g. by having A=Spy **)
goal thy
- "!!evs. [| A ~: bad; B ~: bad; evs : otway |] \
+ "!!evs. [| A ~: bad; B ~: bad; evs : otway |] \
\ ==> Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
\ : set evs --> \
-\ Says B Spy {|NA, NB, Key K|} ~: set evs --> \
+\ Notes Spy {|NA, NB, Key K|} ~: set evs --> \
\ Key K ~: analz (spies evs)";
by (etac otway.induct 1);
by analz_spies_tac;
@@ -276,8 +272,8 @@
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
\ : set evs; \
-\ Says B Spy {|NA, NB, Key K|} ~: set evs; \
-\ A ~: bad; B ~: bad; evs : otway |] \
+\ Notes Spy {|NA, NB, Key K|} ~: set evs; \
+\ A ~: bad; B ~: bad; evs : otway |] \
\ ==> Key K ~: analz (spies evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
by (blast_tac (claset() addSEs [lemma]) 1);
--- a/src/HOL/Auth/OtwayRees_AN.thy Thu Jan 08 18:09:47 1998 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.thy Thu Jan 08 18:10:34 1998 +0100
@@ -68,6 +68,6 @@
{|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|},
Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|}
: set evso |]
- ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
+ ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
end
--- a/src/HOL/Auth/OtwayRees_Bad.ML Thu Jan 08 18:09:47 1998 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Thu Jan 08 18:10:34 1998 +0100
@@ -20,6 +20,10 @@
set proof_timing;
HOL_quantifiers := false;
+AddEs spies_partsEs;
+AddDs [impOfSubs analz_subset_parts];
+AddDs [impOfSubs Fake_parts_insert];
+
(*A "possibility property": there are traces that reach the end*)
goal thy
@@ -46,26 +50,23 @@
(** For reasoning about the encrypted portion of messages **)
-goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs ==> \
-\ X : analz (spies evs)";
-by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
+goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs \
+\ ==> X : analz (spies evs)";
+by (dtac (Says_imp_spies RS analz.Inj) 1);
+by (Blast_tac 1);
qed "OR2_analz_spies";
-goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs ==> \
-\ X : analz (spies evs)";
-by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
+goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
+\ ==> X : analz (spies evs)";
+by (dtac (Says_imp_spies RS analz.Inj) 1);
+by (Blast_tac 1);
qed "OR4_analz_spies";
goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
-\ ==> K : parts (spies evs)";
-by (blast_tac (claset() addSEs spies_partsEs) 1);
+\ ==> K : parts (spies evs)";
+by (Blast_tac 1);
qed "Oops_parts_spies";
-(*OR2_analz... and OR4_analz... let us treat those cases using the same
- argument as for the Fake case. This is possible for most, but not all,
- proofs: Fake does not invent new nonces (as in OR2), and of course Fake
- messages originate from the Spy. *)
-
bind_thm ("OR2_parts_spies",
OR2_analz_spies RS (impOfSubs analz_subset_parts));
bind_thm ("OR4_parts_spies",
@@ -83,11 +84,10 @@
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
sends messages containing X! **)
-(*Spy never sees another agent's shared key! (unless it's bad at start)*)
+(*Spy never sees a good agent's shared key!*)
goal thy
"!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
by (ALLGOALS Blast_tac);
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
@@ -108,7 +108,7 @@
by (parts_induct_tac 1);
(*Fake*)
by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
-(*OR1-3*)
+(*OR2, OR3*)
by (ALLGOALS Blast_tac);
qed_spec_mp "new_keys_not_used";
@@ -125,14 +125,13 @@
(*Describes the form of K and NA when the Server sends this message. Also
for Oops case.*)
goal thy
- "!!evs. [| Says Server B \
-\ {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
-\ evs : otway |] \
+ "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
+\ evs : otway |] \
\ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
by (etac rev_mp 1);
by (etac otway.induct 1);
-by (prove_simple_subgoals_tac 1);
-by (Blast_tac 1);
+by (ALLGOALS Simp_tac);
+by (ALLGOALS Blast_tac);
qed "Says_Server_message_form";
@@ -140,7 +139,7 @@
val analz_spies_tac =
dtac OR2_analz_spies 4 THEN
dtac OR4_analz_spies 6 THEN
- forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN
+ forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN
REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
@@ -192,12 +191,11 @@
by (ALLGOALS Clarify_tac);
(*Remaining cases: OR3 and OR4*)
by (ex_strip_tac 2);
-by (Blast_tac 2);
+by (Best_tac 2); (*Blast_tac's too slow (in reconstruction)*)
by (expand_case_tac "K = ?y" 1);
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
(*...we assume X is a recent message, and handle this case by contradiction*)
-by (blast_tac (claset() addSEs spies_partsEs
- delrules [conjI] (*no split-up to 4 subgoals*)) 1);
+by (blast_tac (claset() addSEs spies_partsEs) 1);
val lemma = result();
goal thy
@@ -208,37 +206,39 @@
qed "unique_session_keys";
-(*Crucial security property, but not itself enough to guarantee correctness!*)
+(** Crucial secrecy property: Spy does not see the keys sent in msg OR3
+ Does not in itself guarantee security: an attack could violate
+ the premises, e.g. by having A=Spy **)
+
goal thy
- "!!evs. [| A ~: bad; B ~: bad; evs : otway |] \
+ "!!evs. [| A ~: bad; B ~: bad; evs : otway |] \
\ ==> Says Server B \
\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
\ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \
-\ Says B Spy {|NA, NB, Key K|} ~: set evs --> \
+\ Notes Spy {|NA, NB, Key K|} ~: set evs --> \
\ Key K ~: analz (spies evs)";
by (etac otway.induct 1);
by analz_spies_tac;
by (ALLGOALS
(asm_simp_tac (simpset() addcongs [conj_cong]
- addsimps [analz_insert_eq, analz_insert_freshK]
- addsimps (pushes@expand_ifs))));
+ addsimps [analz_insert_eq, analz_insert_freshK]
+ addsimps (pushes@expand_ifs))));
(*Oops*)
by (blast_tac (claset() addSDs [unique_session_keys]) 4);
(*OR4*)
by (Blast_tac 3);
(*OR3*)
-by (blast_tac (claset() addSEs spies_partsEs
- addIs [impOfSubs analz_subset_parts]) 2);
+by (Blast_tac 2);
(*Fake*)
by (spy_analz_tac 1);
val lemma = result() RS mp RS mp RSN(2,rev_notE);
goal thy
- "!!evs. [| Says Server B \
-\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
-\ Crypt (shrK B) {|NB, Key K|}|} : set evs; \
-\ Says B Spy {|NA, NB, Key K|} ~: set evs; \
-\ A ~: bad; B ~: bad; evs : otway |] \
+ "!!evs. [| Says Server B \
+\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
+\ Crypt (shrK B) {|NB, Key K|}|} : set evs; \
+\ Notes Spy {|NA, NB, Key K|} ~: set evs; \
+\ A ~: bad; B ~: bad; evs : otway |] \
\ ==> Key K ~: analz (spies evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
by (blast_tac (claset() addSEs [lemma]) 1);
@@ -257,8 +257,7 @@
\ Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs";
by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
-by (Blast_tac 1);
+by (ALLGOALS Blast_tac);
qed_spec_mp "Crypt_imp_OR1";
@@ -277,16 +276,15 @@
\ Crypt (shrK A) {|NA, Key K|}, \
\ Crypt (shrK B) {|NB, Key K|}|} : set evs)";
by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
+(*Fake*)
+by (Blast_tac 1);
(*OR1: it cannot be a new Nonce, contradiction.*)
-by (blast_tac (claset() addSIs [parts_insertI]
- addSEs spies_partsEs) 1);
+by (Blast_tac 1);
(*OR3 and OR4*)
by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
by (ALLGOALS Clarify_tac);
(*OR4*)
-by (blast_tac (claset() addSIs [Crypt_imp_OR1]
- addEs spies_partsEs) 2);
+by (blast_tac (claset() addSIs [Crypt_imp_OR1]) 2);
(*OR3*) (** LEVEL 5 **)
(*The hypotheses at this point suggest an attack in which nonce NB is used
in two different roles:
--- a/src/HOL/Auth/OtwayRees_Bad.thy Thu Jan 08 18:09:47 1998 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.thy Thu Jan 08 18:10:34 1998 +0100
@@ -72,6 +72,6 @@
Oops "[| evso: otway; B ~= Spy;
Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
: set evso |]
- ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
+ ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
end
--- a/src/HOL/Auth/Yahalom.ML Thu Jan 08 18:09:47 1998 +0100
+++ b/src/HOL/Auth/Yahalom.ML Thu Jan 08 18:10:34 1998 +0100
@@ -202,12 +202,12 @@
(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
goal thy
- "!!evs. [| A ~: bad; B ~: bad; evs : yahalom |] \
+ "!!evs. [| A ~: bad; B ~: bad; evs : yahalom |] \
\ ==> Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \
\ Crypt (shrK B) {|Agent A, Key K|}|} \
\ : set evs --> \
-\ Says A Spy {|na, nb, Key K|} ~: set evs --> \
+\ Notes Spy {|na, nb, Key K|} ~: set evs --> \
\ Key K ~: analz (spies evs)";
by (etac yahalom.induct 1);
by analz_spies_tac;
@@ -232,8 +232,8 @@
\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \
\ Crypt (shrK B) {|Agent A, Key K|}|} \
\ : set evs; \
-\ Says A Spy {|na, nb, Key K|} ~: set evs; \
-\ A ~: bad; B ~: bad; evs : yahalom |] \
+\ Notes Spy {|na, nb, Key K|} ~: set evs; \
+\ A ~: bad; B ~: bad; evs : yahalom |] \
\ ==> Key K ~: analz (spies evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
by (blast_tac (claset() addSEs [lemma]) 1);
@@ -322,6 +322,12 @@
qed "KeyWithNonce_Says";
Addsimps [KeyWithNonce_Says];
+goalw thy [KeyWithNonce_def]
+ "KeyWithNonce K NB (Notes A X # evs) = KeyWithNonce K NB evs";
+by (Simp_tac 1);
+qed "KeyWithNonce_Notes";
+Addsimps [KeyWithNonce_Notes];
+
(*A fresh key cannot be associated with any nonce
(with respect to a given trace). *)
goalw thy [KeyWithNonce_def]
@@ -372,7 +378,8 @@
(analz_image_freshK_ss
addsimps expand_ifs
addsimps [all_conj_distrib, analz_image_freshK,
- KeyWithNonce_Says, fresh_not_KeyWithNonce,
+ KeyWithNonce_Says, KeyWithNonce_Notes,
+ fresh_not_KeyWithNonce,
imp_disj_not1, (*Moves NBa~=NB to the front*)
Says_Server_KeyWithNonce])));
(*Fake*)
@@ -478,7 +485,7 @@
\ ==> Says B Server \
\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
\ : set evs --> \
-\ (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs) --> \
+\ (ALL k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs) --> \
\ Nonce NB ~: analz (spies evs)";
by (etac yahalom.induct 1);
by analz_spies_tac;
@@ -529,7 +536,7 @@
(*B's session key guarantee from YM4. The two certificates contribute to a
- single conclusion about the Server's message. Note that the "Says A Spy"
+ single conclusion about the Server's message. Note that the "Notes Spy"
assumption must quantify over ALL POSSIBLE keys instead of our particular K.
If this run is broken and the spy substitutes a certificate containing an
old key, B has no means of telling.*)
@@ -539,7 +546,7 @@
\ : set evs; \
\ Says A' B {|Crypt (shrK B) {|Agent A, Key K|}, \
\ Crypt K (Nonce NB)|} : set evs; \
-\ ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs; \
+\ ALL k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs; \
\ A ~: bad; B ~: bad; evs : yahalom |] \
\ ==> Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, \
@@ -636,7 +643,7 @@
\ : set evs; \
\ Says A' B {|Crypt (shrK B) {|Agent A, Key K|}, \
\ Crypt K (Nonce NB)|} : set evs; \
-\ (ALL NA k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs); \
+\ (ALL NA k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs); \
\ A ~: bad; B ~: bad; evs : yahalom |] \
\ ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
by (dtac B_trusts_YM4 1);
--- a/src/HOL/Auth/Yahalom.thy Thu Jan 08 18:09:47 1998 +0100
+++ b/src/HOL/Auth/Yahalom.thy Thu Jan 08 18:10:34 1998 +0100
@@ -64,7 +64,7 @@
Says Server A {|Crypt (shrK A)
{|Agent B, Key K, Nonce NA, Nonce NB|},
X|} : set evso |]
- ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evso : yahalom"
+ ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : yahalom"
constdefs
--- a/src/HOL/Auth/Yahalom2.ML Thu Jan 08 18:09:47 1998 +0100
+++ b/src/HOL/Auth/Yahalom2.ML Thu Jan 08 18:10:34 1998 +0100
@@ -209,7 +209,7 @@
\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \
\ Crypt (shrK B) {|nb, Key K, Agent A|}|} \
\ : set evs --> \
-\ Says A Spy {|na, nb, Key K|} ~: set evs --> \
+\ Notes Spy {|na, nb, Key K|} ~: set evs --> \
\ Key K ~: analz (spies evs)";
by (etac yahalom.induct 1);
by analz_spies_tac;
@@ -235,8 +235,8 @@
\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \
\ Crypt (shrK B) {|nb, Key K, Agent A|}|} \
\ : set evs; \
-\ Says A Spy {|na, nb, Key K|} ~: set evs; \
-\ A ~: bad; B ~: bad; evs : yahalom |] \
+\ Notes Spy {|na, nb, Key K|} ~: set evs; \
+\ A ~: bad; B ~: bad; evs : yahalom |] \
\ ==> Key K ~: analz (spies evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
by (blast_tac (claset() addSEs [lemma]) 1);
@@ -249,8 +249,8 @@
May now apply Spy_not_see_encrypted_key, subject to its conditions.*)
goal thy
"!!evs. [| Crypt (shrK A) {|Agent B, Key K, na|} \
-\ : parts (spies evs); \
-\ A ~: bad; evs : yahalom |] \
+\ : parts (spies evs); \
+\ A ~: bad; evs : yahalom |] \
\ ==> EX nb. Says Server A \
\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \
\ Crypt (shrK B) {|nb, Key K, Agent A|}|} \
@@ -384,7 +384,7 @@
goal thy
"!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|}, \
\ Crypt K (Nonce NB)|} : set evs; \
-\ (ALL NA. Says A Spy {|Nonce NA, Nonce NB, Key K|} ~: set evs); \
+\ (ALL NA. Notes Spy {|Nonce NA, Nonce NB, Key K|} ~: set evs); \
\ A ~: bad; B ~: bad; evs : yahalom |] \
\ ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1);
--- a/src/HOL/Auth/Yahalom2.thy Thu Jan 08 18:09:47 1998 +0100
+++ b/src/HOL/Auth/Yahalom2.thy Thu Jan 08 18:10:34 1998 +0100
@@ -68,6 +68,6 @@
Says Server A {|Nonce NB,
Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
X|} : set evso |]
- ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evso : yahalom"
+ ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : yahalom"
end