Global change: lost->bad and sees Spy->spies
First change just gives a more sensible name.
Second change eliminates the agent parameter of "sees" to simplify
definitions and theorems
--- a/src/HOL/Auth/Event.ML Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/Event.ML Thu Sep 18 13:24:04 1997 +0200
@@ -10,147 +10,111 @@
open Event;
-AddIffs [Spy_in_lost, Server_not_lost];
-
-(**** Function "sees" ****)
-
-(** Specialized rewrite rules for (sees A' (Says A B X #evs)) **)
+AddIffs [Spy_in_bad, Server_not_bad];
-goal thy "sees B (Says A B X # evs) = insert X (sees B evs)";
-by (Simp_tac 1);
-qed "sees_own_Says";
-
-(** Three special-case rules for rewriting of sees A **)
+(**** Function "spies" ****)
-goal thy "!!A. Server ~= B ==> \
-\ sees Server (Says A B X # evs) = sees Server evs";
-by (Asm_simp_tac 1);
-qed "sees_Server_Says";
+(** Simplifying parts (insert X (spies evs))
+ = parts {X} Un parts (spies evs) -- since general case loops*)
-goal thy "!!A. Friend i ~= B ==> \
-\ sees (Friend i) (Says A B X # evs) = sees (Friend i) evs";
-by (Asm_simp_tac 1);
-qed "sees_Friend_Says";
-
-goal thy "sees Spy (Says A B X # evs) = insert X (sees Spy evs)";
-by (Simp_tac 1);
-qed "sees_Spy_Says";
+bind_thm ("parts_insert_spies",
+ parts_insert |>
+ read_instantiate_sg (sign_of thy) [("H", "spies evs")]);
-(** Specialized rewrite rules for (sees A' (Notes A X evs)) **)
-
-goal thy "sees A (Notes A X # evs) = insert X (sees A evs)";
-by (Simp_tac 1);
-qed "sees_own_Notes";
-
-(** Three special-case rules for rewriting of sees A **)
+goal thy
+ "P(event_case sf nf ev) = \
+\ ((ALL A B X. ev = Says A B X --> P(sf A B X)) & \
+\ (ALL A X. ev = Notes A X --> P(nf A X)))";
+by (induct_tac "ev" 1);
+by (Auto_tac());
+qed "expand_event_case";
-goal thy "!!A. Server ~= A ==> \
-\ sees Server (Notes A X # evs) = sees Server evs";
-by (Asm_simp_tac 1);
-qed "sees_Server_Notes";
-
-goal thy "!!A. Friend i ~= A ==> \
-\ sees (Friend i) (Notes A X # evs) = sees (Friend i) evs";
-by (Asm_simp_tac 1);
-qed "sees_Friend_Notes";
+goal thy "spies (Says A B X # evs) = insert X (spies evs)";
+by (Simp_tac 1);
+qed "spies_Says";
-(*The point of letting the Spy see "lost" agents' notes is to prevent
- redundant case-splits on whether A=Spy and whether A:lost*)
-goal thy "sees Spy (Notes A X # evs) = \
-\ (if A:lost then insert X (sees Spy evs) else sees Spy evs)";
-by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
-by (Blast_tac 1);
-qed "sees_Spy_Notes";
-
+(*The point of letting the Spy see "bad" agents' notes is to prevent
+ redundant case-splits on whether A=Spy and whether A:bad*)
+goal thy "spies (Notes A X # evs) = \
+\ (if A:bad then insert X (spies evs) else spies evs)";
+by (Simp_tac 1);
+qed "spies_Notes";
-(** Other "sees" lemmas **)
+goal thy "spies evs <= spies (Says A B X # evs)";
+by (simp_tac (!simpset addsimps [subset_insertI]) 1);
+qed "spies_subset_spies_Says";
-goal thy "sees A (Says A' B X # evs) <= insert X (sees A evs)";
-by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
-by (Fast_tac 1);
-qed "sees_Says_subset_insert";
-
-goal thy "sees A evs <= sees A (Says A' B X # evs)";
+goal thy "spies evs <= spies (Notes A X # evs)";
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
by (Fast_tac 1);
-qed "sees_subset_sees_Says";
-
-goal thy "sees A evs <= sees A (Notes A' X # evs)";
-by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
-by (Fast_tac 1);
-qed "sees_subset_sees_Notes";
-
-(*Pushing Unions into parts. One of the agents A is B, and thus sees Y.*)
-goal thy "(UN A. parts (sees A (Says B C Y # evs))) = \
-\ parts {Y} Un (UN A. parts (sees A evs))";
-by (Step_tac 1);
-by (etac rev_mp 1); (*split_tac does not work on assumptions*)
-by (ALLGOALS
- (fast_tac (!claset addss (!simpset addsimps [parts_Un]
- setloop split_tac [expand_if]))));
-qed "UN_parts_sees_Says";
-
-goal thy "(UN A. parts (sees A (Notes B Y # evs))) = \
-\ parts {Y} Un (UN A. parts (sees A evs))";
-by (Step_tac 1);
-by (etac rev_mp 1); (*split_tac does not work on assumptions*)
-by (ALLGOALS
- (fast_tac (!claset addss (!simpset addsimps [parts_Un]
- setloop split_tac [expand_if]))));
-qed "UN_parts_sees_Notes";
+qed "spies_subset_spies_Notes";
(*Spy sees all traffic*)
-goal thy "Says A B X : set evs --> X : sees Spy evs";
+goal thy "Says A B X : set evs --> X : spies evs";
by (induct_tac "evs" 1);
-by (Auto_tac ());
-qed_spec_mp "Says_imp_sees_Spy";
+by (ALLGOALS (asm_simp_tac
+ (!simpset setloop split_tac [expand_event_case, expand_if])));
+qed_spec_mp "Says_imp_spies";
-(*Spy sees Notes of lost agents*)
-goal thy "Notes A X : set evs --> A: lost --> X : sees Spy evs";
+(*Spy sees Notes of bad agents*)
+goal thy "Notes A X : set evs --> A: bad --> X : spies evs";
by (induct_tac "evs" 1);
-by (Auto_tac ());
-qed_spec_mp "Notes_imp_sees_Spy";
+by (ALLGOALS (asm_simp_tac
+ (!simpset setloop split_tac [expand_event_case, expand_if])));
+qed_spec_mp "Notes_imp_spies";
(*Use with addSEs to derive contradictions from old Says events containing
items known to be fresh*)
-val sees_Spy_partsEs = make_elim (Says_imp_sees_Spy RS parts.Inj) :: partsEs;
+val spies_partsEs = make_elim (Says_imp_spies RS parts.Inj) :: partsEs;
-Addsimps [sees_own_Says, sees_Server_Says, sees_Friend_Says, sees_Spy_Says,
- sees_own_Notes, sees_Server_Notes, sees_Friend_Notes, sees_Spy_Notes];
+Addsimps [spies_Says, spies_Notes];
-(**** NOTE REMOVAL--laws above are cleaner--def of sees1 is messy ****)
-Delsimps [sees_Cons];
+(**** NOTE REMOVAL--laws above are cleaner, as they don't involve "case" ****)
+Delsimps [spies_Cons];
(*** Fresh nonces ***)
-goalw thy [used_def] "!!X. X: parts (sees B evs) ==> X: used evs";
-by (etac (impOfSubs parts_mono) 1);
-by (Fast_tac 1);
-qed "usedI";
+goal thy "parts (spies evs) <= used evs";
+by (induct_tac "evs" 1);
+by (ALLGOALS (asm_simp_tac
+ (!simpset addsimps [parts_insert_spies]
+ setloop split_tac [expand_event_case, expand_if])));
+by (ALLGOALS Blast_tac);
+bind_thm ("usedI", impOfSubs (result()));
AddIs [usedI];
+goal thy "parts (initState B) <= used evs";
+by (induct_tac "evs" 1);
+by (ALLGOALS (asm_simp_tac
+ (!simpset addsimps [parts_insert_spies]
+ setloop split_tac [expand_event_case, expand_if])));
+by (ALLGOALS Blast_tac);
+bind_thm ("initState_into_used", impOfSubs (result()));
+
goal thy "used (Says A B X # evs) = parts{X} Un used evs";
-by (simp_tac (!simpset addsimps [used_def, UN_parts_sees_Says]) 1);
+by (Simp_tac 1);
qed "used_Says";
Addsimps [used_Says];
goal thy "used (Notes A X # evs) = parts{X} Un used evs";
-by (simp_tac (!simpset addsimps [used_def, UN_parts_sees_Notes]) 1);
+by (Simp_tac 1);
qed "used_Notes";
Addsimps [used_Notes];
-(*These two facts about "used" are unused.*)
-goal thy "used [] <= used l";
-by (induct_tac "l" 1);
-by (induct_tac "a" 2);
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS Blast_tac);
+goal thy "used [] <= used evs";
+by (Simp_tac 1);
+by (blast_tac (!claset addIs [initState_into_used]) 1);
qed "used_nil_subset";
-goal thy "used l <= used (l@l')";
-by (induct_tac "l" 1);
+(**** NOTE REMOVAL--laws above are cleaner, as they don't involve "case" ****)
+Delsimps [used_Nil, used_Cons];
+
+
+(*currently unused*)
+goal thy "used evs <= used (evs@evs')";
+by (induct_tac "evs" 1);
by (simp_tac (!simpset addsimps [used_nil_subset]) 1);
by (induct_tac "a" 1);
by (ALLGOALS Asm_simp_tac);
@@ -158,17 +122,7 @@
qed "used_subset_append";
-(** Simplifying parts (insert X (sees A evs))
- = parts {X} Un parts (sees A evs) -- since general case loops*)
-
-val parts_insert_sees =
- parts_insert |> read_instantiate_sg (sign_of thy)
- [("H", "sees A evs")]
- |> standard;
-
-
-
-(*For proving theorems of the form X ~: analz (sees Spy evs) --> P
+(*For proving theorems of the form X ~: analz (spies evs) --> P
New events added by induction to "evs" are discarded. Provided
this information isn't needed, the proof will be much shorter, since
it will omit complicated reasoning about analz.*)
@@ -179,8 +133,8 @@
rtac impI THEN'
REPEAT1 o
(dresolve_tac
- [sees_subset_sees_Says RS analz_mono RS contra_subsetD,
- sees_subset_sees_Notes RS analz_mono RS contra_subsetD])
+ [spies_subset_spies_Says RS analz_mono RS contra_subsetD,
+ spies_subset_spies_Notes RS analz_mono RS contra_subsetD])
THEN'
mp_tac
end;
--- a/src/HOL/Auth/Event.thy Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/Event.thy Thu Sep 18 13:24:04 1997 +0200
@@ -5,9 +5,9 @@
Theory of events for security protocols
-Datatype of events; function "sees"; freshness
+Datatype of events; function "spies"; freshness
-"lost" agents have been broken by the Spy; their private keys and internal
+"bad" agents have been broken by the Spy; their private keys and internal
stores are visible to him
*)
@@ -21,31 +21,33 @@
| Notes agent msg
consts
- lost :: agent set (*compromised agents*)
- sees :: [agent, event list] => msg set
+ bad :: agent set (*compromised agents*)
+ spies :: event list => msg set
rules
(*Spy has access to his own key for spoof messages, but Server is secure*)
- Spy_in_lost "Spy: lost"
- Server_not_lost "Server ~: lost"
+ Spy_in_bad "Spy: bad"
+ Server_not_bad "Server ~: bad"
-consts
- sees1 :: [agent, event] => msg set
-
-primrec sees1 event
+primrec spies list
(*Spy reads all traffic whether addressed to him or not*)
- sees1_Says "sees1 A (Says A' B X) = (if A:{B,Spy} then {X} else {})"
- sees1_Notes "sees1 A (Notes A' X) = (if A=A' | A=Spy & A':lost then {X}
- else {})"
+ spies_Nil "spies [] = initState Spy"
+ spies_Cons "spies (ev # evs) =
+ (case ev of
+ Says A B X => insert X (spies evs)
+ | Notes A X =>
+ if A:bad then insert X (spies evs) else spies evs)"
-primrec sees list
- sees_Nil "sees A [] = initState A"
- sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
+consts
+ (*Set of items that might be visible to somebody:
+ complement of the set of fresh items*)
+ used :: event list => msg set
-constdefs
- (*Set of items that might be visible to somebody: complement of the set
- of fresh items*)
- used :: event list => msg set
- "used evs == parts (UN B. sees B evs)"
+primrec used list
+ used_Nil "used [] = (UN B. parts (initState B))"
+ used_Cons "used (ev # evs) =
+ (case ev of
+ Says A B X => parts {X} Un (used evs)
+ | Notes A X => parts {X} Un (used evs))"
end
--- a/src/HOL/Auth/Message.ML Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/Message.ML Thu Sep 18 13:24:04 1997 +0200
@@ -875,7 +875,7 @@
(*** Tactics useful for many protocol proofs ***)
(*Prove base case (subgoal i) and simplify others. A typical base case
- concerns Crypt K X ~: Key``shrK``lost and cannot be proved by rewriting
+ concerns Crypt K X ~: Key``shrK``bad and cannot be proved by rewriting
alone.*)
fun prove_simple_subgoals_tac i =
fast_tac (!claset addss (!simpset)) i THEN
--- a/src/HOL/Auth/NS_Public.ML Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/NS_Public.ML Thu Sep 18 13:24:04 1997 +0200
@@ -12,7 +12,7 @@
proof_timing:=true;
HOL_quantifiers := false;
-AddIffs [Spy_in_lost];
+AddIffs [Spy_in_bad];
(*A "possibility property": there are traces that reach the end*)
goal thy
@@ -36,8 +36,8 @@
(*Induction for regularity theorems. If induction formula has the form
- X ~: analz (sees Spy evs) --> ... then it shortens the proof by discarding
- needless information about analz (insert X (sees Spy evs)) *)
+ X ~: analz (spies evs) --> ... then it shortens the proof by discarding
+ needless information about analz (insert X (spies evs)) *)
fun parts_induct_tac i =
etac ns_public.induct i
THEN
@@ -46,25 +46,25 @@
prove_simple_subgoals_tac i;
-(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
+(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
sends messages containing X! **)
-(*Spy never sees another agent's private key! (unless it's lost at start)*)
+(*Spy never sees another agent's private key! (unless it's bad at start)*)
goal thy
- "!!A. evs: ns_public ==> (Key (priK A) : parts (sees Spy evs)) = (A : lost)";
+ "!!A. evs: ns_public ==> (Key (priK A) : parts (spies evs)) = (A : bad)";
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
qed "Spy_see_priK";
Addsimps [Spy_see_priK];
goal thy
- "!!A. evs: ns_public ==> (Key (priK A) : analz (sees Spy evs)) = (A : lost)";
+ "!!A. evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
qed "Spy_analz_priK";
Addsimps [Spy_analz_priK];
-goal thy "!!A. [| Key (priK A) : parts (sees Spy evs); \
-\ evs : ns_public |] ==> A:lost";
+goal thy "!!A. [| Key (priK A) : parts (spies evs); \
+\ evs : ns_public |] ==> A:bad";
by (blast_tac (!claset addDs [Spy_see_priK]) 1);
qed "Spy_see_priK_D";
@@ -77,10 +77,10 @@
(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
is secret. (Honest users generate fresh nonces.)*)
goal thy
- "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees Spy evs); \
-\ Nonce NA ~: analz (sees Spy evs); \
+ "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \
+\ Nonce NA ~: analz (spies evs); \
\ evs : ns_public |] \
-\ ==> Crypt (pubK C) {|NA', Nonce NA, Agent D|} ~: parts (sees Spy evs)";
+\ ==> Crypt (pubK C) {|NA', Nonce NA, Agent D|} ~: parts (spies evs)";
by (etac rev_mp 1);
by (etac rev_mp 1);
by (parts_induct_tac 1);
@@ -94,14 +94,14 @@
(*Unicity for NS1: nonce NA identifies agents A and B*)
goal thy
- "!!evs. [| Nonce NA ~: analz (sees Spy evs); evs : ns_public |] \
+ "!!evs. [| Nonce NA ~: analz (spies evs); evs : ns_public |] \
\ ==> EX A' B'. ALL A B. \
-\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees Spy evs) --> \
+\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs) --> \
\ A=A' & B=B'";
by (etac rev_mp 1);
by (parts_induct_tac 1);
by (ALLGOALS
- (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees])));
+ (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_spies])));
(*NS1*)
by (expand_case_tac "NA = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2);
(*Fake*)
@@ -111,10 +111,10 @@
val lemma = result();
goal thy
- "!!evs. [| Crypt(pubK B) {|Nonce NA, Agent A|} : parts(sees Spy evs); \
-\ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(sees Spy evs); \
-\ Nonce NA ~: analz (sees Spy evs); \
-\ evs : ns_public |] \
+ "!!evs. [| Crypt(pubK B) {|Nonce NA, Agent A|} : parts(spies evs); \
+\ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies evs); \
+\ Nonce NA ~: analz (spies evs); \
+\ evs : ns_public |] \
\ ==> A=A' & B=B'";
by (prove_unique_tac lemma 1);
qed "unique_NA";
@@ -130,19 +130,19 @@
(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
goal thy
"!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \
-\ A ~: lost; B ~: lost; evs : ns_public |] \
-\ ==> Nonce NA ~: analz (sees Spy evs)";
+\ A ~: bad; B ~: bad; evs : ns_public |] \
+\ ==> Nonce NA ~: analz (spies evs)";
by (etac rev_mp 1);
by (analz_induct_tac 1);
(*NS3*)
-by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj]
+by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj]
addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
(*NS2*)
by (blast_tac (!claset addSEs [MPair_parts]
- addDs [Says_imp_sees_Spy RS parts.Inj,
+ addDs [Says_imp_spies RS parts.Inj,
parts.Body, unique_NA]) 3);
(*NS1*)
-by (blast_tac (!claset addSEs sees_Spy_partsEs
+by (blast_tac (!claset addSEs spies_partsEs
addIs [impOfSubs analz_subset_parts]) 2);
(*Fake*)
by (spy_analz_tac 1);
@@ -155,16 +155,16 @@
"!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs; \
\ Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
\ : set evs; \
-\ A ~: lost; B ~: lost; evs : ns_public |] \
+\ A ~: bad; B ~: bad; evs : ns_public |] \
\ ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
\ : set evs";
by (etac rev_mp 1);
(*prepare induction over Crypt (pubK A) {|NA,NB,B|} : parts H*)
-by (etac (Says_imp_sees_Spy RS parts.Inj RS rev_mp) 1);
+by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
by (etac ns_public.induct 1);
by (ALLGOALS Asm_simp_tac);
(*NS1*)
-by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
+by (blast_tac (!claset addSEs spies_partsEs) 2);
(*Fake*)
by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
addDs [Spy_not_see_NA,
@@ -173,9 +173,9 @@
(*If the encrypted message appears then it originated with Alice in NS1*)
goal thy
- "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees Spy evs); \
-\ Nonce NA ~: analz (sees Spy evs); \
-\ evs : ns_public |] \
+ "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \
+\ Nonce NA ~: analz (spies evs); \
+\ evs : ns_public |] \
\ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs";
by (etac rev_mp 1);
by (etac rev_mp 1);
@@ -191,14 +191,14 @@
[unicity of B makes Lowe's fix work]
[proof closely follows that for unique_NA] *)
goal thy
- "!!evs. [| Nonce NB ~: analz (sees Spy evs); evs : ns_public |] \
+ "!!evs. [| Nonce NB ~: analz (spies evs); evs : ns_public |] \
\ ==> EX A' NA' B'. ALL A NA B. \
-\ Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|} \
-\ : parts (sees Spy evs) --> A=A' & NA=NA' & B=B'";
+\ Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|} : parts (spies evs) \
+\ --> A=A' & NA=NA' & B=B'";
by (etac rev_mp 1);
by (parts_induct_tac 1);
by (ALLGOALS
- (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees])));
+ (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_spies])));
(*NS2*)
by (expand_case_tac "NB = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2);
(*Fake*)
@@ -209,10 +209,10 @@
goal thy
"!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|} \
-\ : parts(sees Spy evs); \
+\ : parts(spies evs); \
\ Crypt(pubK A') {|Nonce NA', Nonce NB, Agent B'|} \
-\ : parts(sees Spy evs); \
-\ Nonce NB ~: analz (sees Spy evs); \
+\ : parts(spies evs); \
+\ Nonce NB ~: analz (spies evs); \
\ evs : ns_public |] \
\ ==> A=A' & NA=NA' & B=B'";
by (prove_unique_tac lemma 1);
@@ -223,20 +223,20 @@
goal thy
"!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
\ : set evs; \
-\ A ~: lost; B ~: lost; evs : ns_public |] \
-\ ==> Nonce NB ~: analz (sees Spy evs)";
+\ A ~: bad; B ~: bad; evs : ns_public |] \
+\ ==> Nonce NB ~: analz (spies evs)";
by (etac rev_mp 1);
by (analz_induct_tac 1);
(*NS3*)
-by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj, unique_NB]) 4);
+by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj, unique_NB]) 4);
(*NS1*)
-by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
+by (blast_tac (!claset addSEs spies_partsEs) 2);
(*Fake*)
by (spy_analz_tac 1);
(*NS2*)
by (Step_tac 1);
-by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
+by (blast_tac (!claset addSEs spies_partsEs) 3);
+by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj]
addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 2);
by (blast_tac (!claset addSIs [impOfSubs analz_subset_parts]) 1);
qed "Spy_not_see_NB";
@@ -248,21 +248,21 @@
"!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
\ : set evs; \
\ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \
-\ A ~: lost; B ~: lost; evs : ns_public |] \
+\ A ~: bad; B ~: bad; evs : ns_public |] \
\ ==> Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
by (etac rev_mp 1);
(*prepare induction over Crypt (pubK B) NB : parts H*)
-by (etac (Says_imp_sees_Spy RS parts.Inj RS rev_mp) 1);
+by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
by (parts_induct_tac 1);
(*NS1*)
-by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
+by (blast_tac (!claset addSEs spies_partsEs) 2);
(*Fake*)
by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
addDs [Spy_not_see_NB,
impOfSubs analz_subset_parts]) 1);
(*NS3; not clear why blast_tac needs to be preceeded by Step_tac*)
by (Step_tac 1);
-by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj,
+by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj,
Spy_not_see_NB, unique_NB]) 1);
qed "B_trusts_NS3";
@@ -270,8 +270,8 @@
(**** Overall guarantee for B*)
(*Matches only NS2, not NS1 (or NS3)*)
-val Says_imp_sees_Spy' =
- read_instantiate [("X","Crypt ?K {|?XX,?YY,?ZZ|}")] Says_imp_sees_Spy;
+val Says_imp_spies' =
+ read_instantiate [("X","Crypt ?K {|?XX,?YY,?ZZ|}")] Says_imp_spies;
(*If B receives NS3 and the nonce NB agrees with the nonce he joined with
@@ -280,16 +280,16 @@
"!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
\ : set evs; \
\ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \
-\ A ~: lost; B ~: lost; evs : ns_public |] \
+\ A ~: bad; B ~: bad; evs : ns_public |] \
\ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs";
by (etac rev_mp 1);
(*prepare induction over Crypt (pubK B) {|NB|} : parts H*)
-by (etac (Says_imp_sees_Spy RS parts.Inj RS rev_mp) 1);
+by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
by (etac ns_public.induct 1);
by (ALLGOALS Asm_simp_tac);
(*Fake, NS2, NS3*)
(*NS1*)
-by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
+by (blast_tac (!claset addSEs spies_partsEs) 2);
(*Fake*)
by (REPEAT_FIRST (resolve_tac [impI, conjI]));
by (Blast_tac 1);
@@ -300,7 +300,7 @@
(*NS3*)
by (Step_tac 1);
by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
+by (blast_tac (!claset addSDs [Says_imp_spies' RS parts.Inj]
addDs [unique_NB]) 1);
qed "B_trusts_protocol";
--- a/src/HOL/Auth/NS_Public.thy Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/NS_Public.thy Thu Sep 18 13:24:04 1997 +0200
@@ -20,7 +20,7 @@
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
Fake "[| evs: ns_public; B ~= Spy;
- X: synth (analz (sees Spy evs)) |]
+ X: synth (analz (spies evs)) |]
==> Says Spy B X # evs : ns_public"
(*Alice initiates a protocol run, sending a nonce to Bob*)
--- a/src/HOL/Auth/NS_Public_Bad.ML Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.ML Thu Sep 18 13:24:04 1997 +0200
@@ -16,7 +16,7 @@
proof_timing:=true;
HOL_quantifiers := false;
-AddIffs [Spy_in_lost];
+AddIffs [Spy_in_bad];
(*A "possibility property": there are traces that reach the end*)
goal thy
@@ -40,8 +40,8 @@
(*Induction for regularity theorems. If induction formula has the form
- X ~: analz (sees Spy evs) --> ... then it shortens the proof by discarding
- needless information about analz (insert X (sees Spy evs)) *)
+ X ~: analz (spies evs) --> ... then it shortens the proof by discarding
+ needless information about analz (insert X (spies evs)) *)
fun parts_induct_tac i =
etac ns_public.induct i
THEN
@@ -50,25 +50,25 @@
prove_simple_subgoals_tac i;
-(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
+(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
sends messages containing X! **)
-(*Spy never sees another agent's private key! (unless it's lost at start)*)
+(*Spy never sees another agent's private key! (unless it's bad at start)*)
goal thy
- "!!A. evs: ns_public ==> (Key (priK A) : parts (sees Spy evs)) = (A : lost)";
+ "!!A. evs: ns_public ==> (Key (priK A) : parts (spies evs)) = (A : bad)";
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
qed "Spy_see_priK";
Addsimps [Spy_see_priK];
goal thy
- "!!A. evs: ns_public ==> (Key (priK A) : analz (sees Spy evs)) = (A : lost)";
+ "!!A. evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
qed "Spy_analz_priK";
Addsimps [Spy_analz_priK];
-goal thy "!!A. [| Key (priK A) : parts (sees Spy evs); \
-\ evs : ns_public |] ==> A:lost";
+goal thy "!!A. [| Key (priK A) : parts (spies evs); \
+\ evs : ns_public |] ==> A:bad";
by (blast_tac (!claset addDs [Spy_see_priK]) 1);
qed "Spy_see_priK_D";
@@ -81,9 +81,9 @@
(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
is secret. (Honest users generate fresh nonces.)*)
goal thy
- "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees Spy evs); \
-\ Nonce NA ~: analz (sees Spy evs); evs : ns_public |] \
-\ ==> Crypt (pubK C) {|NA', Nonce NA|} ~: parts (sees Spy evs)";
+ "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \
+\ Nonce NA ~: analz (spies evs); evs : ns_public |] \
+\ ==> Crypt (pubK C) {|NA', Nonce NA|} ~: parts (spies evs)";
by (etac rev_mp 1);
by (etac rev_mp 1);
by (parts_induct_tac 1);
@@ -97,14 +97,14 @@
(*Unicity for NS1: nonce NA identifies agents A and B*)
goal thy
- "!!evs. [| Nonce NA ~: analz (sees Spy evs); evs : ns_public |] \
+ "!!evs. [| Nonce NA ~: analz (spies evs); evs : ns_public |] \
\ ==> EX A' B'. ALL A B. \
-\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees Spy evs) --> \
+\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs) --> \
\ A=A' & B=B'";
by (etac rev_mp 1);
by (parts_induct_tac 1);
by (ALLGOALS
- (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees])));
+ (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_spies])));
(*NS1*)
by (expand_case_tac "NA = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2);
(*Fake*)
@@ -114,9 +114,9 @@
val lemma = result();
goal thy
- "!!evs. [| Crypt(pubK B) {|Nonce NA, Agent A|} : parts(sees Spy evs); \
-\ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(sees Spy evs); \
-\ Nonce NA ~: analz (sees Spy evs); \
+ "!!evs. [| Crypt(pubK B) {|Nonce NA, Agent A|} : parts(spies evs); \
+\ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies evs); \
+\ Nonce NA ~: analz (spies evs); \
\ evs : ns_public |] \
\ ==> A=A' & B=B'";
by (prove_unique_tac lemma 1);
@@ -133,19 +133,19 @@
(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
goal thy
"!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \
-\ A ~: lost; B ~: lost; evs : ns_public |] \
-\ ==> Nonce NA ~: analz (sees Spy evs)";
+\ A ~: bad; B ~: bad; evs : ns_public |] \
+\ ==> Nonce NA ~: analz (spies evs)";
by (etac rev_mp 1);
by (analz_induct_tac 1);
(*NS3*)
-by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj]
+by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj]
addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
(*NS2*)
by (blast_tac (!claset addSEs [MPair_parts]
- addDs [Says_imp_sees_Spy RS parts.Inj,
+ addDs [Says_imp_spies RS parts.Inj,
parts.Body, unique_NA]) 3);
(*NS1*)
-by (blast_tac (!claset addSEs sees_Spy_partsEs
+by (blast_tac (!claset addSEs spies_partsEs
addIs [impOfSubs analz_subset_parts]) 2);
(*Fake*)
by (spy_analz_tac 1);
@@ -157,29 +157,29 @@
goal thy
"!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs; \
\ Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs; \
-\ A ~: lost; B ~: lost; evs : ns_public |] \
+\ A ~: bad; B ~: bad; evs : ns_public |] \
\ ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs";
by (etac rev_mp 1);
(*prepare induction over Crypt (pubK A) {|NA,NB|} : parts H*)
-by (etac (Says_imp_sees_Spy RS parts.Inj RS rev_mp) 1);
+by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
by (etac ns_public.induct 1);
by (ALLGOALS Asm_simp_tac);
(*NS1*)
-by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
+by (blast_tac (!claset addSEs spies_partsEs) 2);
(*Fake*)
by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
addDs [Spy_not_see_NA,
impOfSubs analz_subset_parts]) 1);
(*NS2; not clear why blast_tac needs to be preceeded by Step_tac*)
by (Step_tac 1);
-by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj,
+by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj,
Spy_not_see_NA, unique_NA]) 1);
qed "A_trusts_NS2";
(*If the encrypted message appears then it originated with Alice in NS1*)
goal thy
- "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees Spy evs); \
-\ Nonce NA ~: analz (sees Spy evs); \
+ "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \
+\ Nonce NA ~: analz (spies evs); \
\ evs : ns_public |] \
\ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs";
by (etac rev_mp 1);
@@ -195,14 +195,14 @@
(*Unicity for NS2: nonce NB identifies agent A and nonce NA
[proof closely follows that for unique_NA] *)
goal thy
- "!!evs. [| Nonce NB ~: analz (sees Spy evs); evs : ns_public |] \
+ "!!evs. [| Nonce NB ~: analz (spies evs); evs : ns_public |] \
\ ==> EX A' NA'. ALL A NA. \
\ Crypt (pubK A) {|Nonce NA, Nonce NB|} \
-\ : parts (sees Spy evs) --> A=A' & NA=NA'";
+\ : parts (spies evs) --> A=A' & NA=NA'";
by (etac rev_mp 1);
by (parts_induct_tac 1);
by (ALLGOALS
- (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees])));
+ (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_spies])));
(*NS2*)
by (expand_case_tac "NB = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2);
(*Fake*)
@@ -212,9 +212,9 @@
val lemma = result();
goal thy
- "!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB|} : parts(sees Spy evs); \
-\ Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(sees Spy evs); \
-\ Nonce NB ~: analz (sees Spy evs); \
+ "!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB|} : parts(spies evs); \
+\ Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(spies evs); \
+\ Nonce NB ~: analz (spies evs); \
\ evs : ns_public |] \
\ ==> A=A' & NA=NA'";
by (prove_unique_tac lemma 1);
@@ -225,13 +225,13 @@
goal thy
"!!evs.[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs; \
\ (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set evs); \
-\ A ~: lost; B ~: lost; evs : ns_public |] \
-\ ==> Nonce NB ~: analz (sees Spy evs)";
+\ A ~: bad; B ~: bad; evs : ns_public |] \
+\ ==> Nonce NB ~: analz (spies evs)";
by (etac rev_mp 1);
by (etac rev_mp 1);
by (analz_induct_tac 1);
(*NS1*)
-by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
+by (blast_tac (!claset addSEs spies_partsEs) 2);
(*Fake*)
by (spy_analz_tac 1);
(*NS2 and NS3*)
@@ -239,10 +239,10 @@
by (step_tac (!claset delrules [allI]) 1);
by (Blast_tac 5);
(*NS3*)
-by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj, unique_NB]) 4);
+by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj, unique_NB]) 4);
(*NS2*)
-by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
+by (blast_tac (!claset addSEs spies_partsEs) 3);
+by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj]
addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 2);
by (blast_tac (!claset addSIs [impOfSubs analz_subset_parts]) 1);
qed "Spy_not_see_NB";
@@ -254,35 +254,35 @@
goal thy
"!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs; \
\ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \
-\ A ~: lost; B ~: lost; evs : ns_public |] \
+\ A ~: bad; B ~: bad; evs : ns_public |] \
\ ==> EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set evs";
by (etac rev_mp 1);
(*prepare induction over Crypt (pubK B) NB : parts H*)
-by (etac (Says_imp_sees_Spy RS parts.Inj RS rev_mp) 1);
+by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
by (parts_induct_tac 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
(*NS1*)
-by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
+by (blast_tac (!claset addSEs spies_partsEs) 2);
(*Fake*)
by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
addDs [Spy_not_see_NB,
impOfSubs analz_subset_parts]) 1);
(*NS3; not clear why blast_tac needs to be preceeded by Step_tac*)
by (Step_tac 1);
-by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj,
+by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj,
Spy_not_see_NB, unique_NB]) 1);
qed "B_trusts_NS3";
(*Can we strengthen the secrecy theorem? NO*)
goal thy
- "!!evs. [| A ~: lost; B ~: lost; evs : ns_public |] \
+ "!!evs. [| A ~: bad; B ~: bad; evs : ns_public |] \
\ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs \
-\ --> Nonce NB ~: analz (sees Spy evs)";
+\ --> Nonce NB ~: analz (spies evs)";
by (analz_induct_tac 1);
(*NS1*)
by (blast_tac (!claset addSEs partsEs
- addSDs [Says_imp_sees_Spy RS parts.Inj]) 2);
+ addSDs [Says_imp_spies RS parts.Inj]) 2);
(*Fake*)
by (spy_analz_tac 1);
(*NS2 and NS3*)
@@ -290,27 +290,27 @@
by (blast_tac (!claset addSIs [impOfSubs analz_subset_parts, usedI]) 1);
(*NS2*)
by (blast_tac (!claset addSEs partsEs
- addSDs [Says_imp_sees_Spy RS parts.Inj]) 2);
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
+ addSDs [Says_imp_spies RS parts.Inj]) 2);
+by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj]
addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1);
(*NS3*)
-by (forw_inst_tac [("A'","A")] (Says_imp_sees_Spy RS parts.Inj RS unique_NB) 1
- THEN REPEAT (eresolve_tac [asm_rl, Says_imp_sees_Spy RS parts.Inj] 1));
+by (forw_inst_tac [("A'","A")] (Says_imp_spies RS parts.Inj RS unique_NB) 1
+ THEN REPEAT (eresolve_tac [asm_rl, Says_imp_spies RS parts.Inj] 1));
by (Step_tac 1);
(*
THIS IS THE ATTACK!
Level 9
-!!evs. [| A ~: lost; B ~: lost; evs : ns_public |]
+!!evs. [| A ~: bad; B ~: bad; evs : ns_public |]
==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
: set evs -->
- Nonce NB ~: analz (sees Spy evs)
+ Nonce NB ~: analz (spies evs)
1. !!evs Aa Ba B' NAa NBa evsa.
- [| A ~: lost; B ~: lost; evsa : ns_public; A ~= Ba;
+ [| A ~: bad; B ~: bad; evsa : ns_public; A ~= Ba;
Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evsa;
Says A Ba (Crypt (pubK Ba) {|Nonce NA, Agent A|}) : set evsa;
- Ba : lost;
+ Ba : bad;
Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evsa;
- Nonce NB ~: analz (sees Spy evsa) |]
+ Nonce NB ~: analz (spies evsa) |]
==> False
*)
--- a/src/HOL/Auth/NS_Public_Bad.thy Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.thy Thu Sep 18 13:24:04 1997 +0200
@@ -24,7 +24,7 @@
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
Fake "[| evs: ns_public; B ~= Spy;
- X: synth (analz (sees Spy evs)) |]
+ X: synth (analz (spies evs)) |]
==> Says Spy B X # evs : ns_public"
(*Alice initiates a protocol run, sending a nonce to Bob*)
--- a/src/HOL/Auth/NS_Shared.ML Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/NS_Shared.ML Thu Sep 18 13:24:04 1997 +0200
@@ -48,31 +48,30 @@
(*For reasoning about the encrypted portion of message NS3*)
goal thy "!!evs. Says S A (Crypt KA {|N, B, K, X|}) : set evs \
-\ ==> X : parts (sees Spy evs)";
-by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
-qed "NS3_msg_in_parts_sees_Spy";
+\ ==> X : parts (spies evs)";
+by (blast_tac (!claset addSEs spies_partsEs) 1);
+qed "NS3_msg_in_parts_spies";
goal thy
"!!evs. Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set evs \
-\ ==> K : parts (sees Spy evs)";
-by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
-qed "Oops_parts_sees_Spy";
+\ ==> K : parts (spies evs)";
+by (blast_tac (!claset addSEs spies_partsEs) 1);
+qed "Oops_parts_spies";
-(*For proving the easier theorems about X ~: parts (sees Spy evs).*)
+(*For proving the easier theorems about X ~: parts (spies evs).*)
fun parts_induct_tac i =
etac ns_shared.induct i THEN
- forward_tac [Oops_parts_sees_Spy] (i+7) THEN
- dtac NS3_msg_in_parts_sees_Spy (i+4) THEN
+ forward_tac [Oops_parts_spies] (i+7) THEN
+ dtac NS3_msg_in_parts_spies (i+4) THEN
prove_simple_subgoals_tac i;
-(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
+(** 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 lost at start)*)
+(*Spy never sees another agent's shared key! (unless it's bad at start)*)
goal thy
- "!!evs. evs : ns_shared \
-\ ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
+ "!!evs. evs : ns_shared ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (Blast_tac 1);
@@ -80,14 +79,13 @@
Addsimps [Spy_see_shrK];
goal thy
- "!!evs. evs : ns_shared \
-\ ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
+ "!!evs. evs : ns_shared ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
qed "Spy_analz_shrK";
Addsimps [Spy_analz_shrK];
-goal thy "!!A. [| Key (shrK A) : parts (sees Spy evs); \
-\ evs : ns_shared |] ==> A:lost";
+goal thy "!!A. [| Key (shrK A) : parts (spies evs); \
+\ evs : ns_shared |] ==> A:bad";
by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
qed "Spy_see_shrK_D";
@@ -97,7 +95,7 @@
(*Nobody can have used non-existent keys!*)
goal thy "!!evs. evs : ns_shared ==> \
-\ Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
+\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
by (parts_induct_tac 1);
(*Fake*)
by (best_tac
@@ -106,7 +104,7 @@
impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
addss (!simpset)) 1);
(*NS2, NS4, NS5*)
-by (ALLGOALS (blast_tac (!claset addSEs sees_Spy_partsEs)));
+by (ALLGOALS (blast_tac (!claset addSEs spies_partsEs)));
qed_spec_mp "new_keys_not_used";
bind_thm ("new_keys_not_analzd",
@@ -120,8 +118,7 @@
(*Describes the form of K, X and K' when the Server sends this message.*)
goal thy
- "!!evs. [| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) \
-\ : set evs; \
+ "!!evs. [| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) : set evs; \
\ evs : ns_shared |] \
\ ==> K ~: range shrK & \
\ X = (Crypt (shrK B) {|Key K, Agent A|}) & \
@@ -134,9 +131,8 @@
(*If the encrypted message appears then it originated with the Server*)
goal thy
- "!!evs. [| Crypt (shrK A) {|NA, Agent B, Key K, X|} \
-\ : parts (sees Spy evs); \
-\ A ~: lost; evs : ns_shared |] \
+ "!!evs. [| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
+\ A ~: bad; evs : ns_shared |] \
\ ==> Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \
\ : set evs";
by (etac rev_mp 1);
@@ -153,17 +149,17 @@
\ : set evs; \
\ evs : ns_shared |] \
\ ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|})) \
-\ | X : analz (sees Spy evs)";
-by (case_tac "A : lost" 1);
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
+\ | X : analz (spies evs)";
+by (case_tac "A : bad" 1);
+by (fast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]
addss (!simpset)) 1);
-by (forward_tac [Says_imp_sees_Spy RS parts.Inj] 1);
+by (forward_tac [Says_imp_spies RS parts.Inj] 1);
by (blast_tac (!claset addSDs [A_trusts_NS2, Says_Server_message_form]) 1);
qed "Says_S_message_form";
(*For proofs involving analz.*)
-val analz_sees_tac =
+val analz_spies_tac =
forward_tac [Says_Server_message_form] 8 THEN
forward_tac [Says_S_message_form] 5 THEN
REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac);
@@ -172,8 +168,8 @@
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
- Key K : analz (sees Spy evs)
+ Key K : analz (insert (Key KAB) (spies evs)) ==>
+ Key K : analz (spies evs)
A more general formula must be proved inductively.
@@ -185,8 +181,8 @@
We require that agents should behave like this subsequently also.*)
goal thy
"!!evs. [| evs : ns_shared; Kab ~: range shrK |] ==> \
-\ (Crypt KAB X) : parts (sees Spy evs) & \
-\ Key K : parts {X} --> Key K : parts (sees Spy evs)";
+\ (Crypt KAB X) : parts (spies evs) & \
+\ Key K : parts {X} --> Key K : parts (spies evs)";
by (parts_induct_tac 1);
(*Deals with Faked messages*)
by (blast_tac (!claset addSEs partsEs
@@ -202,10 +198,10 @@
goal thy
"!!evs. evs : ns_shared ==> \
\ ALL K KK. KK <= Compl (range shrK) --> \
-\ (Key K : analz (Key``KK Un (sees Spy evs))) = \
-\ (K : KK | Key K : analz (sees Spy evs))";
+\ (Key K : analz (Key``KK Un (spies evs))) = \
+\ (K : KK | Key K : analz (spies evs))";
by (etac ns_shared.induct 1);
-by analz_sees_tac;
+by analz_spies_tac;
by (REPEAT_FIRST (resolve_tac [allI, impI]));
by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
(*Takes 24 secs*)
@@ -219,8 +215,8 @@
goal thy
"!!evs. [| evs : ns_shared; KAB ~: range shrK |] ==> \
-\ Key K : analz (insert (Key KAB) (sees Spy evs)) = \
-\ (K = KAB | Key K : analz (sees Spy evs))";
+\ Key K : analz (insert (Key KAB) (spies evs)) = \
+\ (K = KAB | Key K : analz (spies evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
qed "analz_insert_freshK";
@@ -230,8 +226,8 @@
goal thy
"!!evs. evs : ns_shared ==> \
\ EX A' NA' B' X'. ALL A NA B X. \
-\ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \
-\ : set evs --> A=A' & NA=NA' & B=B' & X=X'";
+\ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs \
+\ --> A=A' & NA=NA' & B=B' & X=X'";
by (etac ns_shared.induct 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
by (Step_tac 1);
@@ -242,17 +238,15 @@
by (expand_case_tac "K = ?y" 1);
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
by (blast_tac (!claset delrules [conjI] (*prevent split-up into 4 subgoals*)
- addSEs sees_Spy_partsEs) 1);
+ addSEs spies_partsEs) 1);
val lemma = result();
(*In messages of this form, the session key uniquely identifies the rest*)
goal thy
"!!evs. [| Says Server A \
-\ (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \
-\ : set evs; \
+\ (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs; \
\ Says Server A' \
-\ (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) \
-\ : set evs; \
+\ (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) : set evs; \
\ evs : ns_shared |] ==> A=A' & NA=NA' & B=B' & X = X'";
by (prove_unique_tac lemma 1);
qed "unique_session_keys";
@@ -261,15 +255,15 @@
(** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
goal thy
- "!!evs. [| A ~: lost; B ~: lost; evs : ns_shared |] \
+ "!!evs. [| A ~: bad; B ~: bad; evs : ns_shared |] \
\ ==> Says Server A \
\ (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) --> \
-\ Key K ~: analz (sees Spy evs)";
+\ Key K ~: analz (spies evs)";
by (etac ns_shared.induct 1);
-by analz_sees_tac;
+by analz_spies_tac;
by (ALLGOALS
(asm_simp_tac
(!simpset addsimps ([analz_insert_eq, analz_insert_freshK] @ pushes)
@@ -279,16 +273,16 @@
(*NS3, replay sub-case*)
by (Blast_tac 4);
(*NS2*)
-by (blast_tac (!claset addSEs sees_Spy_partsEs
+by (blast_tac (!claset addSEs spies_partsEs
addIs [parts_insertI, impOfSubs analz_subset_parts]) 2);
(*Fake*)
by (spy_analz_tac 1);
(*NS3, Server sub-case*) (**LEVEL 6 **)
by (step_tac (!claset delrules [impCE]) 1);
-by (forward_tac [Says_imp_sees_Spy RS parts.Inj RS A_trusts_NS2] 1);
+by (forward_tac [Says_imp_spies RS parts.Inj RS A_trusts_NS2] 1);
by (assume_tac 2);
-by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj RS
- Crypt_Spy_analz_lost]) 1);
+by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj RS
+ Crypt_Spy_analz_bad]) 1);
by (blast_tac (!claset addDs [unique_session_keys]) 1);
val lemma = result() RS mp RS mp RSN(2,rev_notE);
@@ -298,8 +292,8 @@
"!!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); \
-\ A ~: lost; B ~: lost; evs : ns_shared \
-\ |] ==> Key K ~: analz (sees Spy 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);
by (blast_tac (!claset addSDs [lemma]) 1);
qed "Spy_not_see_encrypted_key";
@@ -312,8 +306,8 @@
(*If the encrypted message appears then it originated with the Server*)
goal thy
- "!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (sees Spy evs); \
-\ B ~: lost; evs : ns_shared |] \
+ "!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs); \
+\ B ~: bad; evs : ns_shared |] \
\ ==> EX NA. Says Server A \
\ (Crypt (shrK A) {|NA, Agent B, Key K, \
\ Crypt (shrK B) {|Key K, Agent A|}|}) \
@@ -327,19 +321,19 @@
goal thy
- "!!evs. [| B ~: lost; evs : ns_shared |] \
-\ ==> Key K ~: analz (sees Spy evs) --> \
+ "!!evs. [| B ~: bad; evs : ns_shared |] \
+\ ==> Key K ~: analz (spies evs) --> \
\ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \
\ : set evs --> \
-\ Crypt K (Nonce NB) : parts (sees Spy evs) --> \
+\ Crypt K (Nonce NB) : parts (spies evs) --> \
\ Says B A (Crypt K (Nonce NB)) : set evs";
by (etac ns_shared.induct 1);
by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);
-by (dtac NS3_msg_in_parts_sees_Spy 5);
-by (forward_tac [Oops_parts_sees_Spy] 8);
+by (dtac NS3_msg_in_parts_spies 5);
+by (forward_tac [Oops_parts_spies] 8);
by (TRYALL (rtac impI));
by (REPEAT_FIRST
- (dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD)));
+ (dtac (spies_subset_spies_Says RS analz_mono RS contra_subsetD)));
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
(**LEVEL 7**)
by (blast_tac (!claset addSDs [Crypt_Fake_parts_insert]
@@ -347,25 +341,25 @@
by (Blast_tac 2);
by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac));
(*Subgoal 1: contradiction from the assumptions
- Key K ~: used evsa and Crypt K (Nonce NB) : parts (sees Spy evsa) *)
+ Key K ~: used evsa and Crypt K (Nonce NB) : parts (spies evsa) *)
by (dtac Crypt_imp_invKey_keysFor 1);
(**LEVEL 11**)
by (Asm_full_simp_tac 1);
by (rtac disjI1 1);
by (thin_tac "?PP-->?QQ" 1);
-by (case_tac "Ba : lost" 1);
-by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS B_trusts_NS3,
+by (case_tac "Ba : bad" 1);
+by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj RS B_trusts_NS3,
unique_session_keys]) 2);
-by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj RS
- Crypt_Spy_analz_lost]) 1);
+by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj RS
+ Crypt_Spy_analz_bad]) 1);
val lemma = result();
goal thy
- "!!evs. [| Crypt K (Nonce NB) : parts (sees Spy evs); \
+ "!!evs. [| Crypt K (Nonce NB) : parts (spies evs); \
\ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \
\ : set evs; \
\ ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs; \
-\ A ~: lost; B ~: lost; evs : ns_shared |] \
+\ A ~: bad; B ~: bad; evs : ns_shared |] \
\ ==> Says B A (Crypt K (Nonce NB)) : set evs";
by (blast_tac (!claset addSIs [lemma RS mp RS mp RS mp]
addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1);
--- a/src/HOL/Auth/NS_Shared.thy Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/NS_Shared.thy Thu Sep 18 13:24:04 1997 +0200
@@ -22,7 +22,7 @@
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
Fake "[| evs: ns_shared; B ~= Spy;
- X: synth (analz (sees Spy evs)) |]
+ X: synth (analz (spies evs)) |]
==> Says Spy B X # evs : ns_shared"
(*Alice initiates a protocol run, requesting to talk to any B*)
--- a/src/HOL/Auth/OtwayRees.ML Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/OtwayRees.ML Thu Sep 18 13:24:04 1997 +0200
@@ -44,46 +44,46 @@
(** For reasoning about the encrypted portion of messages **)
goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs \
-\ ==> X : analz (sees Spy evs)";
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
-qed "OR2_analz_sees_Spy";
+\ ==> X : analz (spies evs)";
+by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1);
+qed "OR2_analz_spies";
goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
-\ ==> X : analz (sees Spy evs)";
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
-qed "OR4_analz_sees_Spy";
+\ ==> X : analz (spies evs)";
+by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1);
+qed "OR4_analz_spies";
goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
-\ ==> K : parts (sees Spy evs)";
-by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
-qed "Oops_parts_sees_Spy";
+\ ==> K : parts (spies evs)";
+by (blast_tac (!claset addSEs spies_partsEs) 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_sees_Spy",
- OR2_analz_sees_Spy RS (impOfSubs analz_subset_parts));
-bind_thm ("OR4_parts_sees_Spy",
- OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
+bind_thm ("OR2_parts_spies",
+ OR2_analz_spies RS (impOfSubs analz_subset_parts));
+bind_thm ("OR4_parts_spies",
+ OR4_analz_spies RS (impOfSubs analz_subset_parts));
-(*For proving the easier theorems about X ~: parts (sees Spy evs).*)
+(*For proving the easier theorems about X ~: parts (spies evs).*)
fun parts_induct_tac i =
etac otway.induct i THEN
- forward_tac [Oops_parts_sees_Spy] (i+6) THEN
- forward_tac [OR4_parts_sees_Spy] (i+5) THEN
- forward_tac [OR2_parts_sees_Spy] (i+3) THEN
+ forward_tac [Oops_parts_spies] (i+6) THEN
+ forward_tac [OR4_parts_spies] (i+5) THEN
+ forward_tac [OR2_parts_spies] (i+3) THEN
prove_simple_subgoals_tac i;
-(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
+(** 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 lost at start)*)
+(*Spy never sees another agent's shared key! (unless it's bad at start)*)
goal thy
- "!!evs. evs : otway ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
+ "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (Blast_tac 1);
@@ -91,13 +91,12 @@
Addsimps [Spy_see_shrK];
goal thy
- "!!evs. evs : otway ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
+ "!!evs. evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
qed "Spy_analz_shrK";
Addsimps [Spy_analz_shrK];
-goal thy "!!A. [| Key (shrK A) : parts (sees Spy evs); \
-\ evs : otway |] ==> A:lost";
+goal thy "!!A. [| Key (shrK A) : parts (spies evs); evs : otway |] ==> A:bad";
by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
qed "Spy_see_shrK_D";
@@ -107,7 +106,7 @@
(*Nobody can have used non-existent keys!*)
goal thy "!!evs. evs : otway ==> \
-\ Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
+\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
by (parts_induct_tac 1);
(*Fake*)
by (best_tac
@@ -142,9 +141,9 @@
(*For proofs involving analz.*)
-val analz_sees_tac =
- dtac OR2_analz_sees_Spy 4 THEN
- dtac OR4_analz_sees_Spy 6 THEN
+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
REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
@@ -153,8 +152,8 @@
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
- Key K : analz (sees Spy evs)
+ Key K : analz (insert (Key KAB) (spies evs)) ==>
+ Key K : analz (spies evs)
A more general formula must be proved inductively.
****)
@@ -166,10 +165,10 @@
goal thy
"!!evs. evs : otway ==> \
\ ALL K KK. KK <= Compl (range shrK) --> \
-\ (Key K : analz (Key``KK Un (sees Spy evs))) = \
-\ (K : KK | Key K : analz (sees Spy evs))";
+\ (Key K : analz (Key``KK Un (spies evs))) = \
+\ (K : KK | Key K : analz (spies evs))";
by (etac otway.induct 1);
-by analz_sees_tac;
+by analz_spies_tac;
by (REPEAT_FIRST (resolve_tac [allI, impI]));
by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
@@ -182,8 +181,8 @@
goal thy
"!!evs. [| evs : otway; KAB ~: range shrK |] ==> \
-\ Key K : analz (insert (Key KAB) (sees Spy evs)) = \
-\ (K = KAB | Key K : analz (sees Spy evs))";
+\ Key K : analz (insert (Key KAB) (spies evs)) = \
+\ (K = KAB | Key K : analz (spies evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
qed "analz_insert_freshK";
@@ -204,7 +203,7 @@
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 sees_Spy_partsEs
+by (blast_tac (!claset addSEs spies_partsEs
delrules [conjI] (*no split-up into 4 subgoals*)) 1);
val lemma = result();
@@ -221,9 +220,8 @@
(*Only OR1 can have caused such a part of a message to appear.*)
goal thy
- "!!evs. [| A ~: lost; evs : otway |] \
-\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \
-\ : parts (sees Spy evs) --> \
+ "!!evs. [| A ~: bad; evs : otway |] \
+\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
\ Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
\ : set evs";
@@ -235,22 +233,22 @@
(** The Nonce NA uniquely identifies A's message. **)
goal thy
- "!!evs. [| evs : otway; A ~: lost |] \
+ "!!evs. [| evs : otway; A ~: bad |] \
\ ==> EX B'. ALL B. \
-\ Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (sees Spy evs) \
+\ Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) \
\ --> B = B'";
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (simp_tac (!simpset addsimps [all_conj_distrib]) 1);
(*OR1: creation of new Nonce. Move assertion into global context*)
by (expand_case_tac "NA = ?y" 1);
-by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
+by (blast_tac (!claset addSEs spies_partsEs) 1);
val lemma = result();
goal thy
- "!!evs.[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (sees Spy evs); \
-\ Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (sees Spy evs); \
-\ evs : otway; A ~: lost |] \
+ "!!evs.[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (spies evs); \
+\ Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (spies evs); \
+\ evs : otway; A ~: bad |] \
\ ==> B = C";
by (prove_unique_tac lemma 1);
qed "unique_NA";
@@ -260,14 +258,13 @@
OR2 encrypts Nonce NB. It prevents the attack that can occur in the
over-simplified version of this protocol: see OtwayRees_Bad.*)
goal thy
- "!!evs. [| A ~: lost; evs : otway |] \
-\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \
-\ : parts (sees Spy evs) --> \
+ "!!evs. [| A ~: bad; evs : otway |] \
+\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
\ Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \
-\ ~: parts (sees Spy evs)";
+\ ~: parts (spies evs)";
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
-by (REPEAT (blast_tac (!claset addSEs sees_Spy_partsEs
+by (REPEAT (blast_tac (!claset addSEs spies_partsEs
addSDs [impOfSubs parts_insert_subset_Un]) 1));
qed_spec_mp"no_nonce_OR1_OR2";
@@ -275,8 +272,8 @@
(*Crucial property: If the encrypted message appears, and A has used NA
to start a run, then it originated with the Server!*)
goal thy
- "!!evs. [| A ~: lost; A ~= Spy; evs : otway |] \
-\ ==> Crypt (shrK A) {|NA, Key K|} : parts (sees Spy evs) \
+ "!!evs. [| A ~: bad; A ~= Spy; evs : otway |] \
+\ ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs) \
\ --> Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
\ : set evs --> \
@@ -288,21 +285,21 @@
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
(*OR1: it cannot be a new Nonce, contradiction.*)
-by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1);
+by (blast_tac (!claset addSIs [parts_insertI] addSEs spies_partsEs) 1);
(*OR3 and OR4*)
(*OR4*)
by (REPEAT (Safe_step_tac 2));
by (REPEAT (blast_tac (!claset addSDs [parts_cut]) 3));
by (blast_tac (!claset addSIs [Crypt_imp_OR1]
- addEs sees_Spy_partsEs) 2);
+ addEs spies_partsEs) 2);
(*OR3*) (** LEVEL 5 **)
by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
by (step_tac (!claset delrules [disjCI, impCE]) 1);
by (blast_tac (!claset addSEs [MPair_parts]
- addSDs [Says_imp_sees_Spy RS parts.Inj]
+ addSDs [Says_imp_spies RS parts.Inj]
addEs [no_nonce_OR1_OR2 RSN (2, rev_notE)]
delrules [conjI] (*stop split-up into 4 subgoals*)) 2);
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
+by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj]
addSEs [MPair_parts]
addIs [unique_NA]) 1);
qed_spec_mp "NA_Crypt_imp_Server_msg";
@@ -313,19 +310,17 @@
bad form of this protocol, even though we can prove
Spy_not_see_encrypted_key*)
goal thy
- "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} \
-\ : set evs; \
-\ Says A B {|NA, Agent A, Agent B, \
-\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
-\ : set evs; \
-\ A ~: lost; A ~= Spy; evs : otway |] \
+ "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
+\ Says A B {|NA, Agent A, Agent B, \
+\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
+\ A ~: bad; A ~= Spy; evs : otway |] \
\ ==> EX NB. Says Server B \
\ {|NA, \
\ Crypt (shrK A) {|NA, Key K|}, \
\ Crypt (shrK B) {|NB, Key K|}|} \
\ : set evs";
by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
- addEs sees_Spy_partsEs) 1);
+ addEs spies_partsEs) 1);
qed "A_trusts_OR4";
@@ -334,14 +329,14 @@
the premises, e.g. by having A=Spy **)
goal thy
- "!!evs. [| A ~: lost; B ~: lost; 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 --> \
-\ Key K ~: analz (sees Spy evs)";
+\ Key K ~: analz (spies evs)";
by (etac otway.induct 1);
-by analz_sees_tac;
+by analz_spies_tac;
by (ALLGOALS
(asm_simp_tac (!simpset addcongs [conj_cong]
addsimps [analz_insert_eq, analz_insert_freshK]
@@ -351,7 +346,7 @@
(*OR4*)
by (Blast_tac 3);
(*OR3*)
-by (blast_tac (!claset addSEs sees_Spy_partsEs
+by (blast_tac (!claset addSEs spies_partsEs
addIs [impOfSubs analz_subset_parts]) 2);
(*Fake*)
by (spy_analz_tac 1);
@@ -362,8 +357,8 @@
\ {|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 ~: lost; B ~: lost; evs : otway |] \
-\ ==> Key K ~: analz (sees Spy 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);
qed "Spy_not_see_encrypted_key";
@@ -374,9 +369,9 @@
(*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.*)
goal thy
- "!!evs. [| B ~: lost; evs : otway |] \
+ "!!evs. [| B ~: bad; evs : otway |] \
\ ==> Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \
-\ : parts (sees Spy evs) --> \
+\ : parts (spies evs) --> \
\ (EX X. Says B Server \
\ {|NA, Agent A, Agent B, X, \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \
@@ -390,24 +385,22 @@
(** The Nonce NB uniquely identifies B's message. **)
goal thy
- "!!evs. [| evs : otway; B ~: lost |] \
+ "!!evs. [| evs : otway; B ~: bad |] \
\ ==> EX NA' A'. ALL NA A. \
-\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(sees Spy evs) \
+\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs) \
\ --> NA = NA' & A = A'";
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (simp_tac (!simpset addsimps [all_conj_distrib]) 1);
(*OR2: creation of new Nonce. Move assertion into global context*)
by (expand_case_tac "NB = ?y" 1);
-by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
+by (blast_tac (!claset addSEs spies_partsEs) 1);
val lemma = result();
goal thy
- "!!evs.[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \
-\ : parts(sees Spy evs); \
-\ Crypt (shrK B) {|NC, NB, Agent C, Agent B|} \
-\ : parts(sees Spy evs); \
-\ evs : otway; B ~: lost |] \
+ "!!evs.[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs); \
+\ Crypt (shrK B) {|NC, NB, Agent C, Agent B|} : parts(spies evs); \
+\ evs : otway; B ~: bad |] \
\ ==> NC = NA & C = A";
by (prove_unique_tac lemma 1);
qed "unique_NB";
@@ -416,8 +409,8 @@
(*If the encrypted message appears, and B has used Nonce NB,
then it originated with the Server!*)
goal thy
- "!!evs. [| B ~: lost; B ~= Spy; evs : otway |] \
-\ ==> Crypt (shrK B) {|NB, Key K|} : parts (sees Spy evs) \
+ "!!evs. [| B ~: bad; B ~= Spy; evs : otway |] \
+\ ==> Crypt (shrK B) {|NB, Key K|} : parts (spies evs) \
\ --> (ALL X'. Says B Server \
\ {|NA, Agent A, Agent B, X', \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \
@@ -429,17 +422,17 @@
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
(*OR1: it cannot be a new Nonce, contradiction.*)
-by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1);
+by (blast_tac (!claset addSIs [parts_insertI] addSEs spies_partsEs) 1);
(*OR4*)
by (blast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 2);
(*OR3*)
by (step_tac (!claset delrules [disjCI, impCE]) 1);
by (blast_tac (!claset delrules [conjI] (*stop split-up*)) 3);
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
+by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj]
addSEs [MPair_parts]
addDs [unique_NB]) 2);
by (blast_tac (!claset addSEs [MPair_parts, no_nonce_OR1_OR2 RSN (2, rev_notE)]
- addSDs [Says_imp_sees_Spy RS parts.Inj]
+ addSDs [Says_imp_spies RS parts.Inj]
delrules [conjI, impCE] (*stop split-up*)) 1);
qed_spec_mp "NB_Crypt_imp_Server_msg";
@@ -447,9 +440,8 @@
(*Guarantee for B: if it gets a message with matching NB then the Server
has sent the correct message.*)
goal thy
- "!!evs. [| B ~: lost; B ~= Spy; evs : otway; \
-\ Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \
-\ : set evs; \
+ "!!evs. [| B ~: bad; B ~= Spy; evs : otway; \
+\ Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
\ Says B Server {|NA, Agent A, Agent B, X', \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
\ : set evs |] \
@@ -459,7 +451,7 @@
\ Crypt (shrK B) {|NB, Key K|}|} \
\ : set evs";
by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
- addSEs sees_Spy_partsEs) 1);
+ addSEs spies_partsEs) 1);
qed "B_trusts_OR3";
@@ -467,7 +459,7 @@
goal thy
- "!!evs. [| B ~: lost; evs : otway |] \
+ "!!evs. [| B ~: bad; evs : otway |] \
\ ==> Says Server B \
\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
\ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \
@@ -476,7 +468,7 @@
\ : set evs)";
by (etac otway.induct 1);
by (ALLGOALS Asm_simp_tac);
-by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj]
+by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj]
addSEs [MPair_parts, Crypt_imp_OR2]) 3);
by (ALLGOALS Blast_tac);
bind_thm ("OR3_imp_OR2", result() RSN (2,rev_mp) RS exE);
@@ -489,7 +481,7 @@
"!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
\ Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
-\ A ~: lost; A ~= Spy; B ~: lost; evs : otway |] \
+\ A ~: bad; A ~= Spy; B ~: bad; evs : otway |] \
\ ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X, \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}\
\ : set evs";
--- a/src/HOL/Auth/OtwayRees.thy Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/OtwayRees.thy Thu Sep 18 13:24:04 1997 +0200
@@ -24,7 +24,7 @@
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
Fake "[| evs: otway; B ~= Spy;
- X: synth (analz (sees Spy evs)) |]
+ X: synth (analz (spies evs)) |]
==> Says Spy B X # evs : otway"
(*Alice initiates a protocol run*)
--- a/src/HOL/Auth/OtwayRees_AN.ML Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML Thu Sep 18 13:24:04 1997 +0200
@@ -44,36 +44,36 @@
(** For reasoning about the encrypted portion of messages **)
goal thy "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \
-\ X : analz (sees Spy evs)";
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
-qed "OR4_analz_sees_Spy";
+\ X : analz (spies evs)";
+by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1);
+qed "OR4_analz_spies";
goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
-\ : set evs ==> K : parts (sees Spy evs)";
-by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
-qed "Oops_parts_sees_Spy";
+\ : set evs ==> K : parts (spies evs)";
+by (blast_tac (!claset addSEs spies_partsEs) 1);
+qed "Oops_parts_spies";
-(*OR4_analz_sees_Spy lets us treat those cases using the same
+(*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_sees_Spy",
- OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
+bind_thm ("OR4_parts_spies",
+ OR4_analz_spies RS (impOfSubs analz_subset_parts));
-(*For proving the easier theorems about X ~: parts (sees Spy evs).*)
+(*For proving the easier theorems about X ~: parts (spies evs).*)
fun parts_induct_tac i =
etac otway.induct i THEN
- forward_tac [Oops_parts_sees_Spy] (i+6) THEN
- forward_tac [OR4_parts_sees_Spy] (i+5) THEN
+ forward_tac [Oops_parts_spies] (i+6) THEN
+ forward_tac [OR4_parts_spies] (i+5) THEN
prove_simple_subgoals_tac i;
-(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
+(** 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 lost at start)*)
+(*Spy never sees another agent's shared key! (unless it's bad at start)*)
goal thy
- "!!evs. evs : otway ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
+ "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (Blast_tac 1);
@@ -81,13 +81,12 @@
Addsimps [Spy_see_shrK];
goal thy
- "!!evs. evs : otway ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
+ "!!evs. evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
qed "Spy_analz_shrK";
Addsimps [Spy_analz_shrK];
-goal thy "!!A. [| Key (shrK A) : parts (sees Spy evs); \
-\ evs : otway |] ==> A:lost";
+goal thy "!!A. [| Key (shrK A) : parts (spies evs); evs : otway |] ==> A:bad";
by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
qed "Spy_see_shrK_D";
@@ -97,7 +96,7 @@
(*Nobody can have used non-existent keys!*)
goal thy "!!evs. evs : otway ==> \
-\ Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
+\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
by (parts_induct_tac 1);
(*Fake*)
by (best_tac
@@ -135,8 +134,8 @@
(*For proofs involving analz.*)
-val analz_sees_tac =
- dtac OR4_analz_sees_Spy 6 THEN
+val analz_spies_tac =
+ dtac OR4_analz_spies 6 THEN
forward_tac [Says_Server_message_form] 7 THEN
assume_tac 7 THEN
REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
@@ -145,8 +144,8 @@
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
- Key K : analz (sees Spy evs)
+ Key K : analz (insert (Key KAB) (spies evs)) ==>
+ Key K : analz (spies evs)
A more general formula must be proved inductively.
****)
@@ -158,10 +157,10 @@
goal thy
"!!evs. evs : otway ==> \
\ ALL K KK. KK <= Compl (range shrK) --> \
-\ (Key K : analz (Key``KK Un (sees Spy evs))) = \
-\ (K : KK | Key K : analz (sees Spy evs))";
+\ (Key K : analz (Key``KK Un (spies evs))) = \
+\ (K : KK | Key K : analz (spies evs))";
by (etac otway.induct 1);
-by analz_sees_tac;
+by analz_spies_tac;
by (REPEAT_FIRST (resolve_tac [allI, impI]));
by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
@@ -174,8 +173,8 @@
goal thy
"!!evs. [| evs : otway; KAB ~: range shrK |] ==> \
-\ Key K : analz (insert (Key KAB) (sees Spy evs)) = \
-\ (K = KAB | Key K : analz (sees Spy evs))";
+\ Key K : analz (insert (Key KAB) (spies evs)) = \
+\ (K = KAB | Key K : analz (spies evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
qed "analz_insert_freshK";
@@ -198,7 +197,7 @@
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 sees_Spy_partsEs
+by (blast_tac (!claset addSEs spies_partsEs
delrules[conjI] (*prevent splitup into 4 subgoals*)) 1);
val lemma = result();
@@ -223,9 +222,8 @@
(*If the encrypted message appears then it originated with the Server!*)
goal thy
- "!!evs. [| A ~: lost; evs : otway |] \
-\ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} \
-\ : parts (sees Spy evs) \
+ "!!evs. [| A ~: bad; evs : otway |] \
+\ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} : parts (spies evs) \
\ --> (EX NB. Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
@@ -243,13 +241,13 @@
goal thy
"!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \
\ : set evs; \
-\ A ~: lost; evs : otway |] \
+\ A ~: bad; evs : otway |] \
\ ==> EX NB. 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";
by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
- addEs sees_Spy_partsEs) 1);
+ addEs spies_partsEs) 1);
qed "A_trusts_OR4";
@@ -258,15 +256,15 @@
the premises, e.g. by having A=Spy **)
goal thy
- "!!evs. [| A ~: lost; B ~: lost; 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 --> \
-\ Key K ~: analz (sees Spy evs)";
+\ Key K ~: analz (spies evs)";
by (etac otway.induct 1);
-by analz_sees_tac;
+by analz_spies_tac;
by (ALLGOALS
(asm_simp_tac (!simpset addcongs [conj_cong, if_weak_cong]
addsimps [analz_insert_eq, analz_insert_freshK]
@@ -276,7 +274,7 @@
(*OR4*)
by (Blast_tac 3);
(*OR3*)
-by (blast_tac (!claset addSEs sees_Spy_partsEs
+by (blast_tac (!claset addSEs spies_partsEs
addIs [impOfSubs analz_subset_parts]) 2);
(*Fake*)
by (spy_analz_tac 1);
@@ -288,8 +286,8 @@
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
\ : set evs; \
\ Says B Spy {|NA, NB, Key K|} ~: set evs; \
-\ A ~: lost; B ~: lost; evs : otway |] \
-\ ==> Key K ~: analz (sees Spy 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);
qed "Spy_not_see_encrypted_key";
@@ -299,9 +297,8 @@
(*If the encrypted message appears then it originated with the Server!*)
goal thy
- "!!evs. [| B ~: lost; evs : otway |] \
-\ ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} \
-\ : parts (sees Spy evs) \
+ "!!evs. [| B ~: bad; evs : otway |] \
+\ ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} : parts (spies evs) \
\ --> (EX NA. Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
@@ -317,7 +314,7 @@
(*Guarantee for B: if it gets a well-formed certificate then the Server
has sent the correct message in round 3.*)
goal thy
- "!!evs. [| B ~: lost; evs : otway; \
+ "!!evs. [| B ~: bad; evs : otway; \
\ Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
\ : set evs |] \
\ ==> EX NA. Says Server B \
@@ -325,5 +322,5 @@
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
\ : set evs";
by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
- addEs sees_Spy_partsEs) 1);
+ addEs spies_partsEs) 1);
qed "B_trusts_OR3";
--- a/src/HOL/Auth/OtwayRees_AN.thy Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.thy Thu Sep 18 13:24:04 1997 +0200
@@ -29,7 +29,7 @@
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
Fake "[| evs: otway; B ~= Spy;
- X: synth (analz (sees Spy evs)) |]
+ X: synth (analz (spies evs)) |]
==> Says Spy B X # evs : otway"
(*Alice initiates a protocol run*)
--- a/src/HOL/Auth/OtwayRees_Bad.ML Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Thu Sep 18 13:24:04 1997 +0200
@@ -47,45 +47,45 @@
(** For reasoning about the encrypted portion of messages **)
goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs ==> \
-\ X : analz (sees Spy evs)";
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
-qed "OR2_analz_sees_Spy";
+\ X : analz (spies evs)";
+by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1);
+qed "OR2_analz_spies";
goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs ==> \
-\ X : analz (sees Spy evs)";
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
-qed "OR4_analz_sees_Spy";
+\ X : analz (spies evs)";
+by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1);
+qed "OR4_analz_spies";
goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
-\ ==> K : parts (sees Spy evs)";
-by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
-qed "Oops_parts_sees_Spy";
+\ ==> K : parts (spies evs)";
+by (blast_tac (!claset addSEs spies_partsEs) 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_sees_Spy",
- OR2_analz_sees_Spy RS (impOfSubs analz_subset_parts));
-bind_thm ("OR4_parts_sees_Spy",
- OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
+bind_thm ("OR2_parts_spies",
+ OR2_analz_spies RS (impOfSubs analz_subset_parts));
+bind_thm ("OR4_parts_spies",
+ OR4_analz_spies RS (impOfSubs analz_subset_parts));
-(*For proving the easier theorems about X ~: parts (sees Spy evs).*)
+(*For proving the easier theorems about X ~: parts (spies evs).*)
fun parts_induct_tac i =
etac otway.induct i THEN
- forward_tac [Oops_parts_sees_Spy] (i+6) THEN
- forward_tac [OR4_parts_sees_Spy] (i+5) THEN
- forward_tac [OR2_parts_sees_Spy] (i+3) THEN
+ forward_tac [Oops_parts_spies] (i+6) THEN
+ forward_tac [OR4_parts_spies] (i+5) THEN
+ forward_tac [OR2_parts_spies] (i+3) THEN
prove_simple_subgoals_tac i;
-(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
+(** 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 lost at start)*)
+(*Spy never sees another agent's shared key! (unless it's bad at start)*)
goal thy
- "!!evs. evs : otway ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
+ "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (Blast_tac 1);
@@ -93,13 +93,12 @@
Addsimps [Spy_see_shrK];
goal thy
- "!!evs. evs : otway ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
+ "!!evs. evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
qed "Spy_analz_shrK";
Addsimps [Spy_analz_shrK];
-goal thy "!!A. [| Key (shrK A) : parts (sees Spy evs); \
-\ evs : otway |] ==> A:lost";
+goal thy "!!A. [| Key (shrK A) : parts (spies evs); evs : otway |] ==> A:bad";
by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
qed "Spy_see_shrK_D";
@@ -109,7 +108,7 @@
(*Nobody can have used non-existent keys!*)
goal thy "!!evs. evs : otway ==> \
-\ Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
+\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
by (parts_induct_tac 1);
(*Fake*)
by (best_tac
@@ -146,9 +145,9 @@
(*For proofs involving analz.*)
-val analz_sees_tac =
- dtac OR2_analz_sees_Spy 4 THEN
- dtac OR4_analz_sees_Spy 6 THEN
+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
REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
@@ -156,8 +155,8 @@
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
- Key K : analz (sees Spy evs)
+ Key K : analz (insert (Key KAB) (spies evs)) ==>
+ Key K : analz (spies evs)
A more general formula must be proved inductively.
****)
@@ -169,10 +168,10 @@
goal thy
"!!evs. evs : otway ==> \
\ ALL K KK. KK <= Compl (range shrK) --> \
-\ (Key K : analz (Key``KK Un (sees Spy evs))) = \
-\ (K : KK | Key K : analz (sees Spy evs))";
+\ (Key K : analz (Key``KK Un (spies evs))) = \
+\ (K : KK | Key K : analz (spies evs))";
by (etac otway.induct 1);
-by analz_sees_tac;
+by analz_spies_tac;
by (REPEAT_FIRST (resolve_tac [allI, impI]));
by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
@@ -185,8 +184,8 @@
goal thy
"!!evs. [| evs : otway; KAB ~: range shrK |] ==> \
-\ Key K : analz (insert (Key KAB) (sees Spy evs)) = \
-\ (K = KAB | Key K : analz (sees Spy evs))";
+\ Key K : analz (insert (Key KAB) (spies evs)) = \
+\ (K = KAB | Key K : analz (spies evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
qed "analz_insert_freshK";
@@ -207,7 +206,7 @@
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 sees_Spy_partsEs
+by (blast_tac (!claset addSEs spies_partsEs
delrules [conjI] (*no split-up to 4 subgoals*)) 1);
val lemma = result();
@@ -221,14 +220,14 @@
(*Crucial security property, but not itself enough to guarantee correctness!*)
goal thy
- "!!evs. [| A ~: lost; B ~: lost; 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 --> \
-\ Key K ~: analz (sees Spy evs)";
+\ Key K ~: analz (spies evs)";
by (etac otway.induct 1);
-by analz_sees_tac;
+by analz_spies_tac;
by (ALLGOALS
(asm_simp_tac (!simpset addcongs [conj_cong]
addsimps [analz_insert_eq, analz_insert_freshK]
@@ -238,7 +237,7 @@
(*OR4*)
by (Blast_tac 3);
(*OR3*)
-by (blast_tac (!claset addSEs sees_Spy_partsEs
+by (blast_tac (!claset addSEs spies_partsEs
addIs [impOfSubs analz_subset_parts]) 2);
(*Fake*)
by (spy_analz_tac 1);
@@ -249,8 +248,8 @@
\ {|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 ~: lost; B ~: lost; evs : otway |] \
-\ ==> Key K ~: analz (sees Spy 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);
qed "Spy_not_see_encrypted_key";
@@ -263,9 +262,8 @@
Perhaps it's because OR2 has two similar-looking encrypted messages in
this version.*)
goal thy
- "!!evs. [| A ~: lost; A ~= B; evs : otway |] \
-\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \
-\ : parts (sees Spy evs) --> \
+ "!!evs. [| A ~: bad; A ~= B; evs : otway |] \
+\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
\ Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs";
by (parts_induct_tac 1);
@@ -279,8 +277,8 @@
(*Only it is FALSE. Somebody could make a fake message to Server
substituting some other nonce NA' for NB.*)
goal thy
- "!!evs. [| A ~: lost; A ~= Spy; evs : otway |] \
-\ ==> Crypt (shrK A) {|NA, Key K|} : parts (sees Spy evs) --> \
+ "!!evs. [| A ~: bad; A ~= Spy; evs : otway |] \
+\ ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs) --> \
\ Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
\ : set evs --> \
@@ -292,12 +290,12 @@
by (Fake_parts_insert_tac 1);
(*OR1: it cannot be a new Nonce, contradiction.*)
by (blast_tac (!claset addSIs [parts_insertI]
- addSEs sees_Spy_partsEs) 1);
+ addSEs spies_partsEs) 1);
(*OR4*)
by (REPEAT (Safe_step_tac 2));
by (REPEAT (blast_tac (!claset addSDs [parts_cut]) 3));
by (blast_tac (!claset addSIs [Crypt_imp_OR1]
- addEs sees_Spy_partsEs) 2);
+ addEs spies_partsEs) 2);
(*OR3*) (** LEVEL 5 **)
by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
by (step_tac (!claset delrules [disjCI, impCE]) 1);
--- a/src/HOL/Auth/OtwayRees_Bad.thy Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.thy Thu Sep 18 13:24:04 1997 +0200
@@ -22,7 +22,7 @@
(*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 "[| evs: otway; B ~= Spy; X: synth (analz (sees Spy evs)) |]
+ Fake "[| evs: otway; B ~= Spy; X: synth (analz (spies evs)) |]
==> Says Spy B X # evs : otway"
(*Alice initiates a protocol run*)
--- a/src/HOL/Auth/Public.ML Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/Public.ML Thu Sep 18 13:24:04 1997 +0200
@@ -44,49 +44,50 @@
Addsimps [keysFor_parts_initState];
-(*** Function "sees" ***)
+(*** Function "spies" ***)
(*Agents see their own private keys!*)
-goal thy "A ~= Spy --> Key (priK A) : sees A evs";
-by (induct_tac "evs" 1);
+goal thy "Key (priK A) : initState A";
by (induct_tac "A" 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
-qed_spec_mp "sees_own_priK";
+by (Auto_tac());
+qed "priK_in_initState";
+AddIffs [priK_in_initState];
-(*All public keys are visible to all*)
-goal thy "Key (pubK A) : sees B evs";
+(*All public keys are visible*)
+goal thy "Key (pubK A) : spies evs";
by (induct_tac "evs" 1);
-by (induct_tac "B" 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
-by (Auto_tac ());
-qed_spec_mp "sees_pubK";
+by (ALLGOALS (asm_simp_tac
+ (!simpset addsimps [imageI, spies_Cons]
+ setloop split_tac [expand_event_case, expand_if])));
+qed_spec_mp "spies_pubK";
-(*Spy sees private keys of agents!*)
-goal thy "!!A. A: lost ==> Key (priK A) : sees Spy evs";
+(*Spy sees private keys of bad agents!*)
+goal thy "!!A. A: bad ==> Key (priK A) : spies evs";
by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
-by (Blast_tac 1);
-qed "Spy_sees_lost";
+by (ALLGOALS (asm_simp_tac
+ (!simpset addsimps [imageI, spies_Cons]
+ setloop split_tac [expand_event_case, expand_if])));
+qed "Spy_spies_bad";
-AddIffs [sees_pubK, sees_pubK RS analz.Inj];
-AddSIs [sees_own_priK, Spy_sees_lost];
+AddIffs [spies_pubK, spies_pubK RS analz.Inj];
+AddSIs [Spy_spies_bad];
-(*For not_lost_tac*)
-goal thy "!!A. [| Crypt (pubK A) X : analz (sees Spy evs); A: lost |] \
-\ ==> X : analz (sees Spy evs)";
+(*For not_bad_tac*)
+goal thy "!!A. [| Crypt (pubK A) X : analz (spies evs); A: bad |] \
+\ ==> X : analz (spies evs)";
by (blast_tac (!claset addSDs [analz.Decrypt]) 1);
-qed "Crypt_Spy_analz_lost";
+qed "Crypt_Spy_analz_bad";
(*Prove that the agent is uncompromised by the confidentiality of
a component of a message she's said.*)
-fun not_lost_tac s =
- case_tac ("(" ^ s ^ ") : lost") THEN'
+fun not_bad_tac s =
+ case_tac ("(" ^ s ^ ") : bad") THEN'
SELECT_GOAL
- (REPEAT_DETERM (dtac (Says_imp_sees_Spy RS analz.Inj) 1) THEN
+ (REPEAT_DETERM (dtac (Says_imp_spies RS analz.Inj) 1) THEN
REPEAT_DETERM (etac MPair_analz 1) THEN
THEN_BEST_FIRST
- (dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN assume_tac 1)
+ (dres_inst_tac [("A", s)] Crypt_Spy_analz_bad 1 THEN assume_tac 1)
(has_fewer_prems 1, size_of_thm)
(Step_tac 1));
@@ -100,27 +101,30 @@
AddIffs [Nonce_notin_initState];
goal thy "Nonce N ~: used []";
-by (simp_tac (!simpset addsimps [used_def]) 1);
+by (simp_tac (!simpset addsimps [used_Nil]) 1);
qed "Nonce_notin_used_empty";
Addsimps [Nonce_notin_used_empty];
(*** Supply fresh nonces for possibility theorems. ***)
-goalw thy [used_def] "EX N. ALL n. N<=n --> Nonce n ~: used evs";
+(*In any trace, there is an upper bound N on the greatest nonce in use.*)
+goal thy "EX N. ALL n. N<=n --> Nonce n ~: used evs";
by (induct_tac "evs" 1);
by (res_inst_tac [("x","0")] exI 1);
+by (ALLGOALS (asm_simp_tac
+ (!simpset addsimps [used_Cons]
+ setloop split_tac [expand_event_case, expand_if])));
by (Step_tac 1);
-by (Full_simp_tac 1);
-(*Inductive step*)
-by (induct_tac "a" 1);
-by (ALLGOALS (full_simp_tac
- (!simpset addsimps [UN_parts_sees_Says,
- UN_parts_sees_Notes])));
by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
by (ALLGOALS (blast_tac (!claset addSEs [add_leE])));
val lemma = result();
+goal thy "EX N. Nonce N ~: used evs";
+by (rtac (lemma RS exE) 1);
+by (Blast_tac 1);
+qed "Nonce_supply1";
+
goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
by (rtac (lemma RS exE) 1);
by (rtac selectI 1);
--- a/src/HOL/Auth/Public.thy Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/Public.thy Thu Sep 18 13:24:04 1997 +0200
@@ -26,7 +26,7 @@
initState_Friend "initState (Friend i) =
insert (Key (priK (Friend i))) (Key `` range pubK)"
initState_Spy "initState Spy =
- (Key``invKey``pubK``lost) Un (Key `` range pubK)"
+ (Key``invKey``pubK``bad) Un (Key `` range pubK)"
rules
--- a/src/HOL/Auth/Recur.ML Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/Recur.ML Thu Sep 18 13:24:04 1997 +0200
@@ -112,45 +112,45 @@
(** For reasoning about the encrypted portion of messages **)
-val RA2_analz_sees_Spy = Says_imp_sees_Spy RS analz.Inj |> standard;
+val RA2_analz_spies = Says_imp_spies RS analz.Inj |> standard;
goal thy "!!evs. Says C' B {|Crypt K X, X', RA|} : set evs \
-\ ==> RA : analz (sees Spy evs)";
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
-qed "RA4_analz_sees_Spy";
+\ ==> RA : analz (spies evs)";
+by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1);
+qed "RA4_analz_spies";
(*RA2_analz... and RA4_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 RA2), and of course Fake
messages originate from the Spy. *)
-bind_thm ("RA2_parts_sees_Spy",
- RA2_analz_sees_Spy RS (impOfSubs analz_subset_parts));
-bind_thm ("RA4_parts_sees_Spy",
- RA4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
+bind_thm ("RA2_parts_spies",
+ RA2_analz_spies RS (impOfSubs analz_subset_parts));
+bind_thm ("RA4_parts_spies",
+ RA4_analz_spies RS (impOfSubs analz_subset_parts));
-(*For proving the easier theorems about X ~: parts (sees Spy evs).*)
+(*For proving the easier theorems about X ~: parts (spies evs).*)
fun parts_induct_tac i =
etac recur.induct i THEN
- forward_tac [RA2_parts_sees_Spy] (i+3) THEN
+ forward_tac [RA2_parts_spies] (i+3) THEN
etac subst (i+3) (*RA2: DELETE needless definition of PA!*) THEN
forward_tac [respond_imp_responses] (i+4) THEN
- forward_tac [RA4_parts_sees_Spy] (i+5) THEN
+ forward_tac [RA4_parts_spies] (i+5) THEN
prove_simple_subgoals_tac i;
-(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
+(** 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 lost at start) **)
+(** Spy never sees another agent's shared key! (unless it's bad at start) **)
goal thy
- "!!evs. evs : recur ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
+ "!!evs. evs : recur ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (ALLGOALS
- (asm_simp_tac (!simpset addsimps [parts_insert2, parts_insert_sees])));
+ (asm_simp_tac (!simpset addsimps [parts_insert2, parts_insert_spies])));
(*RA3*)
by (blast_tac (!claset addDs [Key_in_parts_respond]) 2);
(*RA2*)
@@ -159,13 +159,12 @@
Addsimps [Spy_see_shrK];
goal thy
- "!!evs. evs : recur ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
+ "!!evs. evs : recur ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
qed "Spy_analz_shrK";
Addsimps [Spy_analz_shrK];
-goal thy "!!A. [| Key (shrK A) : parts (sees Spy evs); \
-\ evs : recur |] ==> A:lost";
+goal thy "!!A. [| Key (shrK A) : parts (spies evs); evs : recur |] ==> A:bad";
by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
qed "Spy_see_shrK_D";
@@ -186,11 +185,11 @@
goal thy "!!evs. evs : recur ==> \
-\ Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
+\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
by (parts_induct_tac 1);
(*RA3*)
by (best_tac (!claset addDs [Key_in_keysFor_parts]
- addss (!simpset addsimps [parts_insert_sees])) 2);
+ addss (!simpset addsimps [parts_insert_spies])) 2);
(*Fake*)
by (best_tac
(!claset addIs [impOfSubs analz_subset_parts]
@@ -211,17 +210,17 @@
(*** Proofs involving analz ***)
(*For proofs involving analz.*)
-val analz_sees_tac =
+val analz_spies_tac =
etac subst 4 (*RA2: DELETE needless definition of PA!*) THEN
- dtac RA2_analz_sees_Spy 4 THEN
+ dtac RA2_analz_spies 4 THEN
forward_tac [respond_imp_responses] 5 THEN
- dtac RA4_analz_sees_Spy 6;
+ dtac RA4_analz_spies 6;
(** Session keys are not used to encrypt other session keys **)
(*Version for "responses" relation. Handles case RA3 in the theorem below.
- Note that it holds for *any* set H (not just "sees Spy evs")
+ Note that it holds for *any* set H (not just "spies evs")
satisfying the inductive hypothesis.*)
goal thy
"!!evs. [| RB : responses evs; \
@@ -239,10 +238,10 @@
goal thy
"!!evs. evs : recur ==> \
\ ALL K KK. KK <= Compl (range shrK) --> \
-\ (Key K : analz (Key``KK Un (sees Spy evs))) = \
-\ (K : KK | Key K : analz (sees Spy evs))";
+\ (Key K : analz (Key``KK Un (spies evs))) = \
+\ (K : KK | Key K : analz (spies evs))";
by (etac recur.induct 1);
-by analz_sees_tac;
+by analz_spies_tac;
by (REPEAT_FIRST (resolve_tac [allI, impI]));
by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
by (ALLGOALS
@@ -256,11 +255,11 @@
qed_spec_mp "analz_image_freshK";
-(*Instance of the lemma with H replaced by (sees Spy evs):
+(*Instance of the lemma with H replaced by (spies evs):
[| RB : responses evs; evs : recur; |]
==> KK <= Compl (range shrK) -->
- Key K : analz (insert RB (Key``KK Un sees Spy evs)) =
- (K : KK | Key K : analz (insert RB (sees Spy evs)))
+ Key K : analz (insert RB (Key``KK Un spies evs)) =
+ (K : KK | Key K : analz (insert RB (spies evs)))
*)
bind_thm ("resp_analz_image_freshK",
raw_analz_image_freshK RSN
@@ -268,23 +267,23 @@
goal thy
"!!evs. [| evs : recur; KAB ~: range shrK |] ==> \
-\ Key K : analz (insert (Key KAB) (sees Spy evs)) = \
-\ (K = KAB | Key K : analz (sees Spy evs))";
+\ Key K : analz (insert (Key KAB) (spies evs)) = \
+\ (K = KAB | Key K : analz (spies evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
qed "analz_insert_freshK";
(*Everything that's hashed is already in past traffic. *)
-goal thy "!!evs. [| Hash {|Key(shrK A), X|} : parts (sees Spy evs); \
-\ evs : recur; A ~: lost |] \
-\ ==> X : parts (sees Spy evs)";
+goal thy "!!evs. [| Hash {|Key(shrK A), X|} : parts (spies evs); \
+\ evs : recur; A ~: bad |] \
+\ ==> X : parts (spies evs)";
by (etac rev_mp 1);
by (parts_induct_tac 1);
(*RA3 requires a further induction*)
by (etac responses.induct 2);
by (ALLGOALS Asm_simp_tac);
(*Fake*)
-by (simp_tac (!simpset addsimps [parts_insert_sees]) 1);
+by (simp_tac (!simpset addsimps [parts_insert_spies]) 1);
by (Fake_parts_insert_tac 1);
qed "Hash_imp_body";
@@ -296,9 +295,9 @@
**)
goal thy
- "!!evs. [| evs : recur; A ~: lost |] \
+ "!!evs. [| evs : recur; A ~: bad |] \
\ ==> EX B' P'. ALL B P. \
-\ Hash {|Key(shrK A), Agent A, B, NA, P|} : parts (sees Spy evs) \
+\ Hash {|Key(shrK A), Agent A, B, NA, P|} : parts (spies evs) \
\ --> B=B' & P=P'";
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
@@ -309,13 +308,13 @@
by (ALLGOALS (expand_case_tac "NA = ?y"));
by (REPEAT_FIRST (ares_tac [exI]));
by (REPEAT (blast_tac (!claset addSDs [Hash_imp_body]
- addSEs sees_Spy_partsEs) 1));
+ addSEs spies_partsEs) 1));
val lemma = result();
goalw thy [HPair_def]
- "!!A.[| Hash[Key(shrK A)] {|Agent A, B,NA,P|} : parts(sees Spy evs); \
-\ Hash[Key(shrK A)] {|Agent A, B',NA,P'|} : parts(sees Spy evs); \
-\ evs : recur; A ~: lost |] \
+ "!!A.[| Hash[Key(shrK A)] {|Agent A, B,NA,P|} : parts(spies evs); \
+\ Hash[Key(shrK A)] {|Agent A, B',NA,P'|} : parts(spies evs); \
+\ evs : recur; A ~: bad |] \
\ ==> B=B' & P=P'";
by (REPEAT (eresolve_tac partsEs 1));
by (prove_unique_tac lemma 1);
@@ -328,7 +327,7 @@
goal thy
"!!evs. [| RB : responses evs; evs : recur |] \
-\ ==> (Key (shrK B) : analz (insert RB (sees Spy evs))) = (B:lost)";
+\ ==> (Key (shrK B) : analz (insert RB (spies evs))) = (B:bad)";
by (etac responses.induct 1);
by (ALLGOALS
(asm_simp_tac
@@ -417,9 +416,9 @@
goal thy
"!!evs. [| (PB,RB,KAB) : respond evs; evs : recur |] \
-\ ==> ALL A A' N. A ~: lost & A' ~: lost --> \
+\ ==> ALL A A' N. A ~: bad & A' ~: bad --> \
\ Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} --> \
-\ Key K ~: analz (insert RB (sees Spy evs))";
+\ Key K ~: analz (insert RB (spies evs))";
by (etac respond.induct 1);
by (forward_tac [respond_imp_responses] 2);
by (forward_tac [respond_imp_not_used] 2);
@@ -437,7 +436,7 @@
by (Blast_tac 3);
by (blast_tac (!claset addSEs partsEs
addDs [Key_in_parts_respond]) 2);
-(*by unicity, either B=Aa or B=A', a contradiction since B: lost*)
+(*by unicity, either B=Aa or B=A', a contradiction since B: bad*)
by (dtac unique_session_keys 1);
by (etac respond_certificate 1);
by (assume_tac 1);
@@ -446,16 +445,15 @@
goal thy
- "!!evs. [| Crypt (shrK A) {|Key K, Agent A', N|} \
-\ : parts (sees Spy evs); \
-\ A ~: lost; A' ~: lost; evs : recur |] \
-\ ==> Key K ~: analz (sees Spy evs)";
+ "!!evs. [| Crypt (shrK A) {|Key K, Agent A', N|} : parts (spies evs); \
+\ A ~: bad; A' ~: bad; evs : recur |] \
+\ ==> Key K ~: analz (spies evs)";
by (etac rev_mp 1);
by (etac recur.induct 1);
-by analz_sees_tac;
+by analz_spies_tac;
by (ALLGOALS
(asm_simp_tac
- (!simpset addsimps [parts_insert_sees, analz_insert_freshK]
+ (!simpset addsimps [parts_insert_spies, analz_insert_freshK]
setloop split_tac [expand_if])));
(*RA4*)
by (spy_analz_tac 5);
@@ -494,9 +492,8 @@
it can say nothing about how recent A's message is. It might later be
used to prove B's presence to A at the run's conclusion.*)
goalw thy [HPair_def]
- "!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} \
-\ : parts (sees Spy evs); \
-\ A ~: lost; evs : recur |] \
+ "!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} : parts(spies evs); \
+\ A ~: bad; evs : recur |] \
\ ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) : set evs";
by (etac rev_mp 1);
by (parts_induct_tac 1);
@@ -512,8 +509,8 @@
(*Certificates can only originate with the Server.*)
goal thy
- "!!evs. [| Crypt (shrK A) Y : parts (sees Spy evs); \
-\ A ~: lost; A ~= Spy; evs : recur |] \
+ "!!evs. [| Crypt (shrK A) Y : parts (spies evs); \
+\ A ~: bad; A ~= Spy; evs : recur |] \
\ ==> EX C RC. Says Server C RC : set evs & \
\ Crypt (shrK A) Y : parts {RC}";
by (etac rev_mp 1);
@@ -522,7 +519,7 @@
(*RA4*)
by (Blast_tac 4);
(*RA3*)
-by (full_simp_tac (!simpset addsimps [parts_insert_sees]) 3
+by (full_simp_tac (!simpset addsimps [parts_insert_spies]) 3
THEN Blast_tac 3);
(*RA1*)
by (Blast_tac 1);
--- a/src/HOL/Auth/Recur.thy Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/Recur.thy Thu Sep 18 13:24:04 1997 +0200
@@ -57,7 +57,7 @@
(*The spy MAY say anything he CAN say. Common to
all similar protocols.*)
Fake "[| evs: recur; B ~= Spy;
- X: synth (analz (sees Spy evs)) |]
+ X: synth (analz (spies evs)) |]
==> Says Spy B X # evs : recur"
(*Alice initiates a protocol run.
--- a/src/HOL/Auth/Shared.ML Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/Shared.ML Thu Sep 18 13:24:04 1997 +0200
@@ -29,47 +29,48 @@
Addsimps [keysFor_parts_initState];
-(*** Function "sees" ***)
-
-(*Agents see their own shared keys!*)
-goal thy "A ~= Spy --> Key (shrK A) : sees A evs";
-by (induct_tac "evs" 1);
-by (induct_tac "A" 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
-by (Blast_tac 1);
-qed_spec_mp "sees_own_shrK";
+(*** Function "spies" ***)
(*Spy sees shared keys of agents!*)
-goal thy "!!A. A: lost ==> Key (shrK A) : sees Spy evs";
+goal thy "!!A. A: bad ==> Key (shrK A) : spies evs";
by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
-by (Blast_tac 1);
-qed "Spy_sees_lost";
+by (ALLGOALS (asm_simp_tac
+ (!simpset addsimps [imageI, spies_Cons]
+ setloop split_tac [expand_event_case, expand_if])));
+qed "Spy_spies_bad";
-AddSIs [sees_own_shrK, Spy_sees_lost];
+AddSIs [Spy_spies_bad];
-(*For not_lost_tac*)
-goal thy "!!A. [| Crypt (shrK A) X : analz (sees Spy evs); A: lost |] \
-\ ==> X : analz (sees Spy evs)";
+(*For not_bad_tac*)
+goal thy "!!A. [| Crypt (shrK A) X : analz (spies evs); A: bad |] \
+\ ==> X : analz (spies evs)";
by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
-qed "Crypt_Spy_analz_lost";
+qed "Crypt_Spy_analz_bad";
(*Prove that the agent is uncompromised by the confidentiality of
a component of a message she's said.*)
-fun not_lost_tac s =
- case_tac ("(" ^ s ^ ") : lost") THEN'
+fun not_bad_tac s =
+ case_tac ("(" ^ s ^ ") : bad") THEN'
SELECT_GOAL
- (REPEAT_DETERM (dtac (Says_imp_sees_Spy RS analz.Inj) 1) THEN
+ (REPEAT_DETERM (dtac (Says_imp_spies RS analz.Inj) 1) THEN
REPEAT_DETERM (etac MPair_analz 1) THEN
THEN_BEST_FIRST
- (dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN assume_tac 1)
+ (dres_inst_tac [("A", s)] Crypt_Spy_analz_bad 1 THEN assume_tac 1)
(has_fewer_prems 1, size_of_thm)
(Step_tac 1));
(** Fresh keys never clash with long-term shared keys **)
+(*Agents see their own shared keys!*)
+goal thy "Key (shrK A) : initState A";
+by (induct_tac "A" 1);
+by (Auto_tac());
+qed "shrK_in_initState";
+AddIffs [shrK_in_initState];
+
goal thy "Key (shrK A) : used evs";
+br initState_into_used 1;
by (Blast_tac 1);
qed "shrK_in_used";
AddIffs [shrK_in_used];
@@ -97,7 +98,7 @@
AddIffs [Nonce_notin_initState];
goal thy "Nonce N ~: used []";
-by (simp_tac (!simpset addsimps [used_def]) 1);
+by (simp_tac (!simpset addsimps [used_Nil]) 1);
qed "Nonce_notin_used_empty";
Addsimps [Nonce_notin_used_empty];
@@ -105,16 +106,13 @@
(*** Supply fresh nonces for possibility theorems. ***)
(*In any trace, there is an upper bound N on the greatest nonce in use.*)
-goalw thy [used_def] "EX N. ALL n. N<=n --> Nonce n ~: used evs";
+goal thy "EX N. ALL n. N<=n --> Nonce n ~: used evs";
by (induct_tac "evs" 1);
by (res_inst_tac [("x","0")] exI 1);
+by (ALLGOALS (asm_simp_tac
+ (!simpset addsimps [used_Cons]
+ setloop split_tac [expand_event_case, expand_if])));
by (Step_tac 1);
-by (Full_simp_tac 1);
-(*Inductive step*)
-by (induct_tac "a" 1);
-by (ALLGOALS (full_simp_tac
- (!simpset addsimps [UN_parts_sees_Says,
- UN_parts_sees_Notes])));
by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
by (ALLGOALS (blast_tac (!claset addSEs [add_leE])));
val lemma = result();
--- a/src/HOL/Auth/Shared.thy Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/Shared.thy Thu Sep 18 13:24:04 1997 +0200
@@ -21,7 +21,7 @@
(*Server knows all long-term keys; other agents know only their own*)
initState_Server "initState Server = Key `` range shrK"
initState_Friend "initState (Friend i) = {Key (shrK (Friend i))}"
- initState_Spy "initState Spy = Key``shrK``lost"
+ initState_Spy "initState Spy = Key``shrK``bad"
rules
--- a/src/HOL/Auth/TLS.ML Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/TLS.ML Thu Sep 18 13:24:04 1997 +0200
@@ -144,8 +144,8 @@
(*Induction for regularity theorems. If induction formula has the form
- X ~: analz (sees Spy evs) --> ... then it shortens the proof by discarding
- needless information about analz (insert X (sees Spy evs)) *)
+ X ~: analz (spies evs) --> ... then it shortens the proof by discarding
+ needless information about analz (insert X (spies evs)) *)
fun parts_induct_tac i =
etac tls.induct i
THEN
@@ -155,25 +155,25 @@
ALLGOALS (asm_full_simp_tac (!simpset setloop split_tac [expand_if]));
-(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
+(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
sends messages containing X! **)
-(*Spy never sees another agent's private key! (unless it's lost at start)*)
+(*Spy never sees another agent's private key! (unless it's bad at start)*)
goal thy
- "!!evs. evs : tls ==> (Key (priK A) : parts (sees Spy evs)) = (A : lost)";
+ "!!evs. evs : tls ==> (Key (priK A) : parts (spies evs)) = (A : bad)";
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
qed "Spy_see_priK";
Addsimps [Spy_see_priK];
goal thy
- "!!evs. evs : tls ==> (Key (priK A) : analz (sees Spy evs)) = (A : lost)";
+ "!!evs. evs : tls ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
qed "Spy_analz_priK";
Addsimps [Spy_analz_priK];
-goal thy "!!A. [| Key (priK A) : parts (sees Spy evs); \
-\ evs : tls |] ==> A:lost";
+goal thy "!!A. [| Key (priK A) : parts (spies evs); \
+\ evs : tls |] ==> A:bad";
by (blast_tac (!claset addDs [Spy_see_priK]) 1);
qed "Spy_see_priK_D";
@@ -187,7 +187,7 @@
breach of security.*)
goalw thy [certificate_def]
"!!evs. evs : tls \
-\ ==> certificate B KB : parts (sees Spy evs) --> KB = pubK B";
+\ ==> certificate B KB : parts (spies evs) --> KB = pubK B";
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
bind_thm ("Server_cert_pubB", result() RSN (2, rev_mp));
@@ -195,7 +195,7 @@
(*Replace key KB in ClientCertKeyEx by (pubK B) *)
val ClientCertKeyEx_tac =
- forward_tac [Says_imp_sees_Spy RS parts.Inj RS
+ forward_tac [Says_imp_spies RS parts.Inj RS
parts.Snd RS parts.Snd RS parts.Snd RS Server_cert_pubB]
THEN' assume_tac
THEN' hyp_subst_tac;
@@ -220,27 +220,27 @@
(*Every Nonce that's hashed is already in past traffic.
This event occurs in CERTIFICATE VERIFY*)
-goal thy "!!evs. [| Hash {|Nonce NB, X|} : parts (sees Spy evs); \
+goal thy "!!evs. [| Hash {|Nonce NB, X|} : parts (spies evs); \
\ NB ~: range PRF; evs : tls |] \
-\ ==> Nonce NB : parts (sees Spy evs)";
+\ ==> Nonce NB : parts (spies evs)";
by (etac rev_mp 1);
by (etac rev_mp 1);
by (parts_induct_tac 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_spies])));
by (Fake_parts_insert_tac 1);
(*FINISHED messages are trivial because M : range PRF*)
by (REPEAT (Blast_tac 2));
(*CERTIFICATE VERIFY is the only interesting case*)
-by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
+by (blast_tac (!claset addSEs spies_partsEs) 1);
qed "Hash_Nonce_CV";
goal thy "!!evs. [| Notes A {|Agent B, X|} : set evs; evs : tls |] \
-\ ==> Crypt (pubK B) X : parts (sees Spy evs)";
+\ ==> Crypt (pubK B) X : parts (spies evs)";
by (etac rev_mp 1);
by (analz_induct_tac 1);
by (blast_tac (!claset addIs [parts_insertI]) 1);
-qed "Notes_Crypt_parts_sees";
+qed "Notes_Crypt_parts_spies";
(*** Protocol goal: if B receives CERTIFICATE VERIFY, then A sent it ***)
@@ -248,28 +248,28 @@
(*B can check A's signature if he has received A's certificate.
Perhaps B~=Spy is unnecessary, but there's no obvious proof if the first
message is Fake. We don't need guarantees for the Spy anyway. We must
- assume A~:lost; otherwise, the Spy can forge A's signature.*)
+ assume A~:bad; otherwise, the Spy can forge A's signature.*)
goal thy
"!!evs. [| X = Crypt (priK A) \
\ (Hash{|Nonce NB, certificate B KB, Nonce PMS|}); \
-\ evs : tls; A ~: lost; B ~= Spy |] \
+\ evs : tls; A ~: bad; B ~= Spy |] \
\ ==> Says B A {|Nonce NB, Number SID, Number XB, certificate B KB|} \
\ : set evs --> \
-\ X : parts (sees Spy evs) --> Says A B X : set evs";
+\ X : parts (spies evs) --> Says A B X : set evs";
by (hyp_subst_tac 1);
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
(*ServerHello: nonce NB cannot be in X because it's fresh!*)
by (blast_tac (!claset addSDs [Hash_Nonce_CV]
- addSEs sees_Spy_partsEs) 1);
+ addSEs spies_partsEs) 1);
qed_spec_mp "TrustCertVerify";
(*If CERTIFICATE VERIFY is present then A has chosen PMS.*)
goal thy
"!!evs. [| Crypt (priK A) (Hash{|Nonce NB, certificate B KB, Nonce PMS|}) \
-\ : parts (sees Spy evs); \
-\ evs : tls; A ~: lost |] \
+\ : parts (spies evs); \
+\ evs : tls; A ~: bad |] \
\ ==> Notes A {|Agent B, Nonce PMS|} : set evs";
be rev_mp 1;
by (parts_induct_tac 1);
@@ -280,8 +280,8 @@
(*No collection of keys can help the spy get new private keys*)
goal thy
"!!evs. evs : tls ==> \
-\ ALL KK. (Key(priK B) : analz (Key``KK Un (sees Spy evs))) = \
-\ (priK B : KK | B : lost)";
+\ ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) = \
+\ (priK B : KK | B : bad)";
by (etac tls.induct 1);
by (ALLGOALS
(asm_simp_tac (analz_image_keys_ss
@@ -309,14 +309,14 @@
goal thy
"!!evs. evs : tls ==> \
\ ALL KK. KK <= range sessionK --> \
-\ (Nonce N : analz (Key``KK Un (sees Spy evs))) = \
-\ (Nonce N : analz (sees Spy evs))";
+\ (Nonce N : analz (Key``KK Un (spies evs))) = \
+\ (Nonce N : analz (spies evs))";
by (etac tls.induct 1);
by (ClientCertKeyEx_tac 6);
by (REPEAT_FIRST (resolve_tac [allI, impI]));
by (REPEAT_FIRST (rtac lemma));
writeln"SLOW simplification: 55 secs??";
-(*ClientCertKeyEx is to blame, causing case splits for A, B: lost*)
+(*ClientCertKeyEx is to blame, causing case splits for A, B: bad*)
by (ALLGOALS
(asm_simp_tac (analz_image_keys_ss
addsimps [range_sessionkeys_not_priK,
@@ -337,16 +337,16 @@
Addsimps [no_Notes_A_PRF];
-goal thy "!!evs. [| Nonce (PRF (PMS,NA,NB)) : parts (sees Spy evs); \
+goal thy "!!evs. [| Nonce (PRF (PMS,NA,NB)) : parts (spies evs); \
\ evs : tls |] \
-\ ==> Nonce PMS : parts (sees Spy evs)";
+\ ==> Nonce PMS : parts (spies evs)";
by (etac rev_mp 1);
by (parts_induct_tac 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_spies])));
by (Fake_parts_insert_tac 1);
(*Six others, all trivial or by freshness*)
-by (REPEAT (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
- addSEs sees_Spy_partsEs) 1));
+by (REPEAT (blast_tac (!claset addSDs [Notes_Crypt_parts_spies]
+ addSEs spies_partsEs) 1));
qed "MS_imp_PMS";
AddSDs [MS_imp_PMS];
@@ -360,13 +360,13 @@
Converse doesn't hold; betraying M doesn't force the keys to be sent!*)
goal thy
- "!!evs. [| Nonce M ~: analz (sees Spy evs); evs : tls |] \
-\ ==> Key (sessionK(b,NA,NB,M)) ~: parts (sees Spy evs)";
+ "!!evs. [| Nonce M ~: analz (spies evs); evs : tls |] \
+\ ==> Key (sessionK(b,NA,NB,M)) ~: parts (spies evs)";
by (etac rev_mp 1);
by (analz_induct_tac 1);
(*SpyKeys*)
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3);
-by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj]) 3);
+by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj]) 3);
(*Fake*)
by (spy_analz_tac 2);
(*Base*)
@@ -385,17 +385,17 @@
They are NOT suitable as safe elim rules.*)
goal thy
- "!!evs. [| Nonce PMS ~: parts (sees Spy evs); evs : tls |] \
-\ ==> Crypt (sessionK(b, Na, Nb, PRF(PMS,NA,NB))) Y ~: parts (sees Spy evs)";
+ "!!evs. [| Nonce PMS ~: parts (spies evs); evs : tls |] \
+\ ==> Crypt (sessionK(b, Na, Nb, PRF(PMS,NA,NB))) Y ~: parts (spies evs)";
by (etac rev_mp 1);
by (analz_induct_tac 1);
(*Fake*)
-by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 2);
+by (asm_simp_tac (!simpset addsimps [parts_insert_spies]) 2);
by (Fake_parts_insert_tac 2);
(*Base, ClientFinished, ServerFinished: trivial, e.g. by freshness*)
by (REPEAT
- (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
- addSEs sees_Spy_partsEs) 1));
+ (blast_tac (!claset addSDs [Notes_Crypt_parts_spies]
+ addSEs spies_partsEs) 1));
qed "Crypt_sessionK_notin_parts";
Addsimps [Crypt_sessionK_notin_parts];
@@ -415,9 +415,9 @@
(*PMS determines B. Proof borrowed from NS_Public/unique_NA and from Yahalom*)
goal thy
- "!!evs. [| Nonce PMS ~: analz (sees Spy evs); evs : tls |] \
+ "!!evs. [| Nonce PMS ~: analz (spies evs); evs : tls |] \
\ ==> EX B'. ALL B. \
-\ Crypt (pubK B) (Nonce PMS) : parts (sees Spy evs) --> B=B'";
+\ Crypt (pubK B) (Nonce PMS) : parts (spies evs) --> B=B'";
by (etac rev_mp 1);
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
@@ -429,9 +429,9 @@
val lemma = result();
goal thy
- "!!evs. [| Crypt(pubK B) (Nonce PMS) : parts (sees Spy evs); \
-\ Crypt(pubK B') (Nonce PMS) : parts (sees Spy evs); \
-\ Nonce PMS ~: analz (sees Spy evs); \
+ "!!evs. [| Crypt(pubK B) (Nonce PMS) : parts (spies evs); \
+\ Crypt(pubK B') (Nonce PMS) : parts (spies evs); \
+\ Nonce PMS ~: analz (spies evs); \
\ evs : tls |] \
\ ==> B=B'";
by (prove_unique_tac lemma 1);
@@ -440,7 +440,7 @@
(*In A's internal Note, PMS determines A and B.*)
goal thy
- "!!evs. [| Nonce PMS ~: analz (sees Spy evs); evs : tls |] \
+ "!!evs. [| Nonce PMS ~: analz (spies evs); evs : tls |] \
\ ==> EX A' B'. ALL A B. \
\ Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'";
by (etac rev_mp 1);
@@ -448,13 +448,13 @@
by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
(*ClientCertKeyEx: if PMS is fresh, then it can't appear in Notes A X.*)
by (expand_case_tac "PMS = ?y" 1 THEN
- blast_tac (!claset addSDs [Notes_Crypt_parts_sees] addSEs partsEs) 1);
+ blast_tac (!claset addSDs [Notes_Crypt_parts_spies] addSEs partsEs) 1);
val lemma = result();
goal thy
"!!evs. [| Notes A {|Agent B, Nonce PMS|} : set evs; \
\ Notes A' {|Agent B', Nonce PMS|} : set evs; \
-\ Nonce PMS ~: analz (sees Spy evs); \
+\ Nonce PMS ~: analz (spies evs); \
\ evs : tls |] \
\ ==> A=A' & B=B'";
by (prove_unique_tac lemma 1);
@@ -464,20 +464,20 @@
(*If A sends ClientCertKeyEx to an honest B, then the PMS will stay secret.*)
goal thy
- "!!evs. [| evs : tls; A ~: lost; B ~: lost |] \
+ "!!evs. [| evs : tls; A ~: bad; B ~: bad |] \
\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
-\ Nonce PMS ~: analz (sees Spy evs)";
+\ Nonce PMS ~: analz (spies evs)";
by (analz_induct_tac 1); (*30 seconds???*)
(*ClientAccepts and ServerAccepts: because PMS ~: range PRF*)
by (REPEAT (fast_tac (!claset addss (!simpset)) 6));
(*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
by (REPEAT (blast_tac (!claset addSEs partsEs
- addDs [Notes_Crypt_parts_sees,
+ addDs [Notes_Crypt_parts_spies,
impOfSubs analz_subset_parts,
- Says_imp_sees_Spy RS analz.Inj]) 4));
+ Says_imp_spies RS analz.Inj]) 4));
(*ClientHello*)
-by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
- addSEs sees_Spy_partsEs) 3);
+by (blast_tac (!claset addSDs [Notes_Crypt_parts_spies]
+ addSEs spies_partsEs) 3);
(*SpyKeys*)
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
by (fast_tac (!claset addss (!simpset)) 2);
@@ -492,27 +492,27 @@
(*If A sends ClientCertKeyEx to an honest B, then the MASTER SECRET
will stay secret.*)
goal thy
- "!!evs. [| evs : tls; A ~: lost; B ~: lost |] \
+ "!!evs. [| evs : tls; A ~: bad; B ~: bad |] \
\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
-\ Nonce (PRF(PMS,NA,NB)) ~: analz (sees Spy evs)";
+\ Nonce (PRF(PMS,NA,NB)) ~: analz (spies evs)";
by (analz_induct_tac 1); (*35 seconds*)
(*ClientAccepts and ServerAccepts: because PMS was already visible*)
by (REPEAT (blast_tac (!claset addDs [Spy_not_see_PMS,
- Says_imp_sees_Spy RS analz.Inj,
- Notes_imp_sees_Spy RS analz.Inj]) 6));
+ Says_imp_spies RS analz.Inj,
+ Notes_imp_spies RS analz.Inj]) 6));
(*ClientHello*)
by (Blast_tac 3);
(*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
by (blast_tac (!claset addSDs [Spy_not_see_PMS,
- Says_imp_sees_Spy RS analz.Inj]) 2);
+ Says_imp_spies RS analz.Inj]) 2);
(*Fake*)
by (spy_analz_tac 1);
(*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
by (REPEAT (blast_tac (!claset addSEs partsEs
- addDs [Notes_Crypt_parts_sees,
+ addDs [Notes_Crypt_parts_spies,
impOfSubs analz_subset_parts,
- Says_imp_sees_Spy RS analz.Inj]) 1));
+ Says_imp_spies RS analz.Inj]) 1));
bind_thm ("Spy_not_see_MS", result() RSN (2, rev_mp));
@@ -528,16 +528,16 @@
\ Nonce NA, Number XA, Agent A, \
\ Nonce NB, Number XB, Agent B|}); \
\ M = PRF(PMS,NA,NB); \
-\ evs : tls; A ~: lost; B ~: lost |] \
+\ evs : tls; A ~: bad; B ~: bad |] \
\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
-\ X : parts (sees Spy evs) --> Says B A X : set evs";
+\ X : parts (spies evs) --> Says B A X : set evs";
by (hyp_subst_tac 1);
by (analz_induct_tac 1); (*16 seconds*)
(*ClientCertKeyEx*)
by (Blast_tac 2);
(*Fake: the Spy doesn't have the critical session key!*)
by (REPEAT (rtac impI 1));
-by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(sees Spy evsa)" 1);
+by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS,
not_parts_not_analz]) 2);
by (Fake_parts_insert_tac 1);
@@ -550,10 +550,10 @@
that B sends his message to A. If CLIENT KEY EXCHANGE were augmented
to bind A's identity with M, then we could replace A' by A below.*)
goal thy
- "!!evs. [| evs : tls; A ~: lost; B ~: lost; \
+ "!!evs. [| evs : tls; A ~: bad; B ~: bad; \
\ M = PRF(PMS,NA,NB) |] \
\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
-\ Crypt (serverK(Na,Nb,M)) Y : parts (sees Spy evs) --> \
+\ Crypt (serverK(Na,Nb,M)) Y : parts (spies evs) --> \
\ (EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs)";
by (hyp_subst_tac 1);
by (analz_induct_tac 1); (*12 seconds*)
@@ -561,7 +561,7 @@
(*ClientCertKeyEx*)
by (Blast_tac 2);
(*Fake: the Spy doesn't have the critical session key!*)
-by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(sees Spy evsa)" 1);
+by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS,
not_parts_not_analz]) 2);
by (Fake_parts_insert_tac 1);
@@ -570,11 +570,11 @@
(*...otherwise delete induction hyp and use unicity of PMS.*)
by (thin_tac "?PP-->?QQ" 1);
by (Step_tac 1);
-by (subgoal_tac "Nonce PMS ~: analz(sees Spy evsSF)" 1);
+by (subgoal_tac "Nonce PMS ~: analz(spies evsSF)" 1);
by (asm_simp_tac (!simpset addsimps [Spy_not_see_PMS]) 2);
by (blast_tac (!claset addSEs [MPair_parts]
- addDs [Notes_Crypt_parts_sees,
- Says_imp_sees_Spy RS parts.Inj,
+ addDs [Notes_Crypt_parts_spies,
+ Says_imp_spies RS parts.Inj,
unique_PMS]) 1);
qed_spec_mp "TrustServerMsg";
@@ -585,22 +585,22 @@
CLIENT FINISHED, then B can then check the quoted values XA, XB, etc.
***)
goal thy
- "!!evs. [| evs : tls; A ~: lost; B ~: lost |] \
+ "!!evs. [| evs : tls; A ~: bad; B ~: bad |] \
\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
-\ Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (sees Spy evs) --> \
+\ Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (spies evs) --> \
\ Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
by (analz_induct_tac 1); (*13 seconds*)
by (REPEAT_FIRST (rtac impI));
(*ClientCertKeyEx*)
by (Blast_tac 2);
(*Fake: the Spy doesn't have the critical session key!*)
-by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(sees Spy evsa)" 1);
+by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS,
not_parts_not_analz]) 2);
by (Fake_parts_insert_tac 1);
(*ClientFinished. If the message is old then apply induction hypothesis...*)
by (step_tac (!claset delrules [conjI]) 1);
-by (subgoal_tac "Nonce PMS ~: analz (sees Spy evsCF)" 1);
+by (subgoal_tac "Nonce PMS ~: analz (spies evsCF)" 1);
by (asm_simp_tac (!simpset addsimps [Spy_not_see_PMS]) 2);
by (blast_tac (!claset addSEs [MPair_parts]
addDs [Notes_unique_PMS]) 1);
@@ -618,8 +618,8 @@
\ Says A'' B (Crypt (priK A) \
\ (Hash{|Nonce NB, certificate B KB, Nonce PMS|})) \
\ : set evs; \
-\ evs : tls; A ~: lost; B ~: lost |] \
+\ evs : tls; A ~: bad; B ~: bad |] \
\ ==> Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
by (blast_tac (!claset addSIs [TrustClientMsg, UseCertVerify]
- addDs [Says_imp_sees_Spy RS parts.Inj]) 1);
+ addDs [Says_imp_spies RS parts.Inj]) 1);
qed "AuthClientFinished";
--- a/src/HOL/Auth/TLS.thy Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/TLS.thy Thu Sep 18 13:24:04 1997 +0200
@@ -83,7 +83,7 @@
Fake (*The spy, an active attacker, MAY say anything he CAN say.*)
"[| evs: tls; B ~= Spy;
- X: synth (analz (sees Spy evs)) |]
+ X: synth (analz (spies evs)) |]
==> Says Spy B X # evs : tls"
SpyKeys (*The spy may apply PRF, clientK & serverK to available nonces*)
--- a/src/HOL/Auth/WooLam.ML Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/WooLam.ML Thu Sep 18 13:24:04 1997 +0200
@@ -41,39 +41,39 @@
(** For reasoning about the encrypted portion of messages **)
-goal thy "!!evs. Says A' B X : set evs ==> X : analz (sees Spy evs)";
-by (etac (Says_imp_sees_Spy RS analz.Inj) 1);
-qed "WL4_analz_sees_Spy";
+goal thy "!!evs. Says A' B X : set evs ==> X : analz (spies evs)";
+by (etac (Says_imp_spies RS analz.Inj) 1);
+qed "WL4_analz_spies";
-bind_thm ("WL4_parts_sees_Spy",
- WL4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
+bind_thm ("WL4_parts_spies",
+ WL4_analz_spies RS (impOfSubs analz_subset_parts));
-(*For proving the easier theorems about X ~: parts (sees Spy evs) *)
+(*For proving the easier theorems about X ~: parts (spies evs) *)
fun parts_induct_tac i =
etac woolam.induct i THEN
- forward_tac [WL4_parts_sees_Spy] (i+5) THEN
+ forward_tac [WL4_parts_spies] (i+5) THEN
prove_simple_subgoals_tac 1;
-(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
+(** 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 lost at start)*)
+(*Spy never sees another agent's shared key! (unless it's bad at start)*)
goal thy
- "!!evs. evs : woolam ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
+ "!!evs. evs : woolam ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
goal thy
- "!!evs. evs : woolam ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
+ "!!evs. evs : woolam ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
qed "Spy_analz_shrK";
Addsimps [Spy_analz_shrK];
-goal thy "!!A. [| Key (shrK A) : parts (sees Spy evs); \
-\ evs : woolam |] ==> A:lost";
+goal thy "!!A. [| Key (shrK A) : parts (spies evs); \
+\ evs : woolam |] ==> A:bad";
by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
qed "Spy_see_shrK_D";
@@ -88,8 +88,8 @@
(*If the encrypted message appears then it originated with Alice*)
goal thy
- "!!evs. [| A ~: lost; evs : woolam |] \
-\ ==> Crypt (shrK A) (Nonce NB) : parts (sees Spy evs) \
+ "!!evs. [| A ~: bad; evs : woolam |] \
+\ ==> Crypt (shrK A) (Nonce NB) : parts (spies evs) \
\ --> (EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs)";
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
@@ -100,13 +100,13 @@
Alice, then she originated that certificate. But we DO NOT know that B
ever saw it: the Spy may have rerouted the message to the Server.*)
goal thy
- "!!evs. [| A ~: lost; evs : woolam; \
+ "!!evs. [| A ~: bad; evs : woolam; \
\ Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \
\ : set evs |] \
\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
by (blast_tac (!claset addSIs [NB_Crypt_imp_Alice_msg]
addSEs [MPair_parts]
- addDs [Says_imp_sees_Spy RS parts.Inj]) 1);
+ addDs [Says_imp_spies RS parts.Inj]) 1);
qed "Server_trusts_WL4";
@@ -126,8 +126,8 @@
(*If the encrypted message appears then it originated with the Server!*)
goal thy
- "!!evs. [| B ~: lost; evs : woolam |] \
-\ ==> Crypt (shrK B) {|Agent A, NB|} : parts (sees Spy evs) \
+ "!!evs. [| B ~: bad; evs : woolam |] \
+\ ==> Crypt (shrK B) {|Agent A, NB|} : parts (spies evs) \
\ --> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs";
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
@@ -137,10 +137,10 @@
sent the same message.*)
goal thy
"!!evs. [| Says S B (Crypt (shrK B) {|Agent A, NB|}) : set evs; \
-\ B ~: lost; evs : woolam |] \
+\ B ~: bad; evs : woolam |] \
\ ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs";
by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
- addDs [Says_imp_sees_Spy RS parts.Inj]) 1);
+ addDs [Says_imp_spies RS parts.Inj]) 1);
qed "B_got_WL5";
(*Guarantee for B. If B gets the Server's certificate then A has encrypted
@@ -149,7 +149,7 @@
the Server via the Spy.*)
goal thy
"!!evs. [| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set evs; \
-\ A ~: lost; B ~: lost; evs : woolam |] \
+\ A ~: bad; B ~: bad; evs : woolam |] \
\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
by (blast_tac (!claset addIs [Server_trusts_WL4]
addSDs [B_got_WL5 RS Server_sent_WL5]) 1);
@@ -169,8 +169,8 @@
(**CANNOT be proved because A doesn't know where challenges come from...
goal thy
- "!!evs. [| A ~: lost; B ~= Spy; evs : woolam |] \
-\ ==> Crypt (shrK A) (Nonce NB) : parts (sees Spy evs) & \
+ "!!evs. [| A ~: bad; B ~= Spy; evs : woolam |] \
+\ ==> Crypt (shrK A) (Nonce NB) : parts (spies evs) & \
\ Says B A (Nonce NB) : set evs \
\ --> Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
by (parts_induct_tac 1);
--- a/src/HOL/Auth/WooLam.thy Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/WooLam.thy Thu Sep 18 13:24:04 1997 +0200
@@ -26,7 +26,7 @@
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
Fake "[| evs: woolam; B ~= Spy;
- X: synth (analz (sees Spy evs)) |]
+ X: synth (analz (spies evs)) |]
==> Says Spy B X # evs : woolam"
(*Alice initiates a protocol run*)
@@ -49,7 +49,7 @@
(*Bob forwards Alice's response to the Server. NOTE: usually
the messages are shown in chronological order, for clarity.
But here, exchanging the two events would cause the lemma
- WL4_analz_sees_Spy to pick up the wrong assumption!*)
+ WL4_analz_spies to pick up the wrong assumption!*)
WL4 "[| evs4: woolam; B ~= Server;
Says A' B X : set evs4;
Says A'' B (Agent A) : set evs4 |]
--- a/src/HOL/Auth/Yahalom.ML Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/Yahalom.ML Thu Sep 18 13:24:04 1997 +0200
@@ -44,42 +44,42 @@
(*Lets us treat YM4 using a similar argument as for the Fake case.*)
goal thy "!!evs. Says S A {|Crypt (shrK A) Y, X|} : set evs ==> \
-\ X : analz (sees Spy evs)";
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
-qed "YM4_analz_sees_Spy";
+\ X : analz (spies evs)";
+by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1);
+qed "YM4_analz_spies";
-bind_thm ("YM4_parts_sees_Spy",
- YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
+bind_thm ("YM4_parts_spies",
+ YM4_analz_spies RS (impOfSubs analz_subset_parts));
(*Relates to both YM4 and Oops*)
goal thy "!!evs. Says S A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} : set evs ==> \
-\ K : parts (sees Spy evs)";
+\ K : parts (spies evs)";
by (blast_tac (!claset addSEs partsEs
- addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
-qed "YM4_Key_parts_sees_Spy";
+ addSDs [Says_imp_spies RS parts.Inj]) 1);
+qed "YM4_Key_parts_spies";
-(*For proving the easier theorems about X ~: parts (sees Spy evs).*)
-fun parts_sees_tac i =
- forward_tac [YM4_Key_parts_sees_Spy] (i+6) THEN
- forward_tac [YM4_parts_sees_Spy] (i+5) THEN
+(*For proving the easier theorems about X ~: parts (spies evs).*)
+fun parts_spies_tac i =
+ forward_tac [YM4_Key_parts_spies] (i+6) THEN
+ forward_tac [YM4_parts_spies] (i+5) THEN
prove_simple_subgoals_tac i;
(*Induction for regularity theorems. If induction formula has the form
- X ~: analz (sees Spy evs) --> ... then it shortens the proof by discarding
- needless information about analz (insert X (sees Spy evs)) *)
+ X ~: analz (spies evs) --> ... then it shortens the proof by discarding
+ needless information about analz (insert X (spies evs)) *)
fun parts_induct_tac i =
etac yahalom.induct i
THEN
REPEAT (FIRSTGOAL analz_mono_contra_tac)
- THEN parts_sees_tac i;
+ THEN parts_spies_tac i;
-(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
+(** 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 lost at start)*)
+(*Spy never sees another agent's shared key! (unless it's bad at start)*)
goal thy
- "!!evs. evs : yahalom ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
+ "!!evs. evs : yahalom ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (Blast_tac 1);
@@ -87,13 +87,13 @@
Addsimps [Spy_see_shrK];
goal thy
- "!!evs. evs : yahalom ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
+ "!!evs. evs : yahalom ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
qed "Spy_analz_shrK";
Addsimps [Spy_analz_shrK];
-goal thy "!!A. [| Key (shrK A) : parts (sees Spy evs); \
-\ evs : yahalom |] ==> A:lost";
+goal thy "!!A. [| Key (shrK A) : parts (spies evs); \
+\ evs : yahalom |] ==> A:bad";
by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
qed "Spy_see_shrK_D";
@@ -103,10 +103,10 @@
(*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*)
goal thy "!!evs. evs : yahalom ==> \
-\ Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
+\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
by (parts_induct_tac 1);
(*YM4: Key K is not fresh!*)
-by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
+by (blast_tac (!claset addSEs spies_partsEs) 3);
(*YM3*)
by (Blast_tac 2);
(*Fake*)
@@ -139,8 +139,8 @@
(*For proofs involving analz.*)
-val analz_sees_tac =
- forward_tac [YM4_analz_sees_Spy] 6 THEN
+val analz_spies_tac =
+ forward_tac [YM4_analz_spies] 6 THEN
forward_tac [Says_Server_message_form] 7 THEN
assume_tac 7 THEN REPEAT ((etac exE ORELSE' hyp_subst_tac) 7);
@@ -148,8 +148,8 @@
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
- Key K : analz (sees Spy evs)
+ Key K : analz (insert (Key KAB) (spies evs)) ==>
+ Key K : analz (spies evs)
A more general formula must be proved inductively.
****)
@@ -159,10 +159,10 @@
goal thy
"!!evs. evs : yahalom ==> \
\ ALL K KK. KK <= Compl (range shrK) --> \
-\ (Key K : analz (Key``KK Un (sees Spy evs))) = \
-\ (K : KK | Key K : analz (sees Spy evs))";
+\ (Key K : analz (Key``KK Un (spies evs))) = \
+\ (K : KK | Key K : analz (spies evs))";
by (etac yahalom.induct 1);
-by analz_sees_tac;
+by analz_spies_tac;
by (REPEAT_FIRST (resolve_tac [allI, impI]));
by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
@@ -174,8 +174,8 @@
goal thy
"!!evs. [| evs : yahalom; KAB ~: range shrK |] ==> \
-\ Key K : analz (insert (Key KAB) (sees Spy evs)) = \
-\ (K = KAB | Key K : analz (sees Spy evs))";
+\ Key K : analz (insert (Key KAB) (spies evs)) = \
+\ (K = KAB | Key K : analz (spies evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
qed "analz_insert_freshK";
@@ -197,17 +197,15 @@
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 sees_Spy_partsEs
+by (blast_tac (!claset addSEs spies_partsEs
delrules [conjI] (*no split-up to 4 subgoals*)) 1);
val lemma = result();
goal thy
-"!!evs. [| Says Server A \
-\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \
-\ : set evs; \
-\ Says Server A' \
-\ {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} \
-\ : set evs; \
+"!!evs. [| Says Server A \
+\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} : set evs; \
+\ Says Server A' \
+\ {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} : set evs; \
\ evs : yahalom |] \
\ ==> A=A' & B=B' & na=na' & nb=nb'";
by (prove_unique_tac lemma 1);
@@ -217,15 +215,15 @@
(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
goal thy
- "!!evs. [| A ~: lost; B ~: lost; 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 --> \
-\ Key K ~: analz (sees Spy evs)";
+\ Key K ~: analz (spies evs)";
by (etac yahalom.induct 1);
-by analz_sees_tac;
+by analz_spies_tac;
by (ALLGOALS
(asm_simp_tac
(!simpset addsimps [analz_insert_eq, analz_insert_freshK]
@@ -234,7 +232,7 @@
by (blast_tac (!claset addDs [unique_session_keys]) 3);
(*YM3*)
by (blast_tac (!claset delrules [impCE]
- addSEs sees_Spy_partsEs
+ addSEs spies_partsEs
addIs [impOfSubs analz_subset_parts]) 2);
(*Fake*)
by (spy_analz_tac 1);
@@ -248,8 +246,8 @@
\ Crypt (shrK B) {|Agent A, Key K|}|} \
\ : set evs; \
\ Says A Spy {|na, nb, Key K|} ~: set evs; \
-\ A ~: lost; B ~: lost; evs : yahalom |] \
-\ ==> Key K ~: analz (sees Spy 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);
qed "Spy_not_see_encrypted_key";
@@ -259,9 +257,8 @@
(*If the encrypted message appears then it originated with the Server*)
goal thy
- "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na, nb|} \
-\ : parts (sees Spy evs); \
-\ A ~: lost; evs : yahalom |] \
+ "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na, nb|} : parts (spies evs); \
+\ A ~: bad; evs : yahalom |] \
\ ==> Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \
\ Crypt (shrK B) {|Agent A, Key K|}|} \
@@ -277,8 +274,8 @@
(*B knows, by the first part of A's message, that the Server distributed
the key for A and B. But this part says nothing about nonces.*)
goal thy
- "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (sees Spy evs); \
-\ B ~: lost; evs : yahalom |] \
+ "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (spies evs); \
+\ B ~: bad; evs : yahalom |] \
\ ==> EX NA NB. Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, \
\ Nonce NA, Nonce NB|}, \
@@ -296,8 +293,8 @@
Secrecy of NB is crucial.*)
goal thy
"!!evs. evs : yahalom \
-\ ==> Nonce NB ~: analz (sees Spy evs) --> \
-\ Crypt K (Nonce NB) : parts (sees Spy evs) --> \
+\ ==> Nonce NB ~: analz (spies evs) --> \
+\ Crypt K (Nonce NB) : parts (spies evs) --> \
\ (EX A B NA. Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, \
\ Nonce NA, Nonce NB|}, \
@@ -310,9 +307,9 @@
(*YM4*)
by (Step_tac 1);
(*A is uncompromised because NB is secure*)
-by (not_lost_tac "A" 1);
+by (not_bad_tac "A" 1);
(*A's certificate guarantees the existence of the Server message*)
-by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS
+by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS
A_trusts_YM3]) 1);
bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp));
@@ -342,7 +339,7 @@
(with respect to a given trace). *)
goalw thy [KeyWithNonce_def]
"!!evs. Key K ~: used evs ==> ~ KeyWithNonce K NB evs";
-by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
+by (blast_tac (!claset addSEs spies_partsEs) 1);
qed "fresh_not_KeyWithNonce";
(*The Server message associates K with NB' and therefore not with any
@@ -374,10 +371,10 @@
"!!evs. evs : yahalom ==> \
\ (ALL KK. KK <= Compl (range shrK) --> \
\ (ALL K: KK. ~ KeyWithNonce K NB evs) --> \
-\ (Nonce NB : analz (Key``KK Un (sees Spy evs))) = \
-\ (Nonce NB : analz (sees Spy evs)))";
+\ (Nonce NB : analz (Key``KK Un (spies evs))) = \
+\ (Nonce NB : analz (spies evs)))";
by (etac yahalom.induct 1);
-by analz_sees_tac;
+by analz_spies_tac;
by (REPEAT_FIRST (resolve_tac [impI RS allI]));
by (REPEAT_FIRST (rtac lemma));
(*For Oops, simplification proves NBa~=NB. By Says_Server_KeyWithNonce,
@@ -395,8 +392,8 @@
(*Fake*)
by (spy_analz_tac 1);
(*YM4*) (** LEVEL 7 **)
-by (not_lost_tac "A" 1);
-by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
+by (not_bad_tac "A" 1);
+by (dtac (Says_imp_spies RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
THEN REPEAT (assume_tac 1));
by (blast_tac (!claset addIs [KeyWithNonceI]) 1);
qed_spec_mp "Nonce_secrecy";
@@ -410,8 +407,8 @@
\ {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|} \
\ : set evs; \
\ NB ~= NB'; KAB ~: range shrK; evs : yahalom |] \
-\ ==> (Nonce NB : analz (insert (Key KAB) (sees Spy evs))) = \
-\ (Nonce NB : analz (sees Spy evs))";
+\ ==> (Nonce NB : analz (insert (Key KAB) (spies evs))) = \
+\ (Nonce NB : analz (spies evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps
[Nonce_secrecy, Says_Server_KeyWithNonce]) 1);
qed "single_Nonce_secrecy";
@@ -422,8 +419,8 @@
goal thy
"!!evs. evs : yahalom ==> \
\ EX NA' A' B'. ALL NA A B. \
-\ Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts(sees Spy evs) \
-\ --> B ~: lost --> NA = NA' & A = A' & B = B'";
+\ Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts(spies evs) \
+\ --> B ~: bad --> NA = NA' & A = A' & B = B'";
by (parts_induct_tac 1);
(*Fake*)
by (REPEAT (etac (exI RSN (2,exE)) 1) (*stripping EXs makes proof faster*)
@@ -432,31 +429,29 @@
(*YM2: creation of new Nonce. Move assertion into global context*)
by (expand_case_tac "nb = ?y" 1);
by (REPEAT (resolve_tac [exI, conjI, impI, refl] 1));
-by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
+by (blast_tac (!claset addSEs spies_partsEs) 1);
val lemma = result();
goal thy
- "!!evs.[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} \
-\ : parts (sees Spy evs); \
-\ Crypt (shrK B') {|Agent A', Nonce NA', nb|} \
-\ : parts (sees Spy evs); \
-\ evs : yahalom; B ~: lost; B' ~: lost |] \
+ "!!evs.[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts (spies evs); \
+\ Crypt (shrK B') {|Agent A', Nonce NA', nb|} : parts (spies evs); \
+\ evs : yahalom; B ~: bad; B' ~: bad |] \
\ ==> NA' = NA & A' = A & B' = B";
by (prove_unique_tac lemma 1);
qed "unique_NB";
(*Variant useful for proving secrecy of NB: the Says... form allows
- not_lost_tac to remove the assumption B' ~: lost.*)
+ not_bad_tac to remove the assumption B' ~: bad.*)
goal thy
"!!evs.[| Says C D {|X, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
-\ : set evs; B ~: lost; \
+\ : set evs; B ~: bad; \
\ Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|} \
\ : set evs; \
-\ nb ~: analz (sees Spy evs); evs : yahalom |] \
+\ nb ~: analz (spies evs); evs : yahalom |] \
\ ==> NA' = NA & A' = A & B' = B";
-by (not_lost_tac "B'" 1);
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
+by (not_bad_tac "B'" 1);
+by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj]
addSEs [MPair_parts]
addDs [unique_NB]) 1);
qed "Says_unique_NB";
@@ -465,15 +460,13 @@
(** A nonce value is never used both as NA and as NB **)
goal thy
- "!!evs. [| B ~: lost; evs : yahalom |] \
-\ ==> Nonce NB ~: analz (sees Spy evs) --> \
-\ Crypt (shrK B') {|Agent A', Nonce NB, nb'|} \
-\ : parts(sees Spy evs) \
-\ --> Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} \
-\ ~: parts(sees Spy evs)";
+ "!!evs. [| B ~: bad; evs : yahalom |] \
+\ ==> Nonce NB ~: analz (spies evs) --> \
+\ Crypt (shrK B') {|Agent A', Nonce NB, nb'|} : parts(spies evs) --> \
+\ Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} ~: parts(spies evs)";
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
-by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj]
+by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj]
addSIs [parts_insertI]
addSEs partsEs) 1);
bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE));
@@ -495,37 +488,37 @@
(*A vital theorem for B, that nonce NB remains secure from the Spy.*)
goal thy
- "!!evs. [| A ~: lost; B ~: lost; evs : yahalom |] \
+ "!!evs. [| A ~: bad; B ~: bad; evs : yahalom |] \
\ ==> 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) --> \
-\ Nonce NB ~: analz (sees Spy evs)";
+\ Nonce NB ~: analz (spies evs)";
by (etac yahalom.induct 1);
-by analz_sees_tac;
+by analz_spies_tac;
by (ALLGOALS
(asm_simp_tac
(!simpset addsimps [analz_insert_eq, analz_insert_freshK]
setloop split_tac [expand_if])));
(*Prove YM3 by showing that no NB can also be an NA*)
-by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj]
+by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj]
addSEs [MPair_parts]
addDs [no_nonce_YM1_YM2, Says_unique_NB]) 4
THEN flexflex_tac);
(*YM2: similar freshness reasoning*)
by (blast_tac (!claset addSEs partsEs
- addDs [Says_imp_sees_Spy RS analz.Inj,
+ addDs [Says_imp_spies RS analz.Inj,
impOfSubs analz_subset_parts]) 3);
(*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*)
by (blast_tac (!claset addSIs [parts_insertI]
- addSEs sees_Spy_partsEs) 2);
+ addSEs spies_partsEs) 2);
(*Fake*)
by (spy_analz_tac 1);
(** LEVEL 7: YM4 and Oops remain **)
(*YM4: key K is visible to Spy, contradicting session key secrecy theorem*)
by (REPEAT (Safe_step_tac 1));
-by (not_lost_tac "Aa" 1);
-by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
+by (not_bad_tac "Aa" 1);
+by (dtac (Says_imp_spies RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
by (forward_tac [Says_Server_message_form] 3);
by (forward_tac [Says_Server_imp_YM2] 4);
by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, exE, disjE]));
@@ -544,7 +537,7 @@
(*case NB ~= NBa*)
by (asm_simp_tac (!simpset addsimps [single_Nonce_secrecy]) 1);
by (blast_tac (!claset addSEs [MPair_parts]
- addDs [Says_imp_sees_Spy RS parts.Inj,
+ addDs [Says_imp_spies RS parts.Inj,
no_nonce_YM1_YM2 (*to prove NB~=NAa*) ]) 1);
bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp));
@@ -561,14 +554,14 @@
\ 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; \
-\ A ~: lost; B ~: lost; evs : yahalom |] \
+\ A ~: bad; B ~: bad; evs : yahalom |] \
\ ==> Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, \
\ Nonce NA, Nonce NB|}, \
\ Crypt (shrK B) {|Agent A, Key K|}|} \
\ : set evs";
by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
-by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1 THEN
+by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1 THEN
dtac B_trusts_YM4_shrK 1);
by (dtac B_trusts_YM4_newK 3);
by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
@@ -584,9 +577,8 @@
(*The encryption in message YM2 tells us it cannot be faked.*)
goal thy
"!!evs. evs : yahalom \
-\ ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|} \
-\ : parts (sees Spy evs) --> \
-\ B ~: lost --> \
+\ ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts (spies evs) --> \
+\ B ~: bad --> \
\ Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
\ : set evs";
by (parts_induct_tac 1);
@@ -598,7 +590,7 @@
"!!evs. evs : yahalom \
\ ==> Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
\ : set evs --> \
-\ B ~: lost --> \
+\ B ~: bad --> \
\ Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
\ : set evs";
by (etac yahalom.induct 1);
@@ -606,7 +598,7 @@
(*YM4*)
by (Blast_tac 2);
(*YM3*)
-by (best_tac (!claset addSDs [B_Said_YM2, Says_imp_sees_Spy RS parts.Inj]
+by (best_tac (!claset addSDs [B_Said_YM2, Says_imp_spies RS parts.Inj]
addSEs [MPair_parts]) 1);
val lemma = result() RSN (2, rev_mp) RS mp |> standard;
@@ -614,11 +606,11 @@
goal thy
"!!evs. [| Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
\ : set evs; \
-\ A ~: lost; B ~: lost; evs : yahalom |] \
+\ A ~: bad; B ~: bad; evs : yahalom |] \
\ ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
\ : set evs";
by (blast_tac (!claset addSDs [A_trusts_YM3, lemma]
- addEs sees_Spy_partsEs) 1);
+ addEs spies_partsEs) 1);
qed "YM3_auth_B_to_A";
@@ -629,12 +621,11 @@
NB matters for freshness.*)
goal thy
"!!evs. evs : yahalom \
-\ ==> Key K ~: analz (sees Spy evs) --> \
-\ Crypt K (Nonce NB) : parts (sees Spy evs) --> \
-\ Crypt (shrK B) {|Agent A, Key K|} \
-\ : parts (sees Spy evs) --> \
-\ B ~: lost --> \
-\ (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
+\ ==> Key K ~: analz (spies evs) --> \
+\ Crypt K (Nonce NB) : parts (spies evs) --> \
+\ Crypt (shrK B) {|Agent A, Key K|} : parts (spies evs) --> \
+\ B ~: bad --> \
+\ (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
by (parts_induct_tac 1);
(*Fake*)
by (Fake_parts_insert_tac 1);
@@ -643,10 +634,10 @@
(*YM4: was Crypt K (Nonce NB) the very last message? If not, use ind. hyp.*)
by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
(*yes: apply unicity of session keys*)
-by (not_lost_tac "Aa" 1);
+by (not_bad_tac "Aa" 1);
by (blast_tac (!claset addSEs [MPair_parts]
addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
- addDs [Says_imp_sees_Spy RS parts.Inj,
+ addDs [Says_imp_spies RS parts.Inj,
unique_session_keys]) 1);
val lemma = normalize_thm [RSspec, RSmp] (result()) |> standard;
@@ -660,14 +651,14 @@
\ 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); \
-\ A ~: lost; B ~: lost; evs : yahalom |] \
+\ A ~: bad; B ~: bad; evs : yahalom |] \
\ ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
by (dtac B_trusts_YM4 1);
by (REPEAT_FIRST (eresolve_tac [asm_rl, spec]));
-by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1);
+by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1);
by (rtac lemma 1);
by (rtac Spy_not_see_encrypted_key 2);
by (REPEAT_FIRST assume_tac);
by (blast_tac (!claset addSEs [MPair_parts]
- addDs [Says_imp_sees_Spy RS parts.Inj]) 1);
+ addDs [Says_imp_spies RS parts.Inj]) 1);
qed_spec_mp "YM4_imp_A_Said_YM3";
--- a/src/HOL/Auth/Yahalom.thy Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/Yahalom.thy Thu Sep 18 13:24:04 1997 +0200
@@ -22,7 +22,7 @@
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
Fake "[| evs: yahalom; B ~= Spy;
- X: synth (analz (sees Spy evs)) |]
+ X: synth (analz (spies evs)) |]
==> Says Spy B X # evs : yahalom"
(*Alice initiates a protocol run*)
--- a/src/HOL/Auth/Yahalom2.ML Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/Yahalom2.ML Thu Sep 18 13:24:04 1997 +0200
@@ -44,42 +44,42 @@
(*Lets us treat YM4 using a similar argument as for the Fake case.*)
goal thy "!!evs. Says S A {|NB, Crypt (shrK A) Y, X|} : set evs ==> \
-\ X : analz (sees Spy evs)";
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
-qed "YM4_analz_sees_Spy";
+\ X : analz (spies evs)";
+by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1);
+qed "YM4_analz_spies";
-bind_thm ("YM4_parts_sees_Spy",
- YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
+bind_thm ("YM4_parts_spies",
+ YM4_analz_spies RS (impOfSubs analz_subset_parts));
(*Relates to both YM4 and Oops*)
goal thy "!!evs. Says S A {|NB, Crypt (shrK A) {|B,K,NA|}, X|} : set evs ==> \
-\ K : parts (sees Spy evs)";
+\ K : parts (spies evs)";
by (blast_tac (!claset addSEs partsEs
- addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
-qed "YM4_Key_parts_sees_Spy";
+ addSDs [Says_imp_spies RS parts.Inj]) 1);
+qed "YM4_Key_parts_spies";
-(*For proving the easier theorems about X ~: parts (sees Spy evs).*)
-fun parts_sees_tac i =
- forward_tac [YM4_Key_parts_sees_Spy] (i+6) THEN
- forward_tac [YM4_parts_sees_Spy] (i+5) THEN
+(*For proving the easier theorems about X ~: parts (spies evs).*)
+fun parts_spies_tac i =
+ forward_tac [YM4_Key_parts_spies] (i+6) THEN
+ forward_tac [YM4_parts_spies] (i+5) THEN
prove_simple_subgoals_tac i;
(*Induction for regularity theorems. If induction formula has the form
- X ~: analz (sees Spy evs) --> ... then it shortens the proof by discarding
- needless information about analz (insert X (sees Spy evs)) *)
+ X ~: analz (spies evs) --> ... then it shortens the proof by discarding
+ needless information about analz (insert X (spies evs)) *)
fun parts_induct_tac i =
etac yahalom.induct i
THEN
REPEAT (FIRSTGOAL analz_mono_contra_tac)
- THEN parts_sees_tac i;
+ THEN parts_spies_tac i;
-(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
+(** 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 lost at start)*)
+(*Spy never sees another agent's shared key! (unless it's bad at start)*)
goal thy
- "!!evs. evs : yahalom ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
+ "!!evs. evs : yahalom ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (Blast_tac 1);
@@ -87,13 +87,13 @@
Addsimps [Spy_see_shrK];
goal thy
- "!!evs. evs : yahalom ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
+ "!!evs. evs : yahalom ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
qed "Spy_analz_shrK";
Addsimps [Spy_analz_shrK];
-goal thy "!!A. [| Key (shrK A) : parts (sees Spy evs); \
-\ evs : yahalom |] ==> A:lost";
+goal thy "!!A. [| Key (shrK A) : parts (spies evs); \
+\ evs : yahalom |] ==> A:bad";
by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
qed "Spy_see_shrK_D";
@@ -103,10 +103,10 @@
(*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*)
goal thy "!!evs. evs : yahalom ==> \
-\ Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
+\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
by (parts_induct_tac 1);
(*YM4: Key K is not fresh!*)
-by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
+by (blast_tac (!claset addSEs spies_partsEs) 3);
(*YM3*)
by (blast_tac (!claset addss (!simpset)) 2);
(*Fake*)
@@ -137,8 +137,8 @@
(*For proofs involving analz.*)
-val analz_sees_tac =
- dtac YM4_analz_sees_Spy 6 THEN
+val analz_spies_tac =
+ dtac YM4_analz_spies 6 THEN
forward_tac [Says_Server_message_form] 7 THEN
assume_tac 7 THEN
REPEAT ((etac conjE ORELSE' hyp_subst_tac) 7);
@@ -147,8 +147,8 @@
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
- Key K : analz (sees Spy evs)
+ Key K : analz (insert (Key KAB) (spies evs)) ==>
+ Key K : analz (spies evs)
A more general formula must be proved inductively.
@@ -159,10 +159,10 @@
goal thy
"!!evs. evs : yahalom ==> \
\ ALL K KK. KK <= Compl (range shrK) --> \
-\ (Key K : analz (Key``KK Un (sees Spy evs))) = \
-\ (K : KK | Key K : analz (sees Spy evs))";
+\ (Key K : analz (Key``KK Un (spies evs))) = \
+\ (K : KK | Key K : analz (spies evs))";
by (etac yahalom.induct 1);
-by analz_sees_tac;
+by analz_spies_tac;
by (REPEAT_FIRST (resolve_tac [allI, impI]));
by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
@@ -174,8 +174,8 @@
goal thy
"!!evs. [| evs : yahalom; KAB ~: range shrK |] ==> \
-\ Key K : analz (insert (Key KAB) (sees Spy evs)) = \
-\ (K = KAB | Key K : analz (sees Spy evs))";
+\ Key K : analz (insert (Key KAB) (spies evs)) = \
+\ (K = KAB | Key K : analz (spies evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
qed "analz_insert_freshK";
@@ -195,18 +195,16 @@
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 sees_Spy_partsEs
+by (blast_tac (!claset addSEs spies_partsEs
delrules [conjI] (*prevent split-up into 4 subgoals*)
addss (!simpset addsimps [parts_insertI])) 1);
val lemma = result();
goal thy
"!!evs. [| Says Server A \
-\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} \
-\ : set evs; \
+\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} : set evs; \
\ Says Server A' \
-\ {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|} \
-\ : set evs; \
+\ {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|} : set evs; \
\ evs : yahalom |] \
\ ==> A=A' & B=B' & na=na' & nb=nb'";
by (prove_unique_tac lemma 1);
@@ -216,16 +214,16 @@
(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
goal thy
- "!!evs. [| A ~: lost; B ~: lost; A ~= B; \
+ "!!evs. [| A ~: bad; B ~: bad; A ~= B; \
\ evs : yahalom |] \
\ ==> Says Server A \
\ {|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 --> \
-\ Key K ~: analz (sees Spy evs)";
+\ Key K ~: analz (spies evs)";
by (etac yahalom.induct 1);
-by analz_sees_tac;
+by analz_spies_tac;
by (ALLGOALS
(asm_simp_tac
(!simpset addsimps [analz_insert_eq, analz_insert_freshK]
@@ -234,7 +232,7 @@
by (blast_tac (!claset addDs [unique_session_keys]) 3);
(*YM3*)
by (blast_tac (!claset delrules [impCE]
- addSEs sees_Spy_partsEs
+ addSEs spies_partsEs
addIs [impOfSubs analz_subset_parts]) 2);
(*Fake*)
by (spy_analz_tac 1);
@@ -248,8 +246,8 @@
\ Crypt (shrK B) {|nb, Key K, Agent A|}|} \
\ : set evs; \
\ Says A Spy {|na, nb, Key K|} ~: set evs; \
-\ A ~: lost; B ~: lost; evs : yahalom |] \
-\ ==> Key K ~: analz (sees Spy 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);
qed "Spy_not_see_encrypted_key";
@@ -261,8 +259,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 (sees Spy evs); \
-\ A ~: lost; 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|}|} \
@@ -279,9 +277,8 @@
(*B knows, by the first part of A's message, that the Server distributed
the key for A and B, and has associated it with NB. *)
goal thy
- "!!evs. [| Crypt (shrK B) {|Nonce NB, Key K, Agent A|} \
-\ : parts (sees Spy evs); \
-\ B ~: lost; evs : yahalom |] \
+ "!!evs. [| Crypt (shrK B) {|Nonce NB, Key K, Agent A|} : parts (spies evs); \
+\ B ~: bad; evs : yahalom |] \
\ ==> EX NA. Says Server A \
\ {|Nonce NB, \
\ Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, \
@@ -303,13 +300,13 @@
goal thy
"!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|}, X|} \
\ : set evs; \
-\ A ~: lost; B ~: lost; evs : yahalom |] \
+\ A ~: bad; B ~: bad; evs : yahalom |] \
\ ==> EX NA. Says Server A \
\ {|Nonce NB, \
\ Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, \
\ Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|} \
\ : set evs";
-by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1);
+by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1);
by (blast_tac (!claset addSDs [B_trusts_YM4_shrK]) 1);
qed "B_trusts_YM4";
@@ -320,8 +317,8 @@
(*The encryption in message YM2 tells us it cannot be faked.*)
goal thy
"!!evs. evs : yahalom \
-\ ==> Crypt (shrK B) {|Agent A, Nonce NA|} : parts (sees Spy evs) --> \
-\ B ~: lost --> \
+\ ==> Crypt (shrK B) {|Agent A, Nonce NA|} : parts (spies evs) --> \
+\ B ~: bad --> \
\ (EX NB. Says B Server {|Agent B, Nonce NB, \
\ Crypt (shrK B) {|Agent A, Nonce NA|}|} \
\ : set evs)";
@@ -336,7 +333,7 @@
"!!evs. evs : yahalom \
\ ==> Says Server A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
\ : set evs --> \
-\ B ~: lost --> \
+\ B ~: bad --> \
\ (EX nb'. Says B Server {|Agent B, nb', \
\ Crypt (shrK B) {|Agent A, Nonce NA|}|} \
\ : set evs)";
@@ -345,7 +342,7 @@
(*YM3*)
by (blast_tac (!claset addSDs [B_Said_YM2]
addSEs [MPair_parts]
- addDs [Says_imp_sees_Spy RS parts.Inj]) 3);
+ addDs [Says_imp_spies RS parts.Inj]) 3);
(*Fake, YM2*)
by (ALLGOALS Blast_tac);
val lemma = result() RSN (2, rev_mp) RS mp |> standard;
@@ -354,12 +351,12 @@
goal thy
"!!evs. [| Says S A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
\ : set evs; \
-\ A ~: lost; B ~: lost; evs : yahalom |] \
+\ A ~: bad; B ~: bad; evs : yahalom |] \
\ ==> EX nb'. Says B Server \
\ {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|} \
\ : set evs";
by (blast_tac (!claset addSDs [A_trusts_YM3, lemma]
- addEs sees_Spy_partsEs) 1);
+ addEs spies_partsEs) 1);
qed "YM3_auth_B_to_A";
@@ -370,12 +367,12 @@
NB matters for freshness.*)
goal thy
"!!evs. evs : yahalom \
-\ ==> Key K ~: analz (sees Spy evs) --> \
-\ Crypt K (Nonce NB) : parts (sees Spy evs) --> \
+\ ==> Key K ~: analz (spies evs) --> \
+\ Crypt K (Nonce NB) : parts (spies evs) --> \
\ Crypt (shrK B) {|Nonce NB, Key K, Agent A|} \
-\ : parts (sees Spy evs) --> \
-\ B ~: lost --> \
-\ (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
+\ : parts (spies evs) --> \
+\ B ~: bad --> \
+\ (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
by (parts_induct_tac 1);
(*Fake*)
by (Fake_parts_insert_tac 1);
@@ -384,10 +381,10 @@
(*YM4: was Crypt K (Nonce NB) the very last message? If not, use ind. hyp.*)
by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
(*yes: apply unicity of session keys*)
-by (not_lost_tac "Aa" 1);
+by (not_bad_tac "Aa" 1);
by (blast_tac (!claset addSEs [MPair_parts]
addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
- addDs [Says_imp_sees_Spy RS parts.Inj,
+ addDs [Says_imp_spies RS parts.Inj,
unique_session_keys]) 1);
val lemma = normalize_thm [RSspec, RSmp] (result()) |> standard;
@@ -398,14 +395,14 @@
"!!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); \
-\ A ~: lost; B ~: lost; evs : yahalom |] \
+\ A ~: bad; B ~: bad; evs : yahalom |] \
\ ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
-by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1);
+by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1);
by (dtac B_trusts_YM4_shrK 1);
by (safe_tac (!claset));
by (rtac lemma 1);
by (rtac Spy_not_see_encrypted_key 2);
by (REPEAT_FIRST assume_tac);
by (ALLGOALS (blast_tac (!claset addSEs [MPair_parts]
- addDs [Says_imp_sees_Spy RS parts.Inj])));
+ addDs [Says_imp_spies RS parts.Inj])));
qed_spec_mp "YM4_imp_A_Said_YM3";
--- a/src/HOL/Auth/Yahalom2.thy Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/Yahalom2.thy Thu Sep 18 13:24:04 1997 +0200
@@ -25,7 +25,7 @@
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
Fake "[| evs: yahalom; B ~= Spy;
- X: synth (analz (sees Spy evs)) |]
+ X: synth (analz (spies evs)) |]
==> Says Spy B X # evs : yahalom"
(*Alice initiates a protocol run*)