Changing "lost" from a parameter of protocol definitions to a constant.
Advantages: no "lost" argument everywhere; fewer Vars in subgoals;
less need for specially instantiated rules
Disadvantage: can no longer prove "Agent_not_see_encrypted_key", but this
theorem was never used, and its original proof was also broken
the introduction of the "Notes" constructor.
--- a/src/HOL/Auth/Event.ML Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/Event.ML Mon Jul 14 12:47:21 1997 +0200
@@ -10,53 +10,55 @@
open Event;
+AddIffs [Spy_in_lost, Server_not_lost];
+
(*** Function "sees" ***)
-(** Specialized rewrite rules for (sees lost A (Says...#evs)) **)
+(** Specialized rewrite rules for (sees A (Says...#evs)) **)
-goal thy "sees lost B (Says A B X # evs) = insert X (sees lost B evs)";
+goal thy "sees B (Says A B X # evs) = insert X (sees B evs)";
by (Simp_tac 1);
qed "sees_own";
-goal thy "sees lost B (Notes A X # evs) = \
-\ (if A=B then insert X (sees lost B evs) else sees lost B evs)";
+goal thy "sees B (Notes A X # evs) = \
+\ (if A=B then insert X (sees B evs) else sees B evs)";
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
qed "sees_Notes";
-(** Three special-case rules for rewriting of sees lost A **)
+(** Three special-case rules for rewriting of sees A **)
goal thy "!!A. Server ~= B ==> \
-\ sees lost Server (Says A B X # evs) = sees lost Server evs";
+\ sees Server (Says A B X # evs) = sees Server evs";
by (Asm_simp_tac 1);
qed "sees_Server";
goal thy "!!A. Friend i ~= B ==> \
-\ sees lost (Friend i) (Says A B X # evs) = sees lost (Friend i) evs";
+\ sees (Friend i) (Says A B X # evs) = sees (Friend i) evs";
by (Asm_simp_tac 1);
qed "sees_Friend";
-goal thy "sees lost Spy (Says A B X # evs) = insert X (sees lost Spy evs)";
+goal thy "sees Spy (Says A B X # evs) = insert X (sees Spy evs)";
by (Simp_tac 1);
qed "sees_Spy";
-goal thy "sees lost A (Says A' B X # evs) <= insert X (sees lost A evs)";
+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 lost A evs <= sees lost A (Says A' B X # evs)";
+goal thy "sees A evs <= sees A (Says A' B X # evs)";
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
by (Fast_tac 1);
qed "sees_subset_sees_Says";
-goal thy "sees lost A evs <= sees lost A (Notes A' X # evs)";
+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 lost A (Says B C Y # evs))) = \
-\ parts {Y} Un (UN A. parts (sees lost A evs))";
+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
@@ -64,8 +66,8 @@
setloop split_tac [expand_if]))));
qed "UN_parts_sees_Says";
-goal thy "(UN A. parts (sees lost A (Notes B Y # evs))) = \
-\ parts {Y} Un (UN A. parts (sees lost A evs))";
+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
@@ -73,7 +75,7 @@
setloop split_tac [expand_if]))));
qed "UN_parts_sees_Notes";
-goal thy "Says A B X : set evs --> X : sees lost Spy evs";
+goal thy "Says A B X : set evs --> X : sees Spy evs";
by (list.induct_tac "evs" 1);
by (Auto_tac ());
qed_spec_mp "Says_imp_sees_Spy";
@@ -90,7 +92,7 @@
(*** Fresh nonces ***)
-goalw thy [used_def] "!!X. X: parts (sees lost B evs) ==> X: used evs";
+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";
@@ -124,12 +126,12 @@
qed "used_subset_append";
-(** Simplifying parts (insert X (sees lost A evs))
- = parts {X} Un parts (sees lost A evs) -- since general case loops*)
+(** 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 lost A evs")]
+ [("H", "sees A evs")]
|> standard;
@@ -140,7 +142,7 @@
it will omit complicated reasoning about analz.*)
val analz_mono_contra_tac =
let val impI' = read_instantiate_sg (sign_of thy)
- [("P", "?Y ~: analz (sees lost ?A ?evs)")] impI;
+ [("P", "?Y ~: analz (sees ?A ?evs)")] impI;
in
rtac impI THEN'
REPEAT1 o
--- a/src/HOL/Auth/Event.thy Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/Event.thy Mon Jul 14 12:47:21 1997 +0200
@@ -11,7 +11,7 @@
Event = Message + List +
consts (*Initial states of agents -- parameter of the construction*)
- initState :: [agent set, agent] => msg set
+ initState :: agent => msg set
datatype (*Messages--could add another constructor for agent knowledge*)
event = Says agent agent msg
@@ -26,17 +26,22 @@
sees1_Notes "sees1 A (Notes A' X) = (if A = A' then {X} else {})"
consts
- sees :: [agent set, agent, event list] => msg set
+ lost :: agent set (*agents whose private keys have been compromised*)
+ sees :: [agent, 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"
primrec sees list
- sees_Nil "sees lost A [] = initState lost A"
- sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
-
+ sees_Nil "sees A [] = initState A"
+ sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
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 lost B. sees lost B evs)"
+ "used evs == parts (UN B. sees B evs)"
end
--- a/src/HOL/Auth/Message.ML Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/Message.ML Mon Jul 14 12:47:21 1997 +0200
@@ -908,8 +908,6 @@
val Un_absorb3 = result();
Addsimps [Un_absorb3];
-Addsimps [Un_insert_left, Un_insert_right];
-
(*By default only o_apply is built-in. But in the presence of eta-expansion
this means that some terms displayed as (f o g) will be rewritten, and others
will not!*)
--- a/src/HOL/Auth/NS_Public.ML Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/NS_Public.ML Mon Jul 14 12:47:21 1997 +0200
@@ -5,8 +5,6 @@
Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
Version incorporating Lowe's fix (inclusion of B's identify in round 2).
-
-PROOFS BELOW MIGHT BE SIMPLIFIED using Yahalom's analz_mono_parts_induct_tac
*)
open NS_Public;
@@ -16,10 +14,6 @@
AddIffs [Spy_in_lost];
-(*Replacing the variable by a constant improves search speed by 50%!*)
-val Says_imp_sees_Spy' =
- read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
-
(*A "possibility property": there are traces that reach the end*)
goal thy
"!!A B. A ~= B ==> EX NB. EX evs: ns_public. \
@@ -41,27 +35,35 @@
AddSEs [not_Says_to_self RSN (2, rev_notE)];
-(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
+(*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)) *)
+fun parts_induct_tac i =
+ etac ns_public.induct i
+ THEN
+ REPEAT (FIRSTGOAL analz_mono_contra_tac)
+ THEN
+ prove_simple_subgoals_tac i;
+
+
+(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
sends messages containing X! **)
(*Spy never sees another agent's private key! (unless it's lost at start)*)
goal thy
- "!!evs. evs : ns_public \
-\ ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)";
-by (etac ns_public.induct 1);
-by (prove_simple_subgoals_tac 1);
+ "!!A. evs: ns_public ==> (Key (priK A) : parts (sees Spy evs)) = (A : lost)";
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
qed "Spy_see_priK";
Addsimps [Spy_see_priK];
goal thy
- "!!evs. evs : ns_public \
-\ ==> (Key (priK A) : analz (sees lost Spy evs)) = (A : lost)";
+ "!!A. evs: ns_public ==> (Key (priK A) : analz (sees Spy evs)) = (A : lost)";
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 lost Spy evs); \
+goal thy "!!A. [| Key (priK A) : parts (sees Spy evs); \
\ evs : ns_public |] ==> A:lost";
by (blast_tac (!claset addDs [Spy_see_priK]) 1);
qed "Spy_see_priK_D";
@@ -70,87 +72,79 @@
AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
+(**** Authenticity properties obtained from NS2 ****)
+
+(*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, Agent D|} ~: parts (sees Spy evs)";
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (parts_induct_tac 1);
+(*NS3*)
+by (blast_tac (!claset addSEs partsEs) 3);
+(*NS2*)
+by (blast_tac (!claset addSEs partsEs) 2);
+by (Fake_parts_insert_tac 1);
+qed "no_nonce_NS1_NS2";
+
+
+(*Unicity for NS1: nonce NA identifies agents A and B*)
+goal thy
+ "!!evs. [| Nonce NA ~: analz (sees Spy evs); evs : ns_public |] \
+\ ==> EX A' B'. ALL A B. \
+\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees Spy 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])));
+(*NS1*)
+by (expand_case_tac "NA = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2);
+(*Fake*)
+by (step_tac (!claset addSIs [analz_insertI]) 1);
+by (ex_strip_tac 1);
+by (Fake_parts_insert_tac 1);
+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 |] \
+\ ==> A=A' & B=B'";
+by (prove_unique_tac lemma 1);
+qed "unique_NA";
+
+
+(*Tactic for proving secrecy theorems*)
fun analz_induct_tac i =
etac ns_public.induct i THEN
ALLGOALS (asm_simp_tac
(!simpset addsimps [not_parts_not_analz]
setloop split_tac [expand_if]));
-(**** Authenticity properties obtained from NS2 ****)
-
-(*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. [| Nonce NA ~: analz (sees lost Spy evs); \
-\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs); \
-\ evs : ns_public |] \
-\ ==> Crypt (pubK C) {|NA', Nonce NA, Agent D|} ~: parts (sees lost Spy evs)";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (analz_induct_tac 1);
-(*NS3*)
-by (blast_tac (!claset addSEs partsEs) 4);
-(*NS2*)
-by (blast_tac (!claset addSEs partsEs) 3);
-(*Fake*)
-by (blast_tac (!claset addSIs [analz_insertI]
- addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]) 2);
-(*Base*)
-by (Blast_tac 1);
-qed "no_nonce_NS1_NS2";
-
-
-(*Unicity for NS1: nonce NA identifies agents A and B*)
-goal thy
- "!!evs. [| Nonce NA ~: analz (sees lost Spy evs); evs : ns_public |] \
-\ ==> EX A' B'. ALL A B. \
-\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \
-\ A=A' & B=B'";
-by (etac rev_mp 1);
-by (analz_induct_tac 1);
-(*NS1*)
-by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
-by (expand_case_tac "NA = ?y" 3 THEN
- REPEAT (blast_tac (!claset addSEs partsEs) 3));
-(*Base*)
-by (Blast_tac 1);
-(*Fake*)
-by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1);
-by (step_tac (!claset addSIs [analz_insertI]) 1);
-by (ex_strip_tac 1);
-by (blast_tac (!claset delrules [conjI]
- addSDs [impOfSubs Fake_parts_insert]
- addDs [impOfSubs analz_subset_parts]) 1);
-val lemma = result();
-
-goal thy
- "!!evs. [| Crypt(pubK B) {|Nonce NA, Agent A|} : parts(sees lost Spy evs); \
-\ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(sees lost Spy evs); \
-\ Nonce NA ~: analz (sees lost Spy evs); \
-\ evs : ns_public |] \
-\ ==> A=A' & B=B'";
-by (prove_unique_tac lemma 1);
-qed "unique_NA";
-
(*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 lost Spy evs)";
+\ ==> Nonce NA ~: analz (sees Spy 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_sees_Spy 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_sees_Spy RS parts.Inj,
parts.Body, unique_NA]) 3);
(*NS1*)
by (blast_tac (!claset addSEs sees_Spy_partsEs
- addIs [impOfSubs analz_subset_parts]) 2);
+ addIs [impOfSubs analz_subset_parts]) 2);
(*Fake*)
by (spy_analz_tac 1);
qed "Spy_not_see_NA";
@@ -159,15 +153,15 @@
(*Authentication for A: if she receives message 2 and has used NA
to start a run, then B has sent message 2.*)
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, Agent B|}) \
-\ : set evs; \
-\ A ~: lost; B ~: lost; evs : ns_public |] \
-\ ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
+ "!!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 |] \
+\ ==> 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_sees_Spy RS parts.Inj RS rev_mp) 1);
by (etac ns_public.induct 1);
by (ALLGOALS Asm_simp_tac);
(*NS1*)
@@ -180,19 +174,14 @@
(*If the encrypted message appears then it originated with Alice in NS1*)
goal thy
- "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs); \
-\ Nonce NA ~: analz (sees lost Spy evs); \
+ "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees Spy evs); \
+\ Nonce NA ~: analz (sees Spy 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);
-by (analz_induct_tac 1);
-(*Fake*)
-by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
- addIs [analz_insertI]
- addDs [impOfSubs analz_subset_parts]) 2);
-(*Base*)
-by (Blast_tac 1);
+by (parts_induct_tac 1);
+by (Fake_parts_insert_tac 1);
qed "B_trusts_NS1";
@@ -203,33 +192,28 @@
[unicity of B makes Lowe's fix work]
[proof closely follows that for unique_NA] *)
goal thy
- "!!evs. [| Nonce NB ~: analz (sees lost Spy evs); evs : ns_public |] \
+ "!!evs. [| Nonce NB ~: analz (sees Spy evs); evs : ns_public |] \
\ ==> EX A' NA' B'. ALL A NA B. \
\ Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|} \
-\ : parts (sees lost Spy evs) --> A=A' & NA=NA' & B=B'";
+\ : parts (sees Spy evs) --> A=A' & NA=NA' & B=B'";
by (etac rev_mp 1);
-by (analz_induct_tac 1);
+by (parts_induct_tac 1);
+by (ALLGOALS
+ (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees])));
(*NS2*)
-by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
-by (expand_case_tac "NB = ?y" 3 THEN
- REPEAT (blast_tac (!claset addSEs partsEs) 3));
-(*Base*)
-by (Blast_tac 1);
+by (expand_case_tac "NB = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2);
(*Fake*)
-by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1);
by (step_tac (!claset addSIs [analz_insertI]) 1);
by (ex_strip_tac 1);
-by (blast_tac (!claset delrules [conjI]
- addSDs [impOfSubs Fake_parts_insert]
- addDs [impOfSubs analz_subset_parts]) 1);
+by (Fake_parts_insert_tac 1);
val lemma = result();
goal thy
"!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|} \
-\ : parts(sees lost Spy evs); \
+\ : parts(sees Spy evs); \
\ Crypt(pubK A') {|Nonce NA', Nonce NB, Agent B'|} \
-\ : parts(sees lost Spy evs); \
-\ Nonce NB ~: analz (sees lost Spy evs); \
+\ : parts(sees Spy evs); \
+\ Nonce NB ~: analz (sees Spy evs); \
\ evs : ns_public |] \
\ ==> A=A' & NA=NA' & B=B'";
by (prove_unique_tac lemma 1);
@@ -241,12 +225,11 @@
"!!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 lost Spy evs)";
+\ ==> Nonce NB ~: analz (sees Spy 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_sees_Spy RS parts.Inj, unique_NB]) 4);
(*NS1*)
by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
(*Fake*)
@@ -254,7 +237,7 @@
(*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 addSDs [Says_imp_sees_Spy 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";
@@ -270,8 +253,8 @@
\ ==> 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 (analz_induct_tac 1);
+by (etac (Says_imp_sees_Spy RS parts.Inj RS rev_mp) 1);
+by (parts_induct_tac 1);
(*NS1*)
by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
(*Fake*)
@@ -280,7 +263,7 @@
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_sees_Spy RS parts.Inj,
Spy_not_see_NB, unique_NB]) 1);
qed "B_trusts_NS3";
@@ -288,8 +271,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_sees_Spy' =
+ read_instantiate [("X","Crypt ?K {|?XX,?YY,?ZZ|}")] Says_imp_sees_Spy;
(*If B receives NS3 and the nonce NB agrees with the nonce he joined with
@@ -302,7 +285,7 @@
\ ==> 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_sees_Spy RS parts.Inj RS rev_mp) 1);
by (etac ns_public.induct 1);
by (ALLGOALS Asm_simp_tac);
(*Fake, NS2, NS3*)
@@ -318,7 +301,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_sees_Spy' RS parts.Inj]
addDs [unique_NB]) 1);
qed "B_trusts_protocol";
--- a/src/HOL/Auth/NS_Public.thy Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/NS_Public.thy Mon Jul 14 12:47:21 1997 +0200
@@ -9,8 +9,7 @@
NS_Public = Public +
-consts lost :: agent set (*No need for it to be a variable*)
- ns_public :: event list set
+consts ns_public :: event list set
inductive ns_public
intrs
@@ -21,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 lost Spy evs)) |]
+ X: synth (analz (sees Spy evs)) |]
==> Says Spy B X # evs : ns_public"
(*Alice initiates a protocol run, sending a nonce to Bob*)
@@ -44,8 +43,4 @@
(**Oops message??**)
-rules
- (*Spy has access to his own key for spoof messages*)
- Spy_in_lost "Spy: lost"
-
end
--- a/src/HOL/Auth/NS_Public_Bad.ML Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.ML Mon Jul 14 12:47:21 1997 +0200
@@ -18,10 +18,6 @@
AddIffs [Spy_in_lost];
-(*Replacing the variable by a constant improves search speed by 50%!*)
-val Says_imp_sees_Spy' =
- read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
-
(*A "possibility property": there are traces that reach the end*)
goal thy
"!!A B. A ~= B ==> EX NB. EX evs: ns_public. \
@@ -43,27 +39,35 @@
AddSEs [not_Says_to_self RSN (2, rev_notE)];
-(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
+(*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)) *)
+fun parts_induct_tac i =
+ etac ns_public.induct i
+ THEN
+ REPEAT (FIRSTGOAL analz_mono_contra_tac)
+ THEN
+ prove_simple_subgoals_tac i;
+
+
+(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
sends messages containing X! **)
(*Spy never sees another agent's private key! (unless it's lost at start)*)
goal thy
- "!!evs. evs : ns_public \
-\ ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)";
-by (etac ns_public.induct 1);
-by (prove_simple_subgoals_tac 1);
+ "!!A. evs: ns_public ==> (Key (priK A) : parts (sees Spy evs)) = (A : lost)";
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
qed "Spy_see_priK";
Addsimps [Spy_see_priK];
goal thy
- "!!evs. evs : ns_public \
-\ ==> (Key (priK A) : analz (sees lost Spy evs)) = (A : lost)";
+ "!!A. evs: ns_public ==> (Key (priK A) : analz (sees Spy evs)) = (A : lost)";
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 lost Spy evs); \
+goal thy "!!A. [| Key (priK A) : parts (sees Spy evs); \
\ evs : ns_public |] ==> A:lost";
by (blast_tac (!claset addDs [Spy_see_priK]) 1);
qed "Spy_see_priK_D";
@@ -72,6 +76,55 @@
AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
+(**** Authenticity properties obtained from NS2 ****)
+
+(*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)";
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (parts_induct_tac 1);
+(*NS3*)
+by (blast_tac (!claset addSEs partsEs) 3);
+(*NS2*)
+by (blast_tac (!claset addSEs partsEs) 2);
+by (Fake_parts_insert_tac 1);
+qed "no_nonce_NS1_NS2";
+
+
+(*Unicity for NS1: nonce NA identifies agents A and B*)
+goal thy
+ "!!evs. [| Nonce NA ~: analz (sees Spy evs); evs : ns_public |] \
+\ ==> EX A' B'. ALL A B. \
+\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees Spy 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])));
+(*NS1*)
+by (expand_case_tac "NA = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2);
+(*Fake*)
+by (step_tac (!claset addSIs [analz_insertI]) 1);
+by (ex_strip_tac 1);
+by (Fake_parts_insert_tac 1);
+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 |] \
+\ ==> A=A' & B=B'";
+by (prove_unique_tac lemma 1);
+qed "unique_NA";
+
+
+(*Tactic for proving secrecy theorems*)
fun analz_induct_tac i =
etac ns_public.induct i THEN
ALLGOALS (asm_simp_tac
@@ -79,77 +132,19 @@
setloop split_tac [expand_if]));
-(**** Authenticity properties obtained from NS2 ****)
-
-(*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. [| Nonce NA ~: analz (sees lost Spy evs); \
-\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs); \
-\ evs : ns_public |] \
-\ ==> Crypt (pubK C) {|NA', Nonce NA|} ~: parts (sees lost Spy evs)";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (analz_induct_tac 1);
-(*NS3*)
-by (blast_tac (!claset addSEs partsEs) 4);
-(*NS2*)
-by (blast_tac (!claset addSEs partsEs) 3);
-(*Fake*)
-by (blast_tac (!claset addSIs [analz_insertI]
- addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]) 2);
-(*Base*)
-by (Blast_tac 1);
-qed "no_nonce_NS1_NS2";
-
-
-(*Unicity for NS1: nonce NA identifies agents A and B*)
-goal thy
- "!!evs. [| Nonce NA ~: analz (sees lost Spy evs); evs : ns_public |] \
-\ ==> EX A' B'. ALL A B. \
-\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \
-\ A=A' & B=B'";
-by (etac rev_mp 1);
-by (analz_induct_tac 1);
-(*NS1*)
-by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
-by (expand_case_tac "NA = ?y" 3 THEN
- REPEAT (blast_tac (!claset addSEs partsEs) 3));
-(*Base*)
-by (Blast_tac 1);
-(*Fake*)
-by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1);
-by (step_tac (!claset addSIs [analz_insertI]) 1);
-by (ex_strip_tac 1);
-by (blast_tac (!claset delrules [conjI]
- addSDs [impOfSubs Fake_parts_insert]
- addDs [impOfSubs analz_subset_parts]) 1);
-val lemma = result();
-
-goal thy
- "!!evs. [| Crypt(pubK B) {|Nonce NA, Agent A|} : parts(sees lost Spy evs); \
-\ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(sees lost Spy evs); \
-\ Nonce NA ~: analz (sees lost Spy evs); \
-\ evs : ns_public |] \
-\ ==> A=A' & B=B'";
-by (prove_unique_tac lemma 1);
-qed "unique_NA";
-
-
(*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 lost Spy evs)";
+\ ==> Nonce NA ~: analz (sees Spy 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_sees_Spy 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_sees_Spy RS parts.Inj,
parts.Body, unique_NA]) 3);
(*NS1*)
by (blast_tac (!claset addSEs sees_Spy_partsEs
@@ -168,7 +163,7 @@
\ ==> 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_sees_Spy RS parts.Inj RS rev_mp) 1);
by (etac ns_public.induct 1);
by (ALLGOALS Asm_simp_tac);
(*NS1*)
@@ -179,25 +174,20 @@
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_sees_Spy 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 lost Spy evs); \
-\ Nonce NA ~: analz (sees lost Spy evs); \
+ "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees Spy evs); \
+\ Nonce NA ~: analz (sees Spy 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);
-by (analz_induct_tac 1);
-(*Fake*)
-by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
- addIs [analz_insertI]
- addDs [impOfSubs analz_subset_parts]) 2);
-(*Base*)
-by (Blast_tac 1);
+by (parts_induct_tac 1);
+by (Fake_parts_insert_tac 1);
qed "B_trusts_NS1";
@@ -207,31 +197,26 @@
(*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 lost Spy evs); evs : ns_public |] \
+ "!!evs. [| Nonce NB ~: analz (sees Spy evs); evs : ns_public |] \
\ ==> EX A' NA'. ALL A NA. \
\ Crypt (pubK A) {|Nonce NA, Nonce NB|} \
-\ : parts (sees lost Spy evs) --> A=A' & NA=NA'";
+\ : parts (sees Spy evs) --> A=A' & NA=NA'";
by (etac rev_mp 1);
-by (analz_induct_tac 1);
+by (parts_induct_tac 1);
+by (ALLGOALS
+ (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees])));
(*NS2*)
-by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
-by (expand_case_tac "NB = ?y" 3 THEN
- REPEAT (blast_tac (!claset addSEs partsEs) 3));
-(*Base*)
-by (Blast_tac 1);
+by (expand_case_tac "NB = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2);
(*Fake*)
-by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1);
by (step_tac (!claset addSIs [analz_insertI]) 1);
by (ex_strip_tac 1);
-by (blast_tac (!claset delrules [conjI]
- addSDs [impOfSubs Fake_parts_insert]
- addDs [impOfSubs analz_subset_parts]) 1);
+by (Fake_parts_insert_tac 1);
val lemma = result();
goal thy
- "!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB|} : parts(sees lost Spy evs); \
-\ Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(sees lost Spy evs); \
-\ Nonce NB ~: analz (sees lost Spy evs); \
+ "!!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 : ns_public |] \
\ ==> A=A' & NA=NA'";
by (prove_unique_tac lemma 1);
@@ -243,7 +228,7 @@
"!!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 lost Spy evs)";
+\ ==> Nonce NB ~: analz (sees Spy evs)";
by (etac rev_mp 1);
by (etac rev_mp 1);
by (analz_induct_tac 1);
@@ -256,10 +241,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_sees_Spy 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 addSDs [Says_imp_sees_Spy 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";
@@ -276,8 +261,8 @@
\ ==> 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 (analz_induct_tac 1);
+by (etac (Says_imp_sees_Spy 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);
@@ -287,7 +272,7 @@
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_sees_Spy RS parts.Inj,
Spy_not_see_NB, unique_NB]) 1);
qed "B_trusts_NS3";
@@ -296,11 +281,11 @@
goal thy
"!!evs. [| A ~: lost; B ~: lost; evs : ns_public |] \
\ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs \
-\ --> Nonce NB ~: analz (sees lost Spy evs)";
+\ --> Nonce NB ~: analz (sees Spy 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_sees_Spy RS parts.Inj]) 2);
(*Fake*)
by (spy_analz_tac 1);
(*NS2 and NS3*)
@@ -308,12 +293,12 @@
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_sees_Spy RS parts.Inj]) 2);
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy 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_sees_Spy RS parts.Inj RS unique_NB) 1
+ THEN REPEAT (eresolve_tac [asm_rl, Says_imp_sees_Spy RS parts.Inj] 1));
by (Step_tac 1);
(*
@@ -322,14 +307,14 @@
!!evs. [| A ~: lost; B ~: lost; evs : ns_public |]
==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
: set evs -->
- Nonce NB ~: analz (sees lost Spy evs)
+ Nonce NB ~: analz (sees Spy evs)
1. !!evs Aa Ba B' NAa NBa evsa.
[| A ~: lost; B ~: lost; 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;
Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evsa;
- Nonce NB ~: analz (sees lost Spy evsa) |]
+ Nonce NB ~: analz (sees Spy evsa) |]
==> False
*)
--- a/src/HOL/Auth/NS_Public_Bad.thy Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.thy Mon Jul 14 12:47:21 1997 +0200
@@ -13,8 +13,7 @@
NS_Public_Bad = Public +
-consts lost :: agent set (*No need for it to be a variable*)
- ns_public :: event list set
+consts ns_public :: event list set
inductive ns_public
intrs
@@ -25,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 lost Spy evs)) |]
+ X: synth (analz (sees Spy evs)) |]
==> Says Spy B X # evs : ns_public"
(*Alice initiates a protocol run, sending a nonce to Bob*)
@@ -47,8 +46,4 @@
(**Oops message??**)
-rules
- (*Spy has access to his own key for spoof messages*)
- Spy_in_lost "Spy: lost"
-
end
--- a/src/HOL/Auth/NS_Shared.ML Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/NS_Shared.ML Mon Jul 14 12:47:21 1997 +0200
@@ -15,14 +15,11 @@
proof_timing:=true;
HOL_quantifiers := false;
-(*Replacing the variable by a constant improves search speed by 50%!*)
-val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy;
-
(*A "possibility property": there are traces that reach the end*)
goal thy
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
-\ ==> EX N K. EX evs: ns_shared lost. \
+\ ==> EX N K. EX evs: ns_shared. \
\ Says A B (Crypt K {|Nonce N, Nonce N|}) : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS
@@ -34,7 +31,7 @@
(**** Inductive proofs about ns_shared ****)
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs : ns_shared lost ==> ALL A X. Says A A X ~: set evs";
+goal thy "!!evs. evs : ns_shared ==> ALL A X. Says A A X ~: set evs";
by (etac ns_shared.induct 1);
by (Auto_tac());
qed_spec_mp "not_Says_to_self";
@@ -43,48 +40,46 @@
(*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 lost Spy evs)";
+\ ==> X : parts (sees Spy evs)";
by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
qed "NS3_msg_in_parts_sees_Spy";
goal thy
"!!evs. Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set evs \
-\ ==> K : parts (sees lost Spy evs)";
+\ ==> K : parts (sees Spy evs)";
by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
qed "Oops_parts_sees_Spy";
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
- We instantiate the variable to "lost" since leaving it as a Var would
- interfere with simplification.*)
-val parts_induct_tac =
- etac ns_shared.induct 1 THEN
- dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5 THEN
- forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 8 THEN
- prove_simple_subgoals_tac 1;
+(*For proving the easier theorems about X ~: parts (sees Spy 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
+ prove_simple_subgoals_tac i;
-(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
+(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
sends messages containing X! **)
(*Spy never sees another agent's shared key! (unless it's lost at start)*)
goal thy
- "!!evs. evs : ns_shared lost \
-\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by parts_induct_tac;
+ "!!evs. evs : ns_shared \
+\ ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (Blast_tac 1);
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
goal thy
- "!!evs. evs : ns_shared lost \
-\ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
+ "!!evs. evs : ns_shared \
+\ ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
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 lost Spy evs); \
-\ evs : ns_shared lost |] ==> A:lost";
+goal thy "!!A. [| Key (shrK A) : parts (sees Spy evs); \
+\ evs : ns_shared |] ==> A:lost";
by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
qed "Spy_see_shrK_D";
@@ -93,9 +88,9 @@
(*Nobody can have used non-existent keys!*)
-goal thy "!!evs. evs : ns_shared lost ==> \
-\ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
-by parts_induct_tac;
+goal thy "!!evs. evs : ns_shared ==> \
+\ Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
+by (parts_induct_tac 1);
(*Fake*)
by (best_tac
(!claset addIs [impOfSubs analz_subset_parts]
@@ -119,7 +114,7 @@
goal thy
"!!evs. [| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) \
\ : set evs; \
-\ evs : ns_shared lost |] \
+\ evs : ns_shared |] \
\ ==> K ~: range shrK & \
\ X = (Crypt (shrK B) {|Key K, Agent A|}) & \
\ K' = shrK A";
@@ -132,15 +127,15 @@
(*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 lost Spy evs); \
-\ A ~: lost; evs : ns_shared lost |] \
+\ : parts (sees Spy evs); \
+\ A ~: lost; evs : ns_shared |] \
\ ==> X = (Crypt (shrK B) {|Key K, Agent A|}) & \
\ Says Server A \
\ (Crypt (shrK A) {|NA, Agent B, Key K, \
\ Crypt (shrK B) {|Key K, Agent A|}|}) \
\ : set evs";
by (etac rev_mp 1);
-by parts_induct_tac;
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (Auto_tac());
qed "A_trusts_NS2";
@@ -151,11 +146,11 @@
Use Says_Server_message_form if applicable.*)
goal thy
"!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) \
-\ : set evs; evs : ns_shared lost |] \
+\ : set evs; evs : ns_shared |] \
\ ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|})) \
-\ | X : analz (sees lost Spy evs)";
+\ | X : analz (sees Spy evs)";
by (case_tac "A : lost" 1);
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]
+by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
addss (!simpset)) 1);
by (forward_tac [Says_imp_sees_Spy RS parts.Inj] 1);
by (blast_tac (!claset addEs partsEs
@@ -163,18 +158,18 @@
qed "Says_S_message_form";
-(*For proofs involving analz. We again instantiate the variable to "lost".*)
+(*For proofs involving analz.*)
val analz_sees_tac =
- forw_inst_tac [("lost","lost")] Says_Server_message_form 8 THEN
- forw_inst_tac [("lost","lost")] Says_S_message_form 5 THEN
+ 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);
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
- Key K : analz (sees lost Spy evs)
+ Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
+ Key K : analz (sees Spy evs)
A more general formula must be proved inductively.
@@ -185,10 +180,10 @@
to encrypt messages containing other keys, in the actual protocol.
We require that agents should behave like this subsequently also.*)
goal thy
- "!!evs. [| evs : ns_shared lost; Kab ~: range shrK |] ==> \
-\ (Crypt KAB X) : parts (sees lost Spy evs) & \
-\ Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
-by parts_induct_tac;
+ "!!evs. [| evs : ns_shared; Kab ~: range shrK |] ==> \
+\ (Crypt KAB X) : parts (sees Spy evs) & \
+\ Key K : parts {X} --> Key K : parts (sees Spy evs)";
+by (parts_induct_tac 1);
(*Deals with Faked messages*)
by (blast_tac (!claset addSEs partsEs
addDs [impOfSubs parts_insert_subset_Un]) 1);
@@ -201,10 +196,10 @@
(*The equality makes the induction hypothesis easier to apply*)
goal thy
- "!!evs. evs : ns_shared lost ==> \
+ "!!evs. evs : ns_shared ==> \
\ ALL K KK. KK <= Compl (range shrK) --> \
-\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
-\ (K : KK | Key K : analz (sees lost Spy evs))";
+\ (Key K : analz (Key``KK Un (sees Spy evs))) = \
+\ (K : KK | Key K : analz (sees Spy evs))";
by (etac ns_shared.induct 1);
by analz_sees_tac;
by (REPEAT_FIRST (resolve_tac [allI, impI]));
@@ -219,9 +214,9 @@
goal thy
- "!!evs. [| evs : ns_shared lost; KAB ~: range shrK |] ==> \
-\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
-\ (K = KAB | Key K : analz (sees lost Spy evs))";
+ "!!evs. [| evs : ns_shared; KAB ~: range shrK |] ==> \
+\ Key K : analz (insert (Key KAB) (sees Spy evs)) = \
+\ (K = KAB | Key K : analz (sees Spy evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
qed "analz_insert_freshK";
@@ -229,7 +224,7 @@
(** The session key K uniquely identifies the message **)
goal thy
- "!!evs. evs : ns_shared lost ==> \
+ "!!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'";
@@ -254,7 +249,7 @@
\ Says Server A' \
\ (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) \
\ : set evs; \
-\ evs : ns_shared lost |] ==> A=A' & NA=NA' & B=B' & X = X'";
+\ evs : ns_shared |] ==> A=A' & NA=NA' & B=B' & X = X'";
by (prove_unique_tac lemma 1);
qed "unique_session_keys";
@@ -262,13 +257,13 @@
(** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
goal thy
- "!!evs. [| A ~: lost; B ~: lost; evs : ns_shared lost |] \
+ "!!evs. [| A ~: lost; B ~: lost; 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 lost Spy evs)";
+\ Key K ~: analz (sees Spy evs)";
by (etac ns_shared.induct 1);
by analz_sees_tac;
by (ALLGOALS
@@ -287,7 +282,7 @@
by (spy_analz_tac 1);
(*NS3*) (**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_sees_Spy 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);
@@ -300,8 +295,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 lost \
-\ |] ==> Key K ~: analz (sees lost Spy evs)";
+\ A ~: lost; B ~: lost; evs : ns_shared \
+\ |] ==> Key K ~: analz (sees Spy 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";
@@ -314,14 +309,14 @@
(*If the encrypted message appears then it originated with the Server*)
goal thy
- "!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (sees lost Spy evs); \
-\ B ~: lost; evs : ns_shared lost |] \
+ "!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (sees Spy evs); \
+\ B ~: lost; evs : ns_shared |] \
\ ==> EX NA. Says Server A \
\ (Crypt (shrK A) {|NA, Agent B, Key K, \
\ Crypt (shrK B) {|Key K, Agent A|}|}) \
\ : set evs";
by (etac rev_mp 1);
-by parts_induct_tac;
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
(*Fake case*)
by (ALLGOALS Blast_tac);
@@ -329,16 +324,16 @@
goal thy
- "!!evs. [| B ~: lost; evs : ns_shared lost |] \
-\ ==> Key K ~: analz (sees lost Spy evs) --> \
+ "!!evs. [| B ~: lost; evs : ns_shared |] \
+\ ==> Key K ~: analz (sees Spy evs) --> \
\ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \
\ : set evs --> \
-\ Crypt K (Nonce NB) : parts (sees lost Spy evs) --> \
+\ Crypt K (Nonce NB) : parts (sees Spy 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 (dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5);
-by (forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 8);
+by (dtac NS3_msg_in_parts_sees_Spy 5);
+by (forward_tac [Oops_parts_sees_Spy] 8);
by (TRYALL (rtac impI));
by (REPEAT_FIRST
(dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD)));
@@ -349,25 +344,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 lost Spy evsa) *)
+ Key K ~: used evsa and Crypt K (Nonce NB) : parts (sees Spy 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 (blast_tac (!claset addDs [Says_imp_sees_Spy 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);
val lemma = result();
goal thy
- "!!evs. [| Crypt K (Nonce NB) : parts (sees lost Spy evs); \
+ "!!evs. [| Crypt K (Nonce NB) : parts (sees Spy 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 lost |] \
+\ A ~: lost; B ~: lost; 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 Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/NS_Shared.thy Mon Jul 14 12:47:21 1997 +0200
@@ -12,69 +12,69 @@
NS_Shared = Shared +
-consts ns_shared :: agent set => event list set
-inductive "ns_shared lost"
+consts ns_shared :: event list set
+inductive "ns_shared"
intrs
(*Initial trace is empty*)
- Nil "[]: ns_shared lost"
+ Nil "[]: ns_shared"
(*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: ns_shared lost; B ~= Spy;
- X: synth (analz (sees lost Spy evs)) |]
- ==> Says Spy B X # evs : ns_shared lost"
+ Fake "[| evs: ns_shared; B ~= Spy;
+ X: synth (analz (sees Spy evs)) |]
+ ==> Says Spy B X # evs : ns_shared"
(*Alice initiates a protocol run, requesting to talk to any B*)
- NS1 "[| evs: ns_shared lost; A ~= Server; Nonce NA ~: used evs |]
+ NS1 "[| evs: ns_shared; A ~= Server; Nonce NA ~: used evs |]
==> Says A Server {|Agent A, Agent B, Nonce NA|} # evs
- : ns_shared lost"
+ : ns_shared"
(*Server's response to Alice's message.
!! It may respond more than once to A's request !!
Server doesn't know who the true sender is, hence the A' in
the sender field.*)
- NS2 "[| evs: ns_shared lost; A ~= B; A ~= Server; Key KAB ~: used evs;
+ NS2 "[| evs: ns_shared; A ~= B; A ~= Server; Key KAB ~: used evs;
Says A' Server {|Agent A, Agent B, Nonce NA|} : set evs |]
==> Says Server A
(Crypt (shrK A)
{|Nonce NA, Agent B, Key KAB,
(Crypt (shrK B) {|Key KAB, Agent A|})|})
- # evs : ns_shared lost"
+ # evs : ns_shared"
(*We can't assume S=Server. Agent A "remembers" her nonce.
Can inductively show A ~= Server*)
- NS3 "[| evs: ns_shared lost; A ~= B;
+ NS3 "[| evs: ns_shared; A ~= B;
Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
: set evs;
Says A Server {|Agent A, Agent B, Nonce NA|} : set evs |]
- ==> Says A B X # evs : ns_shared lost"
+ ==> Says A B X # evs : ns_shared"
(*Bob's nonce exchange. He does not know who the message came
from, but responds to A because she is mentioned inside.*)
- NS4 "[| evs: ns_shared lost; A ~= B; Nonce NB ~: used evs;
+ NS4 "[| evs: ns_shared; A ~= B; Nonce NB ~: used evs;
Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set evs |]
==> Says B A (Crypt K (Nonce NB)) # evs
- : ns_shared lost"
+ : ns_shared"
(*Alice responds with Nonce NB if she has seen the key before.
Maybe should somehow check Nonce NA again.
We do NOT send NB-1 or similar as the Spy cannot spoof such things.
Letting the Spy add or subtract 1 lets him send ALL nonces.
Instead we distinguish the messages by sending the nonce twice.*)
- NS5 "[| evs: ns_shared lost; A ~= B;
+ NS5 "[| evs: ns_shared; A ~= B;
Says B' A (Crypt K (Nonce NB)) : set evs;
Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
: set evs |]
- ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) # evs : ns_shared lost"
+ ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) # evs : ns_shared"
(*This message models possible leaks of session keys.
The two Nonces identify the protocol run: the rule insists upon
the true senders in order to make them accurate.*)
- Oops "[| evs: ns_shared lost; A ~= Spy;
+ Oops "[| evs: ns_shared; A ~= Spy;
Says B A (Crypt K (Nonce NB)) : set evs;
Says Server A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
: set evs |]
- ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : ns_shared lost"
+ ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : ns_shared"
end
--- a/src/HOL/Auth/OtwayRees.ML Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/OtwayRees.ML Mon Jul 14 12:47:21 1997 +0200
@@ -17,14 +17,11 @@
proof_timing:=true;
HOL_quantifiers := false;
-(*Replacing the variable by a constant improves search speed by 50%!*)
-val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy;
-
(*A "possibility property": there are traces that reach the end*)
goal thy
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
-\ ==> EX K. EX NA. EX evs: otway lost. \
+\ ==> EX K. EX NA. EX evs: otway. \
\ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
\ : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -36,7 +33,7 @@
(**** Inductive proofs about otway ****)
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set evs";
+goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs";
by (etac otway.induct 1);
by (Auto_tac());
qed_spec_mp "not_Says_to_self";
@@ -47,17 +44,17 @@
(** 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 lost Spy evs)";
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
+\ ==> X : analz (sees Spy evs)";
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "OR2_analz_sees_Spy";
goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
-\ ==> X : analz (sees lost Spy evs)";
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
+\ ==> X : analz (sees Spy evs)";
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "OR4_analz_sees_Spy";
goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
-\ ==> K : parts (sees lost Spy evs)";
+\ ==> K : parts (sees Spy evs)";
by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
qed "Oops_parts_sees_Spy";
@@ -71,42 +68,36 @@
bind_thm ("OR4_parts_sees_Spy",
OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
- We instantiate the variable to "lost" since leaving it as a Var would
- interfere with simplification.*)
-val parts_induct_tac =
- let val tac = forw_inst_tac [("lost","lost")]
- in etac otway.induct 1 THEN
- tac OR2_parts_sees_Spy 4 THEN
- tac OR4_parts_sees_Spy 6 THEN
- tac Oops_parts_sees_Spy 7 THEN
- prove_simple_subgoals_tac 1
- end;
+(*For proving the easier theorems about X ~: parts (sees Spy 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
+ prove_simple_subgoals_tac i;
-(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
+(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
sends messages containing X! **)
(*Spy never sees another agent's shared key! (unless it's lost at start)*)
goal thy
- "!!evs. evs : otway lost \
-\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by parts_induct_tac;
+ "!!evs. evs : otway ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (Blast_tac 1);
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
goal thy
- "!!evs. evs : otway lost \
-\ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
+ "!!evs. evs : otway ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
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 lost Spy evs); \
-\ evs : otway lost |] ==> A:lost";
+goal thy "!!A. [| Key (shrK A) : parts (sees Spy evs); \
+\ evs : otway |] ==> A:lost";
by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
qed "Spy_see_shrK_D";
@@ -115,9 +106,9 @@
(*Nobody can have used non-existent keys!*)
-goal thy "!!evs. evs : otway lost ==> \
-\ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
-by parts_induct_tac;
+goal thy "!!evs. evs : otway ==> \
+\ Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
+by (parts_induct_tac 1);
(*Fake*)
by (best_tac
(!claset addIs [impOfSubs analz_subset_parts]
@@ -140,9 +131,8 @@
(*Describes the form of K and NA when the Server sends this message. Also
for Oops case.*)
goal thy
- "!!evs. [| Says Server B \
-\ {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
-\ evs : otway lost |] \
+ "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
+\ evs : otway |] \
\ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
by (etac rev_mp 1);
by (etac otway.induct 1);
@@ -151,11 +141,11 @@
qed "Says_Server_message_form";
-(*For proofs involving analz. We again instantiate the variable to "lost".*)
+(*For proofs involving analz.*)
val analz_sees_tac =
- dres_inst_tac [("lost","lost")] OR2_analz_sees_Spy 4 THEN
- dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
- forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
+ dtac OR2_analz_sees_Spy 4 THEN
+ dtac OR4_analz_sees_Spy 6 THEN
+ forward_tac [Says_Server_message_form] 7 THEN
assume_tac 7 THEN
REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
@@ -163,8 +153,8 @@
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
- Key K : analz (sees lost Spy evs)
+ Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
+ Key K : analz (sees Spy evs)
A more general formula must be proved inductively.
****)
@@ -174,10 +164,10 @@
(*The equality makes the induction hypothesis easier to apply*)
goal thy
- "!!evs. evs : otway lost ==> \
-\ ALL K KK. KK <= Compl (range shrK) --> \
-\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
-\ (K : KK | Key K : analz (sees lost Spy evs))";
+ "!!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))";
by (etac otway.induct 1);
by analz_sees_tac;
by (REPEAT_FIRST (resolve_tac [allI, impI]));
@@ -191,9 +181,9 @@
goal thy
- "!!evs. [| evs : otway lost; KAB ~: range shrK |] ==> \
-\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
-\ (K = KAB | Key K : analz (sees lost Spy evs))";
+ "!!evs. [| evs : otway; KAB ~: range shrK |] ==> \
+\ Key K : analz (insert (Key KAB) (sees Spy evs)) = \
+\ (K = KAB | Key K : analz (sees Spy evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
qed "analz_insert_freshK";
@@ -201,7 +191,7 @@
(*** The Key K uniquely identifies the Server's message. **)
goal thy
- "!!evs. evs : otway lost ==> \
+ "!!evs. evs : otway ==> \
\ EX B' NA' NB' X'. ALL B NA NB X. \
\ Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs --> \
\ B=B' & NA=NA' & NB=NB' & X=X'";
@@ -223,7 +213,7 @@
\ : set evs; \
\ Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \
\ : set evs; \
-\ evs : otway lost |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
+\ evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
by (prove_unique_tac lemma 1);
qed "unique_session_keys";
@@ -233,13 +223,13 @@
(*Only OR1 can have caused such a part of a message to appear.*)
goal thy
- "!!evs. [| A ~: lost; evs : otway lost |] \
+ "!!evs. [| A ~: lost; evs : otway |] \
\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \
-\ : parts (sees lost Spy evs) --> \
+\ : parts (sees Spy evs) --> \
\ Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
\ : set evs";
-by parts_induct_tac;
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
qed_spec_mp "Crypt_imp_OR1";
@@ -247,11 +237,11 @@
(** The Nonce NA uniquely identifies A's message. **)
goal thy
- "!!evs. [| evs : otway lost; A ~: lost |] \
-\ ==> EX B'. ALL B. \
-\ Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (sees lost Spy evs) \
+ "!!evs. [| evs : otway; A ~: lost |] \
+\ ==> EX B'. ALL B. \
+\ Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (sees Spy evs) \
\ --> B = B'";
-by parts_induct_tac;
+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*)
@@ -260,9 +250,9 @@
val lemma = result();
goal thy
- "!!evs.[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts(sees lost Spy evs); \
-\ Crypt (shrK A) {|NA, Agent A, Agent C|}: parts(sees lost Spy evs); \
-\ evs : otway lost; A ~: lost |] \
+ "!!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 |] \
\ ==> B = C";
by (prove_unique_tac lemma 1);
qed "unique_NA";
@@ -272,12 +262,12 @@
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 lost |] \
-\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \
-\ : parts (sees lost Spy evs) --> \
-\ Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \
-\ ~: parts (sees lost Spy evs)";
-by parts_induct_tac;
+ "!!evs. [| A ~: lost; evs : otway |] \
+\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \
+\ : parts (sees Spy evs) --> \
+\ Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \
+\ ~: parts (sees Spy evs)";
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (REPEAT (blast_tac (!claset addSEs sees_Spy_partsEs
addSDs [impOfSubs parts_insert_subset_Un]) 1));
@@ -287,8 +277,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 lost |] \
-\ ==> Crypt (shrK A) {|NA, Key K|} : parts (sees lost Spy evs) \
+ "!!evs. [| A ~: lost; A ~= Spy; evs : otway |] \
+\ ==> Crypt (shrK A) {|NA, Key K|} : parts (sees Spy evs) \
\ --> Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
\ : set evs --> \
@@ -297,7 +287,7 @@
\ Crypt (shrK A) {|NA, Key K|}, \
\ Crypt (shrK B) {|NB, Key K|}|} \
\ : set evs)";
-by parts_induct_tac;
+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);
@@ -311,10 +301,10 @@
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_sees_Spy 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_sees_Spy RS parts.Inj]
addSEs [MPair_parts]
addIs [unique_NA]) 1);
qed_spec_mp "NA_Crypt_imp_Server_msg";
@@ -330,7 +320,7 @@
\ Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
\ : set evs; \
-\ A ~: lost; A ~= Spy; evs : otway lost |] \
+\ A ~: lost; A ~= Spy; evs : otway |] \
\ ==> EX NB. Says Server B \
\ {|NA, \
\ Crypt (shrK A) {|NA, Key K|}, \
@@ -346,12 +336,12 @@
the premises, e.g. by having A=Spy **)
goal thy
- "!!evs. [| A ~: lost; B ~: lost; evs : otway lost |] \
-\ ==> 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 lost Spy evs)";
+ "!!evs. [| A ~: lost; B ~: lost; 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)";
by (etac otway.induct 1);
by analz_sees_tac;
by (ALLGOALS
@@ -371,12 +361,12 @@
val lemma = result() RS mp RS mp RSN(2,rev_notE);
goal thy
- "!!evs. [| Says Server B \
-\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
-\ Crypt (shrK B) {|NB, Key K|}|} : set evs; \
-\ Says B Spy {|NA, NB, Key K|} ~: set evs; \
-\ A ~: lost; B ~: lost; evs : otway lost |] \
-\ ==> Key K ~: analz (sees lost Spy evs)";
+ "!!evs. [| Says Server B \
+\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
+\ Crypt (shrK B) {|NB, Key K|}|} : set evs; \
+\ Says B Spy {|NA, NB, Key K|} ~: set evs; \
+\ A ~: lost; B ~: lost; evs : otway |] \
+\ ==> Key K ~: analz (sees Spy 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";
@@ -387,14 +377,14 @@
(*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 lost |] \
+ "!!evs. [| B ~: lost; evs : otway |] \
\ ==> Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \
-\ : parts (sees lost Spy evs) --> \
+\ : parts (sees Spy evs) --> \
\ (EX X. Says B Server \
\ {|NA, Agent A, Agent B, X, \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \
\ : set evs)";
-by parts_induct_tac;
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (ALLGOALS Blast_tac);
bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE);
@@ -403,11 +393,11 @@
(** The Nonce NB uniquely identifies B's message. **)
goal thy
- "!!evs. [| evs : otway lost; B ~: lost |] \
+ "!!evs. [| evs : otway; B ~: lost |] \
\ ==> EX NA' A'. ALL NA A. \
-\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(sees lost Spy evs) \
+\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(sees Spy evs) \
\ --> NA = NA' & A = A'";
-by parts_induct_tac;
+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*)
@@ -417,10 +407,10 @@
goal thy
"!!evs.[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \
-\ : parts(sees lost Spy evs); \
+\ : parts(sees Spy evs); \
\ Crypt (shrK B) {|NC, NB, Agent C, Agent B|} \
-\ : parts(sees lost Spy evs); \
-\ evs : otway lost; B ~: lost |] \
+\ : parts(sees Spy evs); \
+\ evs : otway; B ~: lost |] \
\ ==> NC = NA & C = A";
by (prove_unique_tac lemma 1);
qed "unique_NB";
@@ -429,8 +419,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 lost |] \
-\ ==> Crypt (shrK B) {|NB, Key K|} : parts (sees lost Spy evs) \
+ "!!evs. [| B ~: lost; B ~= Spy; evs : otway |] \
+\ ==> Crypt (shrK B) {|NB, Key K|} : parts (sees Spy evs) \
\ --> (ALL X'. Says B Server \
\ {|NA, Agent A, Agent B, X', \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \
@@ -439,7 +429,7 @@
\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
\ Crypt (shrK B) {|NB, Key K|}|} \
\ : set evs)";
-by parts_induct_tac;
+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);
@@ -448,11 +438,11 @@
(*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_sees_Spy 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_sees_Spy RS parts.Inj]
delrules [conjI, impCE] (*stop split-up*)) 1);
qed_spec_mp "NB_Crypt_imp_Server_msg";
@@ -460,7 +450,7 @@
(*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 lost; \
+ "!!evs. [| B ~: lost; 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', \
@@ -480,16 +470,16 @@
goal thy
- "!!evs. [| B ~: lost; evs : otway lost |] \
-\ ==> Says Server B \
-\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
-\ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \
-\ (EX X. Says B Server {|NA, Agent A, Agent B, X, \
+ "!!evs. [| B ~: lost; evs : otway |] \
+\ ==> Says Server B \
+\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
+\ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \
+\ (EX X. Says B Server {|NA, Agent A, Agent B, X, \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
\ : 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_sees_Spy 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);
@@ -502,7 +492,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 lost |] \
+\ A ~: lost; A ~= Spy; B ~: lost; 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 Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/OtwayRees.thy Mon Jul 14 12:47:21 1997 +0200
@@ -14,40 +14,40 @@
OtwayRees = Shared +
-consts otway :: agent set => event list set
-inductive "otway lost"
+consts otway :: event list set
+inductive "otway"
intrs
(*Initial trace is empty*)
- Nil "[]: otway lost"
+ Nil "[]: otway"
(*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 lost; B ~= Spy;
- X: synth (analz (sees lost Spy evs)) |]
- ==> Says Spy B X # evs : otway lost"
+ Fake "[| evs: otway; B ~= Spy;
+ X: synth (analz (sees Spy evs)) |]
+ ==> Says Spy B X # evs : otway"
(*Alice initiates a protocol run*)
- OR1 "[| evs: otway lost; A ~= B; B ~= Server; Nonce NA ~: used evs |]
+ OR1 "[| evs: otway; A ~= B; B ~= Server; Nonce NA ~: used evs |]
==> Says A B {|Nonce NA, Agent A, Agent B,
Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |}
- # evs : otway lost"
+ # evs : otway"
(*Bob's response to Alice's message. Bob doesn't know who
the sender is, hence the A' in the sender field.
Note that NB is encrypted.*)
- OR2 "[| evs: otway lost; B ~= Server; Nonce NB ~: used evs;
+ OR2 "[| evs: otway; B ~= Server; Nonce NB ~: used evs;
Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs |]
==> Says B Server
{|Nonce NA, Agent A, Agent B, X,
Crypt (shrK B)
{|Nonce NA, Nonce NB, Agent A, Agent B|}|}
- # evs : otway lost"
+ # evs : otway"
(*The Server receives Bob's message and checks that the three NAs
match. Then he sends a new session key to Bob with a packet for
forwarding to Alice.*)
- OR3 "[| evs: otway lost; B ~= Server; Key KAB ~: used evs;
+ OR3 "[| evs: otway; B ~= Server; Key KAB ~: used evs;
Says B' Server
{|Nonce NA, Agent A, Agent B,
Crypt (shrK A) {|Nonce NA, Agent A, Agent B|},
@@ -57,24 +57,24 @@
{|Nonce NA,
Crypt (shrK A) {|Nonce NA, Key KAB|},
Crypt (shrK B) {|Nonce NB, Key KAB|}|}
- # evs : otway lost"
+ # evs : otway"
(*Bob receives the Server's (?) message and compares the Nonces with
those in the message he previously sent the Server.*)
- OR4 "[| evs: otway lost; A ~= B;
+ OR4 "[| evs: otway; A ~= B;
Says B Server {|Nonce NA, Agent A, Agent B, X',
Crypt (shrK B)
{|Nonce NA, Nonce NB, Agent A, Agent B|}|}
: set evs;
Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
: set evs |]
- ==> Says B A {|Nonce NA, X|} # evs : otway lost"
+ ==> Says B A {|Nonce NA, X|} # evs : otway"
(*This message models possible leaks of session keys. The nonces
identify the protocol run.*)
- Oops "[| evs: otway lost; B ~= Spy;
+ Oops "[| evs: otway; B ~= Spy;
Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
: set evs |]
- ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost"
+ ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway"
end
--- a/src/HOL/Auth/OtwayRees_AN.ML Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML Mon Jul 14 12:47:21 1997 +0200
@@ -21,7 +21,7 @@
(*A "possibility property": there are traces that reach the end*)
goal thy
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
-\ ==> EX K. EX NA. EX evs: otway lost. \
+\ ==> EX K. EX NA. EX evs: otway. \
\ Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
\ : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -33,7 +33,7 @@
(**** Inductive proofs about otway ****)
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set evs";
+goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs";
by (etac otway.induct 1);
by (Auto_tac());
qed_spec_mp "not_Says_to_self";
@@ -44,12 +44,12 @@
(** For reasoning about the encrypted portion of messages **)
goal thy "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \
-\ X : analz (sees lost Spy evs)";
+\ X : analz (sees Spy evs)";
by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "OR4_analz_sees_Spy";
goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
-\ : set evs ==> K : parts (sees lost Spy evs)";
+\ : set evs ==> K : parts (sees Spy evs)";
by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
qed "Oops_parts_sees_Spy";
@@ -60,40 +60,34 @@
bind_thm ("OR4_parts_sees_Spy",
OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
- We instantiate the variable to "lost" since leaving it as a Var would
- interfere with simplification.*)
-val parts_induct_tac =
- let val tac = forw_inst_tac [("lost","lost")]
- in etac otway.induct 1 THEN
- tac OR4_parts_sees_Spy 6 THEN
- tac Oops_parts_sees_Spy 7 THEN
- prove_simple_subgoals_tac 1
- end;
+(*For proving the easier theorems about X ~: parts (sees Spy 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
+ prove_simple_subgoals_tac i;
-(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
+(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
sends messages containing X! **)
(*Spy never sees another agent's shared key! (unless it's lost at start)*)
goal thy
- "!!evs. evs : otway lost \
-\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by parts_induct_tac;
+ "!!evs. evs : otway ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (Blast_tac 1);
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
goal thy
- "!!evs. evs : otway lost \
-\ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
+ "!!evs. evs : otway ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
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 lost Spy evs); \
-\ evs : otway lost |] ==> A:lost";
+goal thy "!!A. [| Key (shrK A) : parts (sees Spy evs); \
+\ evs : otway |] ==> A:lost";
by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
qed "Spy_see_shrK_D";
@@ -102,9 +96,9 @@
(*Nobody can have used non-existent keys!*)
-goal thy "!!evs. evs : otway lost ==> \
-\ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
-by parts_induct_tac;
+goal thy "!!evs. evs : otway ==> \
+\ Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
+by (parts_induct_tac 1);
(*Fake*)
by (best_tac
(!claset addIs [impOfSubs analz_subset_parts]
@@ -131,7 +125,7 @@
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
\ : set evs; \
-\ evs : otway lost |] \
+\ evs : otway |] \
\ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
by (etac rev_mp 1);
by (etac otway.induct 1);
@@ -140,10 +134,10 @@
qed "Says_Server_message_form";
-(*For proofs involving analz. We again instantiate the variable to "lost".*)
+(*For proofs involving analz.*)
val analz_sees_tac =
- dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
- forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
+ dtac OR4_analz_sees_Spy 6 THEN
+ forward_tac [Says_Server_message_form] 7 THEN
assume_tac 7 THEN
REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
@@ -151,8 +145,8 @@
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
- Key K : analz (sees lost Spy evs)
+ Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
+ Key K : analz (sees Spy evs)
A more general formula must be proved inductively.
****)
@@ -162,10 +156,10 @@
(*The equality makes the induction hypothesis easier to apply*)
goal thy
- "!!evs. evs : otway lost ==> \
-\ ALL K KK. KK <= Compl (range shrK) --> \
-\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
-\ (K : KK | Key K : analz (sees lost Spy evs))";
+ "!!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))";
by (etac otway.induct 1);
by analz_sees_tac;
by (REPEAT_FIRST (resolve_tac [allI, impI]));
@@ -179,9 +173,9 @@
goal thy
- "!!evs. [| evs : otway lost; KAB ~: range shrK |] ==> \
-\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
-\ (K = KAB | Key K : analz (sees lost Spy evs))";
+ "!!evs. [| evs : otway; KAB ~: range shrK |] ==> \
+\ Key K : analz (insert (Key KAB) (sees Spy evs)) = \
+\ (K = KAB | Key K : analz (sees Spy evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
qed "analz_insert_freshK";
@@ -189,7 +183,7 @@
(*** The Key K uniquely identifies the Server's message. **)
goal thy
- "!!evs. evs : otway lost ==> \
+ "!!evs. evs : otway ==> \
\ EX A' B' NA' NB'. ALL A B NA NB. \
\ Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, K|}, \
@@ -218,7 +212,7 @@
\ {|Crypt (shrK A') {|NA', Agent A', Agent B', K|}, \
\ Crypt (shrK B') {|NB', Agent A', Agent B', K|}|} \
\ : set evs; \
-\ evs : otway lost |] \
+\ evs : otway |] \
\ ==> A=A' & B=B' & NA=NA' & NB=NB'";
by (prove_unique_tac lemma 1);
qed "unique_session_keys";
@@ -229,14 +223,14 @@
(*If the encrypted message appears then it originated with the Server!*)
goal thy
- "!!evs. [| A ~: lost; evs : otway lost |] \
-\ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} \
-\ : parts (sees lost Spy evs) \
+ "!!evs. [| A ~: lost; evs : otway |] \
+\ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} \
+\ : parts (sees Spy 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|}|} \
\ : set evs)";
-by parts_induct_tac;
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
(*OR3*)
@@ -249,7 +243,7 @@
goal thy
"!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \
\ : set evs; \
-\ A ~: lost; evs : otway lost |] \
+\ A ~: lost; 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|}|} \
@@ -264,13 +258,13 @@
the premises, e.g. by having A=Spy **)
goal thy
- "!!evs. [| A ~: lost; B ~: lost; evs : otway lost |] \
+ "!!evs. [| A ~: lost; B ~: lost; 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 lost Spy evs)";
+\ Key K ~: analz (sees Spy evs)";
by (etac otway.induct 1);
by analz_sees_tac;
by (ALLGOALS
@@ -295,8 +289,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 lost |] \
-\ ==> Key K ~: analz (sees lost Spy evs)";
+\ A ~: lost; B ~: lost; evs : otway |] \
+\ ==> Key K ~: analz (sees Spy 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";
@@ -306,14 +300,14 @@
(*If the encrypted message appears then it originated with the Server!*)
goal thy
- "!!evs. [| B ~: lost; evs : otway lost |] \
-\ ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} \
-\ : parts (sees lost Spy evs) \
+ "!!evs. [| B ~: lost; evs : otway |] \
+\ ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} \
+\ : parts (sees Spy 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|}|} \
\ : set evs)";
-by parts_induct_tac;
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
(*OR3*)
@@ -324,7 +318,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 lost; \
+ "!!evs. [| B ~: lost; evs : otway; \
\ Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
\ : set evs |] \
\ ==> EX NA. Says Server B \
--- a/src/HOL/Auth/OtwayRees_AN.thy Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.thy Mon Jul 14 12:47:21 1997 +0200
@@ -19,55 +19,55 @@
OtwayRees_AN = Shared +
-consts otway :: agent set => event list set
-inductive "otway lost"
+consts otway :: event list set
+inductive "otway"
intrs
(*Initial trace is empty*)
- Nil "[]: otway lost"
+ Nil "[]: otway"
(*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 lost; B ~= Spy;
- X: synth (analz (sees lost Spy evs)) |]
- ==> Says Spy B X # evs : otway lost"
+ Fake "[| evs: otway; B ~= Spy;
+ X: synth (analz (sees Spy evs)) |]
+ ==> Says Spy B X # evs : otway"
(*Alice initiates a protocol run*)
- OR1 "[| evs: otway lost; A ~= B; B ~= Server |]
- ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs : otway lost"
+ OR1 "[| evs: otway; A ~= B; B ~= Server |]
+ ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs : otway"
(*Bob's response to Alice's message. Bob doesn't know who
the sender is, hence the A' in the sender field.*)
- OR2 "[| evs: otway lost; B ~= Server;
+ OR2 "[| evs: otway; B ~= Server;
Says A' B {|Agent A, Agent B, Nonce NA|} : set evs |]
==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
- # evs : otway lost"
+ # evs : otway"
(*The Server receives Bob's message. Then he sends a new
session key to Bob with a packet for forwarding to Alice.*)
- OR3 "[| evs: otway lost; B ~= Server; A ~= B; Key KAB ~: used evs;
+ OR3 "[| evs: otway; B ~= Server; A ~= B; Key KAB ~: used evs;
Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
: set evs |]
==> Says Server B
{|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key KAB|},
Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key KAB|}|}
- # evs : otway lost"
+ # evs : otway"
(*Bob receives the Server's (?) message and compares the Nonces with
those in the message he previously sent the Server.*)
- OR4 "[| evs: otway lost; A ~= B;
+ OR4 "[| evs: otway; A ~= B;
Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} : set evs;
Says S' B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
: set evs |]
- ==> Says B A X # evs : otway lost"
+ ==> Says B A X # evs : otway"
(*This message models possible leaks of session keys. The nonces
identify the protocol run. B is not assumed to know shrK A.*)
- Oops "[| evs: otway lost; B ~= Spy;
+ Oops "[| evs: otway; B ~= Spy;
Says Server B
{|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|},
Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|}
: set evs |]
- ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost"
+ ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway"
end
--- a/src/HOL/Auth/OtwayRees_Bad.ML Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Mon Jul 14 12:47:21 1997 +0200
@@ -20,9 +20,6 @@
proof_timing:=true;
HOL_quantifiers := false;
-(*Replacing the variable by a constant improves search speed by 50%!*)
-val Says_imp_sees_Spy' =
- read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
(*A "possibility property": there are traces that reach the end*)
goal thy
@@ -50,17 +47,17 @@
(** 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 lost Spy evs)";
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
+\ X : analz (sees Spy evs)";
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "OR2_analz_sees_Spy";
goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs ==> \
-\ X : analz (sees lost Spy evs)";
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
+\ X : analz (sees Spy evs)";
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "OR4_analz_sees_Spy";
goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
-\ ==> K : parts (sees lost Spy evs)";
+\ ==> K : parts (sees Spy evs)";
by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
qed "Oops_parts_sees_Spy";
@@ -74,36 +71,34 @@
bind_thm ("OR4_parts_sees_Spy",
OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
-val parts_induct_tac =
- etac otway.induct 1 THEN
- forward_tac [OR2_parts_sees_Spy] 4 THEN
- forward_tac [OR4_parts_sees_Spy] 6 THEN
- forward_tac [Oops_parts_sees_Spy] 7 THEN
- prove_simple_subgoals_tac 1;
+(*For proving the easier theorems about X ~: parts (sees Spy 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
+ prove_simple_subgoals_tac i;
-(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
+(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
sends messages containing X! **)
(*Spy never sees another agent's shared key! (unless it's lost at start)*)
goal thy
- "!!evs. evs : otway \
-\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by parts_induct_tac;
+ "!!evs. evs : otway ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (Blast_tac 1);
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
goal thy
- "!!evs. evs : otway \
-\ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
+ "!!evs. evs : otway ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
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 lost Spy evs); \
+goal thy "!!A. [| Key (shrK A) : parts (sees Spy evs); \
\ evs : otway |] ==> A:lost";
by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
qed "Spy_see_shrK_D";
@@ -114,8 +109,8 @@
(*Nobody can have used non-existent keys!*)
goal thy "!!evs. evs : otway ==> \
-\ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
-by parts_induct_tac;
+\ Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
+by (parts_induct_tac 1);
(*Fake*)
by (best_tac
(!claset addIs [impOfSubs analz_subset_parts]
@@ -161,8 +156,8 @@
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
- Key K : analz (sees lost Spy evs)
+ Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
+ Key K : analz (sees Spy evs)
A more general formula must be proved inductively.
****)
@@ -172,10 +167,10 @@
(*The equality makes the induction hypothesis easier to apply*)
goal thy
- "!!evs. evs : otway ==> \
-\ ALL K KK. KK <= Compl (range shrK) --> \
-\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
-\ (K : KK | Key K : analz (sees lost Spy evs))";
+ "!!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))";
by (etac otway.induct 1);
by analz_sees_tac;
by (REPEAT_FIRST (resolve_tac [allI, impI]));
@@ -189,9 +184,9 @@
goal thy
- "!!evs. [| evs : otway; KAB ~: range shrK |] ==> \
-\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
-\ (K = KAB | Key K : analz (sees lost Spy evs))";
+ "!!evs. [| evs : otway; KAB ~: range shrK |] ==> \
+\ Key K : analz (insert (Key KAB) (sees Spy evs)) = \
+\ (K = KAB | Key K : analz (sees Spy evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
qed "analz_insert_freshK";
@@ -231,7 +226,7 @@
\ {|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 lost Spy evs)";
+\ Key K ~: analz (sees Spy evs)";
by (etac otway.induct 1);
by analz_sees_tac;
by (ALLGOALS
@@ -256,7 +251,7 @@
\ 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 lost Spy evs)";
+\ ==> Key K ~: analz (sees Spy 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";
@@ -271,10 +266,10 @@
goal thy
"!!evs. [| A ~: lost; A ~= B; evs : otway |] \
\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \
-\ : parts (sees lost Spy evs) --> \
+\ : parts (sees Spy evs) --> \
\ Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs";
-by parts_induct_tac;
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (Blast_tac 1);
qed_spec_mp "Crypt_imp_OR1";
@@ -285,16 +280,16 @@
(*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 lost Spy evs) --> \
-\ Says A B {|NA, Agent A, Agent B, \
-\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
-\ : set evs --> \
-\ (EX B NB. Says Server B \
-\ {|NA, \
-\ Crypt (shrK A) {|NA, Key K|}, \
+ "!!evs. [| A ~: lost; A ~= Spy; evs : otway |] \
+\ ==> Crypt (shrK A) {|NA, Key K|} : parts (sees Spy evs) --> \
+\ Says A B {|NA, Agent A, Agent B, \
+\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
+\ : set evs --> \
+\ (EX B NB. Says Server B \
+\ {|NA, \
+\ Crypt (shrK A) {|NA, Key K|}, \
\ Crypt (shrK B) {|NB, Key K|}|} : set evs)";
-by parts_induct_tac;
+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]
--- a/src/HOL/Auth/OtwayRees_Bad.thy Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.thy Mon Jul 14 12:47:21 1997 +0200
@@ -12,8 +12,7 @@
OtwayRees_Bad = Shared +
-consts lost :: agent set (*No need for it to be a variable*)
- otway :: event list set
+consts otway :: event list set
inductive otway
intrs
@@ -23,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 lost Spy evs)) |]
+ Fake "[| evs: otway; B ~= Spy; X: synth (analz (sees Spy evs)) |]
==> Says Spy B X # evs : otway"
(*Alice initiates a protocol run*)
--- a/src/HOL/Auth/Public.ML Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/Public.ML Mon Jul 14 12:47:21 1997 +0200
@@ -37,7 +37,7 @@
(** Rewrites should not refer to initState(Friend i)
-- not in normal form! **)
-goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}";
+goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
by (agent.induct_tac "C" 1);
by (auto_tac (!claset addIs [range_eqI], !simpset));
qed "keysFor_parts_initState";
@@ -47,22 +47,22 @@
(*** Function "sees" ***)
(*Agents see their own private keys!*)
-goal thy "A ~= Spy --> Key (priK A) : sees lost A evs";
+goal thy "A ~= Spy --> Key (priK A) : sees A evs";
by (list.induct_tac "evs" 1);
by (agent.induct_tac "A" 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
qed_spec_mp "sees_own_priK";
(*All public keys are visible to all*)
-goal thy "Key (pubK A) : sees lost B evs";
+goal thy "Key (pubK A) : sees B evs";
by (list.induct_tac "evs" 1);
by (agent.induct_tac "B" 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
by (Auto_tac ());
qed_spec_mp "sees_pubK";
-(*Spy sees private keys of lost agents!*)
-goal thy "!!A. A: lost ==> Key (priK A) : sees lost Spy evs";
+(*Spy sees private keys of agents!*)
+goal thy "!!A. A: lost ==> Key (priK A) : sees Spy evs";
by (list.induct_tac "evs" 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
by (Blast_tac 1);
@@ -73,8 +73,8 @@
(*For not_lost_tac*)
-goal thy "!!A. [| Crypt (pubK A) X : analz (sees lost Spy evs); A: lost |] \
-\ ==> X : analz (sees lost Spy evs)";
+goal thy "!!A. [| Crypt (pubK A) X : analz (sees Spy evs); A: lost |] \
+\ ==> X : analz (sees Spy evs)";
by (blast_tac (!claset addSDs [analz.Decrypt]) 1);
qed "Crypt_Spy_analz_lost";
@@ -93,7 +93,7 @@
(*** Fresh nonces ***)
-goal thy "Nonce N ~: parts (initState lost B)";
+goal thy "Nonce N ~: parts (initState B)";
by (agent.induct_tac "B" 1);
by (Auto_tac ());
qed "Nonce_notin_initState";
--- a/src/HOL/Auth/Public.thy Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/Public.thy Mon Jul 14 12:47:21 1997 +0200
@@ -21,11 +21,11 @@
primrec initState agent
(*Agents know their private key and all public keys*)
- initState_Server "initState lost Server =
+ initState_Server "initState Server =
insert (Key (priK Server)) (Key `` range pubK)"
- initState_Friend "initState lost (Friend i) =
+ initState_Friend "initState (Friend i) =
insert (Key (priK (Friend i))) (Key `` range pubK)"
- initState_Spy "initState lost Spy =
+ initState_Spy "initState Spy =
(Key``invKey``pubK``lost) Un (Key `` range pubK)"
--- a/src/HOL/Auth/Recur.ML Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/Recur.ML Mon Jul 14 12:47:21 1997 +0200
@@ -22,7 +22,7 @@
(*Simplest case: Alice goes directly to the server*)
goal thy
"!!A. A ~= Server \
-\ ==> EX K NA. EX evs: recur lost. \
+\ ==> EX K NA. EX evs: recur. \
\ Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
\ Agent Server|} : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -35,7 +35,7 @@
(*Case two: Alice, Bob and the server*)
goal thy
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
-\ ==> EX K. EX NA. EX evs: recur lost. \
+\ ==> EX K. EX NA. EX evs: recur. \
\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
\ Agent Server|} : set evs";
by (cut_facts_tac [Nonce_supply2, Key_supply2] 1);
@@ -54,7 +54,7 @@
TOO SLOW to run every time!
goal thy
"!!A B. [| A ~= B; B ~= C; A ~= Server; B ~= Server; C ~= Server |] \
-\ ==> EX K. EX NA. EX evs: recur lost. \
+\ ==> EX K. EX NA. EX evs: recur. \
\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
\ Agent Server|} : set evs";
by (cut_facts_tac [Nonce_supply3, Key_supply3] 1);
@@ -75,7 +75,7 @@
(**** Inductive proofs about recur ****)
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs : recur lost ==> ALL A X. Says A A X ~: set evs";
+goal thy "!!evs. evs : recur ==> ALL A X. Says A A X ~: set evs";
by (etac recur.induct 1);
by (Auto_tac());
qed_spec_mp "not_Says_to_self";
@@ -115,7 +115,7 @@
val RA2_analz_sees_Spy = Says_imp_sees_Spy RS analz.Inj |> standard;
goal thy "!!evs. Says C' B {|Crypt K X, X', RA|} : set evs \
-\ ==> RA : analz (sees lost Spy evs)";
+\ ==> RA : analz (sees Spy evs)";
by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "RA4_analz_sees_Spy";
@@ -129,30 +129,25 @@
bind_thm ("RA4_parts_sees_Spy",
RA4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
- We instantiate the variable to "lost" since leaving it as a Var would
- interfere with simplification.*)
-val parts_induct_tac =
- let val tac = forw_inst_tac [("lost","lost")]
- in etac recur.induct 1 THEN
- tac RA2_parts_sees_Spy 4 THEN
- etac subst 4 (*RA2: DELETE needless definition of PA!*) THEN
- forward_tac [respond_imp_responses] 5 THEN
- tac RA4_parts_sees_Spy 6 THEN
- prove_simple_subgoals_tac 1
- end;
+(*For proving the easier theorems about X ~: parts (sees Spy evs).*)
+fun parts_induct_tac i =
+ etac recur.induct i THEN
+ forward_tac [RA2_parts_sees_Spy] (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
+ prove_simple_subgoals_tac i;
-(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
+(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
sends messages containing X! **)
-(** Spy never sees another agent's long-term key (unless initially lost) **)
+(** Spy never sees another agent's shared key! (unless it's lost at start) **)
goal thy
- "!!evs. evs : recur lost \
-\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by parts_induct_tac;
+ "!!evs. evs : recur ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (ALLGOALS
(asm_simp_tac (!simpset addsimps [parts_insert2, parts_insert_sees])));
@@ -164,14 +159,13 @@
Addsimps [Spy_see_shrK];
goal thy
- "!!evs. evs : recur lost \
-\ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
+ "!!evs. evs : recur ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
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 lost Spy evs); \
-\ evs : recur lost |] ==> A:lost";
+goal thy "!!A. [| Key (shrK A) : parts (sees Spy evs); \
+\ evs : recur |] ==> A:lost";
by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
qed "Spy_see_shrK_D";
@@ -191,9 +185,9 @@
qed_spec_mp "Key_in_keysFor_parts";
-goal thy "!!evs. evs : recur lost ==> \
-\ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
-by parts_induct_tac;
+goal thy "!!evs. evs : recur ==> \
+\ Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
+by (parts_induct_tac 1);
(*RA3*)
by (best_tac (!claset addDs [Key_in_keysFor_parts]
addss (!simpset addsimps [parts_insert_sees])) 2);
@@ -216,18 +210,18 @@
(*** Proofs involving analz ***)
-(*For proofs involving analz. We again instantiate the variable to "lost".*)
+(*For proofs involving analz.*)
val analz_sees_tac =
etac subst 4 (*RA2: DELETE needless definition of PA!*) THEN
- dres_inst_tac [("lost","lost")] RA2_analz_sees_Spy 4 THEN
+ dtac RA2_analz_sees_Spy 4 THEN
forward_tac [respond_imp_responses] 5 THEN
- dres_inst_tac [("lost","lost")] RA4_analz_sees_Spy 6;
+ dtac RA4_analz_sees_Spy 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 lost Spy evs")
+ Note that it holds for *any* set H (not just "sees Spy evs")
satisfying the inductive hypothesis.*)
goal thy
"!!evs. [| RB : responses evs; \
@@ -243,10 +237,10 @@
(*Version for the protocol. Proof is almost trivial, thanks to the lemma.*)
goal thy
- "!!evs. evs : recur lost ==> \
-\ ALL K KK. KK <= Compl (range shrK) --> \
-\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
-\ (K : KK | Key K : analz (sees lost Spy evs))";
+ "!!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))";
by (etac recur.induct 1);
by analz_sees_tac;
by (REPEAT_FIRST (resolve_tac [allI, impI]));
@@ -262,30 +256,30 @@
qed_spec_mp "analz_image_freshK";
-(*Instance of the lemma with H replaced by (sees lost Spy evs):
- [| RB : responses evs; evs : recur lost; |]
+(*Instance of the lemma with H replaced by (sees Spy evs):
+ [| RB : responses evs; evs : recur; |]
==> KK <= Compl (range shrK) -->
- Key K : analz (insert RB (Key``KK Un sees lost Spy evs)) =
- (K : KK | Key K : analz (insert RB (sees lost Spy evs)))
+ Key K : analz (insert RB (Key``KK Un sees Spy evs)) =
+ (K : KK | Key K : analz (insert RB (sees Spy evs)))
*)
bind_thm ("resp_analz_image_freshK",
raw_analz_image_freshK RSN
(2, resp_analz_image_freshK_lemma) RS spec RS spec);
goal thy
- "!!evs. [| evs : recur lost; KAB ~: range shrK |] ==> \
-\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
-\ (K = KAB | Key K : analz (sees lost Spy evs))";
+ "!!evs. [| evs : recur; KAB ~: range shrK |] ==> \
+\ Key K : analz (insert (Key KAB) (sees Spy evs)) = \
+\ (K = KAB | Key K : analz (sees Spy 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 lost Spy evs); \
-\ evs : recur lost; A ~: lost |] \
-\ ==> X : parts (sees lost Spy evs)";
+goal thy "!!evs. [| Hash {|Key(shrK A), X|} : parts (sees Spy evs); \
+\ evs : recur; A ~: lost |] \
+\ ==> X : parts (sees Spy evs)";
by (etac rev_mp 1);
-by parts_induct_tac;
+by (parts_induct_tac 1);
(*RA3 requires a further induction*)
by (etac responses.induct 2);
by (ALLGOALS Asm_simp_tac);
@@ -302,11 +296,11 @@
**)
goal thy
- "!!evs. [| evs : recur lost; A ~: lost |] \
+ "!!evs. [| evs : recur; A ~: lost |] \
\ ==> EX B' P'. ALL B P. \
-\ Hash {|Key(shrK A), Agent A, B, NA, P|} : parts (sees lost Spy evs) \
+\ Hash {|Key(shrK A), Agent A, B, NA, P|} : parts (sees Spy evs) \
\ --> B=B' & P=P'";
-by parts_induct_tac;
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (etac responses.induct 3);
by (ALLGOALS (simp_tac (!simpset addsimps [all_conj_distrib])));
@@ -319,9 +313,9 @@
val lemma = result();
goalw thy [HPair_def]
- "!!A.[| Hash[Key(shrK A)] {|Agent A, B,NA,P|} : parts(sees lost Spy evs); \
-\ Hash[Key(shrK A)] {|Agent A, B',NA,P'|} : parts(sees lost Spy evs); \
-\ evs : recur lost; A ~: lost |] \
+ "!!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 |] \
\ ==> B=B' & P=P'";
by (REPEAT (eresolve_tac partsEs 1));
by (prove_unique_tac lemma 1);
@@ -333,8 +327,8 @@
***)
goal thy
- "!!evs. [| RB : responses evs; evs : recur lost |] \
-\ ==> (Key (shrK B) : analz (insert RB (sees lost Spy evs))) = (B:lost)";
+ "!!evs. [| RB : responses evs; evs : recur |] \
+\ ==> (Key (shrK B) : analz (insert RB (sees Spy evs))) = (B:lost)";
by (etac responses.induct 1);
by (ALLGOALS
(asm_simp_tac
@@ -368,7 +362,7 @@
(*The Server does not send such messages. This theorem lets us avoid
assuming B~=Server in RA4.*)
goal thy
- "!!evs. evs : recur lost \
+ "!!evs. evs : recur \
\ ==> ALL C X Y. Says Server C {|X, Agent Server, Y|} ~: set evs";
by (etac recur.induct 1);
by (etac (respond.induct) 5);
@@ -399,8 +393,8 @@
by (expand_case_tac "K = KBC" 1);
by (dtac respond_Key_in_parts 1);
by (blast_tac (!claset addSIs [exI]
- addSEs partsEs
- addDs [Key_in_parts_respond]) 1);
+ addSEs partsEs
+ addDs [Key_in_parts_respond]) 1);
by (expand_case_tac "K = KAB" 1);
by (REPEAT (ares_tac [exI] 2));
by (ex_strip_tac 1);
@@ -422,10 +416,10 @@
the premises, e.g. by having A=Spy **)
goal thy
- "!!evs. [| (PB,RB,KAB) : respond evs; evs : recur lost |] \
+ "!!evs. [| (PB,RB,KAB) : respond evs; evs : recur |] \
\ ==> ALL A A' N. A ~: lost & A' ~: lost --> \
\ Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} --> \
-\ Key K ~: analz (insert RB (sees lost Spy evs))";
+\ Key K ~: analz (insert RB (sees Spy evs))";
by (etac respond.induct 1);
by (forward_tac [respond_imp_responses] 2);
by (forward_tac [respond_imp_not_used] 2);
@@ -450,10 +444,10 @@
goal thy
- "!!evs. [| Crypt (shrK A) {|Key K, Agent A', N|} \
-\ : parts (sees lost Spy evs); \
-\ A ~: lost; A' ~: lost; evs : recur lost |] \
-\ ==> Key K ~: analz (sees lost Spy evs)";
+ "!!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)";
by (etac rev_mp 1);
by (etac recur.induct 1);
by analz_sees_tac;
@@ -499,11 +493,11 @@
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 lost Spy evs); \
-\ A ~: lost; evs : recur lost |] \
+\ : parts (sees Spy evs); \
+\ A ~: lost; 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;
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
(*RA3*)
by (blast_tac (!claset addSDs [Hash_in_parts_respond]) 1);
@@ -516,12 +510,12 @@
(*Certificates can only originate with the Server.*)
goal thy
- "!!evs. [| Crypt (shrK A) Y : parts (sees lost Spy evs); \
-\ A ~: lost; A ~= Spy; evs : recur lost |] \
-\ ==> EX C RC. Says Server C RC : set evs & \
+ "!!evs. [| Crypt (shrK A) Y : parts (sees Spy evs); \
+\ A ~: lost; A ~= Spy; evs : recur |] \
+\ ==> EX C RC. Says Server C RC : set evs & \
\ Crypt (shrK A) Y : parts {RC}";
by (etac rev_mp 1);
-by parts_induct_tac;
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
(*RA4*)
by (Blast_tac 4);
--- a/src/HOL/Auth/Recur.thy Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/Recur.thy Mon Jul 14 12:47:21 1997 +0200
@@ -48,25 +48,25 @@
RA|} : responses evs"
-consts recur :: agent set => event list set
-inductive "recur lost"
+consts recur :: event list set
+inductive "recur"
intrs
(*Initial trace is empty*)
- Nil "[]: recur lost"
+ Nil "[]: recur"
(*The spy MAY say anything he CAN say. Common to
all similar protocols.*)
- Fake "[| evs: recur lost; B ~= Spy;
- X: synth (analz (sees lost Spy evs)) |]
- ==> Says Spy B X # evs : recur lost"
+ Fake "[| evs: recur; B ~= Spy;
+ X: synth (analz (sees Spy evs)) |]
+ ==> Says Spy B X # evs : recur"
(*Alice initiates a protocol run.
"Agent Server" is just a placeholder, to terminate the nesting.*)
- RA1 "[| evs: recur lost; A ~= B; A ~= Server; Nonce NA ~: used evs |]
+ RA1 "[| evs: recur; A ~= B; A ~= Server; Nonce NA ~: used evs |]
==> Says A B
(Hash[Key(shrK A)]
{|Agent A, Agent B, Nonce NA, Agent Server|})
- # evs : recur lost"
+ # evs : recur"
(*Bob's response to Alice's message. C might be the Server.
XA should be the Hash of the remaining components with KA, but
@@ -74,27 +74,27 @@
P is the previous recur message from Alice's caller.
NOTE: existing proofs don't need PA and are complicated by its
presence! See parts_Fake_tac.*)
- RA2 "[| evs: recur lost; B ~= C; B ~= Server; Nonce NB ~: used evs;
+ RA2 "[| evs: recur; B ~= C; B ~= Server; Nonce NB ~: used evs;
Says A' B PA : set evs;
PA = {|XA, Agent A, Agent B, Nonce NA, P|} |]
==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
- # evs : recur lost"
+ # evs : recur"
(*The Server receives Bob's message and prepares a response.*)
- RA3 "[| evs: recur lost; B ~= Server;
+ RA3 "[| evs: recur; B ~= Server;
Says B' Server PB : set evs;
(PB,RB,K) : respond evs |]
- ==> Says Server B RB # evs : recur lost"
+ ==> Says Server B RB # evs : recur"
(*Bob receives the returned message and compares the Nonces with
those in the message he previously sent the Server.*)
- RA4 "[| evs: recur lost; A ~= B;
+ RA4 "[| evs: recur; A ~= B;
Says B C {|XH, Agent B, Agent C, Nonce NB,
XA, Agent A, Agent B, Nonce NA, P|} : set evs;
Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|},
Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
RA|} : set evs |]
- ==> Says B A RA # evs : recur lost"
+ ==> Says B A RA # evs : recur"
(**No "oops" message can easily be expressed. Each session key is
associated--in two separate messages--with two nonces.
--- a/src/HOL/Auth/Shared.ML Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/Shared.ML Mon Jul 14 12:47:21 1997 +0200
@@ -22,7 +22,7 @@
(** Rewrites should not refer to initState(Friend i)
-- not in normal form! **)
-goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}";
+goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
by (agent.induct_tac "C" 1);
by (Auto_tac ());
qed "keysFor_parts_initState";
@@ -32,15 +32,15 @@
(*** Function "sees" ***)
(*Agents see their own shared keys!*)
-goal thy "A ~= Spy --> Key (shrK A) : sees lost A evs";
+goal thy "A ~= Spy --> Key (shrK A) : sees A evs";
by (list.induct_tac "evs" 1);
by (agent.induct_tac "A" 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
by (Blast_tac 1);
qed_spec_mp "sees_own_shrK";
-(*Spy sees shared keys of lost agents!*)
-goal thy "!!A. A: lost ==> Key (shrK A) : sees lost Spy evs";
+(*Spy sees shared keys of agents!*)
+goal thy "!!A. A: lost ==> Key (shrK A) : sees Spy evs";
by (list.induct_tac "evs" 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
by (Blast_tac 1);
@@ -49,8 +49,8 @@
AddSIs [sees_own_shrK, Spy_sees_lost];
(*For not_lost_tac*)
-goal thy "!!A. [| Crypt (shrK A) X : analz (sees lost Spy evs); A: lost |] \
-\ ==> X : analz (sees lost Spy evs)";
+goal thy "!!A. [| Crypt (shrK A) X : analz (sees Spy evs); A: lost |] \
+\ ==> X : analz (sees Spy evs)";
by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
qed "Crypt_Spy_analz_lost";
@@ -90,7 +90,7 @@
(*** Fresh nonces ***)
-goal thy "Nonce N ~: parts (initState lost B)";
+goal thy "Nonce N ~: parts (initState B)";
by (agent.induct_tac "B" 1);
by (Auto_tac ());
qed "Nonce_notin_initState";
--- a/src/HOL/Auth/Shared.thy Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/Shared.thy Mon Jul 14 12:47:21 1997 +0200
@@ -19,9 +19,9 @@
primrec initState agent
(*Server knows all long-term keys; other agents know only their own*)
- initState_Server "initState lost Server = Key `` range shrK"
- initState_Friend "initState lost (Friend i) = {Key (shrK (Friend i))}"
- initState_Spy "initState lost Spy = Key``shrK``lost"
+ initState_Server "initState Server = Key `` range shrK"
+ initState_Friend "initState (Friend i) = {Key (shrK (Friend i))}"
+ initState_Spy "initState Spy = Key``shrK``lost"
rules
--- a/src/HOL/Auth/TLS.ML Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/TLS.ML Mon Jul 14 12:47:21 1997 +0200
@@ -22,13 +22,30 @@
proof_timing:=true;
HOL_quantifiers := false;
-AddIffs [Spy_in_lost, Server_not_lost];
-Addsimps [certificate_def];
+(** We mostly DO NOT unfold the definition of "certificate". The attached
+ lemmas unfold it lazily, when "certificate B KB" occurs in appropriate
+ contexts.
+**)
+
+goalw thy [certificate_def]
+ "parts (insert (certificate B KB) H) = \
+\ parts (insert (Crypt (priK Server) {|Agent B, Key KB|}) H)";
+by (rtac refl 1);
+qed "parts_insert_certificate";
-goal thy "!!A. A ~: lost ==> A ~= Spy";
+goalw thy [certificate_def]
+ "analz (insert (certificate B KB) H) = \
+\ analz (insert (Crypt (priK Server) {|Agent B, Key KB|}) H)";
+by (rtac refl 1);
+qed "analz_insert_certificate";
+Addsimps [parts_insert_certificate, analz_insert_certificate];
+
+goalw thy [certificate_def]
+ "(X = certificate B KB) = (Crypt (priK Server) {|Agent B, Key KB|} = X)";
by (Blast_tac 1);
-qed "not_lost_not_eq_Spy";
-Addsimps [not_lost_not_eq_Spy];
+qed "eq_certificate_iff";
+AddIffs [eq_certificate_iff];
+
(*Injectiveness of key-generating functions*)
AddIffs [inj_clientK RS inj_eq, inj_serverK RS inj_eq];
@@ -38,11 +55,6 @@
isSym_serverK, rewrite_rule [isSymKey_def] isSym_serverK];
-(*Replacing the variable by a constant improves search speed by 50%!*)
-val Says_imp_sees_Spy' =
- read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
-
-
(*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***)
goal thy "pubK A ~= clientK arg";
@@ -102,11 +114,10 @@
(*And one for ClientFinished. Either FINISHED message may come first.*)
goal thy
- "!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls. \
-\ Says A B (Crypt (clientK(NA,NB,M)) \
-\ (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \
-\ Nonce NA, Agent XA, \
-\ certificate A (pubK A), \
+ "!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls. \
+\ Says A B (Crypt (clientK(NA,NB,M)) \
+\ (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \
+\ Nonce NA, Agent XA, certificate A (pubK A), \
\ Nonce NB, Agent XB, Agent B|})) : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
@@ -116,7 +127,7 @@
(*Another one, for CertVerify (which is optional)*)
goal thy
- "!!A B. A ~= B ==> EX NB M. EX evs: tls. \
+ "!!A B. A ~= B ==> EX NB M. EX evs: tls. \
\ Says A B (Crypt (priK A) \
\ (Hash{|Nonce NB, certificate B (pubK B), Nonce M|})) : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -137,28 +148,36 @@
AddSEs [not_Says_to_self RSN (2, rev_notE)];
-(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
+(*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)) *)
+fun parts_induct_tac i =
+ etac tls.induct i
+ THEN
+ REPEAT (FIRSTGOAL analz_mono_contra_tac)
+ THEN
+ fast_tac (!claset addss (!simpset)) i THEN
+ ALLGOALS (asm_full_simp_tac (!simpset setloop split_tac [expand_if]));
+
+
+(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
sends messages containing X! **)
(*Spy never sees another agent's private key! (unless it's lost at start)*)
goal thy
- "!!evs. evs : tls \
-\ ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)";
-by (etac tls.induct 1);
-by (prove_simple_subgoals_tac 1);
-by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 2);
+ "!!evs. evs : tls ==> (Key (priK A) : parts (sees Spy evs)) = (A : lost)";
+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 lost Spy evs)) = (A : lost)";
+ "!!evs. evs : tls ==> (Key (priK A) : analz (sees Spy evs)) = (A : lost)";
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 lost Spy evs); \
+goal thy "!!A. [| Key (priK A) : parts (sees Spy evs); \
\ evs : tls |] ==> A:lost";
by (blast_tac (!claset addDs [Spy_see_priK]) 1);
qed "Spy_see_priK_D";
@@ -168,22 +187,20 @@
(*This lemma says that no false certificates exist. One might extend the
- model to include bogus certificates for the lost agents, but there seems
+ model to include bogus certificates for the agents, but there seems
little point in doing so: the loss of their private keys is a worse
breach of security.*)
goalw thy [certificate_def]
"!!evs. evs : tls \
-\ ==> certificate B KB : parts (sees lost Spy evs) --> KB = pubK B";
-by (etac tls.induct 1);
-by (ALLGOALS (asm_full_simp_tac (!simpset setloop split_tac [expand_if])));
-by (Fake_parts_insert_tac 2);
-by (Blast_tac 1);
+\ ==> certificate B KB : parts (sees Spy 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));
(*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_sees_Spy RS parts.Inj RS
parts.Snd RS parts.Snd RS parts.Snd RS Server_cert_pubB]
THEN' assume_tac
THEN' hyp_subst_tac;
@@ -193,7 +210,6 @@
ClientCertKeyEx_tac (i+7) THEN (*ClientFinished*)
ClientCertKeyEx_tac (i+6) THEN (*CertVerify*)
ClientCertKeyEx_tac (i+5) THEN (*ClientCertKeyEx*)
- rewrite_goals_tac [certificate_def] THEN
ALLGOALS (asm_simp_tac
(!simpset addsimps [not_parts_not_analz]
setloop split_tac [expand_if])) THEN
@@ -207,36 +223,32 @@
(*** Hashing of nonces ***)
(*Every Nonce that's hashed is already in past traffic. *)
-goal thy "!!evs. [| Hash {|Nonce N, X|} : parts (sees lost Spy evs); \
+goal thy "!!evs. [| Hash {|Nonce N, X|} : parts (sees Spy evs); \
\ evs : tls |] \
-\ ==> Nonce N : parts (sees lost Spy evs)";
+\ ==> Nonce N : parts (sees Spy evs)";
by (etac rev_mp 1);
-by (etac tls.induct 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees]
- setloop split_tac [expand_if])));
-by (Fake_parts_insert_tac 2);
-by (REPEAT (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
- addSEs partsEs) 1));
+by (parts_induct_tac 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
+by (Fake_parts_insert_tac 1);
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
+ addSEs partsEs) 1);
qed "Hash_imp_Nonce1";
(*Lemma needed to prove Hash_Hash_imp_Nonce*)
goal thy "!!evs. [| Hash{|Nonce NA, Nonce NB, Nonce M|} \
-\ : parts (sees lost Spy evs); \
+\ : parts (sees Spy evs); \
\ evs : tls |] \
-\ ==> Nonce M : parts (sees lost Spy evs)";
+\ ==> Nonce M : parts (sees Spy evs)";
by (etac rev_mp 1);
-by (etac tls.induct 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees]
- setloop split_tac [expand_if])));
-by (Fake_parts_insert_tac 2);
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
- addSEs partsEs) 1);
+by (parts_induct_tac 1);
+by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 1);
+by (Fake_parts_insert_tac 1);
qed "Hash_imp_Nonce2";
AddSDs [Hash_imp_Nonce2];
goal thy "!!evs. [| Notes A {|Agent B, X|} : set evs; evs : tls |] \
-\ ==> Crypt (pubK B) X : parts (sees lost Spy evs)";
+\ ==> Crypt (pubK B) X : parts (sees Spy evs)";
by (etac rev_mp 1);
by (analz_induct_tac 1);
by (blast_tac (!claset addIs [parts_insertI]) 1);
@@ -245,17 +257,16 @@
(*NEEDED??*)
goal thy "!!evs. [| Hash {| Hash{|Nonce NA, Nonce NB, Nonce M|}, X |} \
-\ : parts (sees lost Spy evs); \
+\ : parts (sees Spy evs); \
\ evs : tls |] \
-\ ==> Nonce M : parts (sees lost Spy evs)";
+\ ==> Nonce M : parts (sees Spy evs)";
by (etac rev_mp 1);
-by (etac tls.induct 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees]
- setloop split_tac [expand_if])));
-by (Fake_parts_insert_tac 2);
-by (step_tac (!claset addSDs [Notes_Crypt_parts_sees,
- Says_imp_sees_Spy' RS parts.Inj]
- addSEs partsEs) 1);
+by (parts_induct_tac 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
+by (Fake_parts_insert_tac 1);
+by (REPEAT (blast_tac (!claset addSDs [Notes_Crypt_parts_sees,
+ Says_imp_sees_Spy RS parts.Inj]
+ addSEs partsEs) 1));
qed "Hash_Hash_imp_Nonce";
@@ -263,14 +274,13 @@
Every Nonce that's hashed is already in past traffic.
This general formulation is tricky to prove and hard to use, since the
2nd premise is typically proved by simplification.*)
-goal thy "!!evs. [| Hash X : parts (sees lost Spy evs); \
+goal thy "!!evs. [| Hash X : parts (sees Spy evs); \
\ Nonce N : parts {X}; evs : tls |] \
-\ ==> Nonce N : parts (sees lost Spy evs)";
+\ ==> Nonce N : parts (sees Spy evs)";
by (etac rev_mp 1);
-by (etac tls.induct 1);
-by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
+by (parts_induct_tac 1);
by (step_tac (!claset addSDs [Notes_Crypt_parts_sees,
- Says_imp_sees_Spy' RS parts.Inj]
+ Says_imp_sees_Spy RS parts.Inj]
addSEs partsEs) 1);
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [parts_insert_sees])));
by (Fake_parts_insert_tac 1);
@@ -285,16 +295,15 @@
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.*)
-goalw thy [certificate_def]
+goal thy
"!!evs. [| X = Crypt (priK A) \
\ (Hash{|Nonce NB, certificate B KB, Nonce M|}); \
\ evs : tls; A ~: lost; B ~= Spy |] \
\ ==> Says B A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|} \
\ : set evs --> \
-\ X : parts (sees lost Spy evs) --> Says A B X : set evs";
+\ X : parts (sees Spy evs) --> Says A B X : set evs";
by (hyp_subst_tac 1);
-by (etac tls.induct 1);
-by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
+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_imp_Nonce1]
@@ -305,25 +314,23 @@
(*If CERTIFICATE VERIFY is present then A has chosen M.*)
goal thy
"!!evs. [| Crypt (priK A) (Hash{|Nonce NB, certificate B KB, Nonce M|}) \
-\ : parts (sees lost Spy evs); \
+\ : parts (sees Spy evs); \
\ evs : tls; A ~: lost |] \
\ ==> Notes A {|Agent B, Nonce M|} : set evs";
be rev_mp 1;
-by (etac tls.induct 1);
-by (ALLGOALS (asm_full_simp_tac (!simpset setloop split_tac [expand_if])));
-by (Fake_parts_insert_tac 2);
-by (Blast_tac 1);
+by (parts_induct_tac 1);
+by (Fake_parts_insert_tac 1);
qed "UseCertVerify";
(*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 lost Spy evs))) = \
+\ ALL KK. (Key(priK B) : analz (Key``KK Un (sees Spy evs))) = \
\ (priK B : KK | B : lost)";
by (etac tls.induct 1);
by (ALLGOALS
- (asm_simp_tac (analz_image_keys_ss
+ (asm_simp_tac (analz_image_keys_ss
addsimps (certificate_def::keys_distinct))));
(*Fake*)
by (spy_analz_tac 2);
@@ -343,8 +350,8 @@
goal thy
"!!evs. evs : tls ==> \
\ ALL KK. KK <= (range clientK Un range serverK) --> \
-\ (Nonce N : analz (Key``KK Un (sees lost Spy evs))) = \
-\ (Nonce N : analz (sees lost Spy evs))";
+\ (Nonce N : analz (Key``KK Un (sees Spy evs))) = \
+\ (Nonce N : analz (sees Spy evs))";
by (etac tls.induct 1);
by (ClientCertKeyEx_tac 6);
by (REPEAT_FIRST (resolve_tac [allI, impI]));
@@ -352,8 +359,8 @@
writeln"SLOW simplification: 50 secs!??";
by (ALLGOALS
(asm_simp_tac (analz_image_keys_ss
- addsimps (analz_image_priK::certificate_def::
- keys_distinct))));
+ addsimps (analz_image_priK::certificate_def::
+ keys_distinct))));
by (ALLGOALS (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_priK])));
by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb])));
(*ClientCertKeyEx: a nonce is sent, but one needs a priK to read it.*)
@@ -369,7 +376,7 @@
goal thy
"!!evs. [| evs : tls; A ~: lost; B ~: lost |] \
\ ==> Notes A {|Agent B, Nonce M|} : set evs --> \
-\ Nonce M ~: analz (sees lost Spy evs)";
+\ Nonce M ~: analz (sees Spy evs)";
by (analz_induct_tac 1);
(*ClientHello*)
by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
@@ -382,7 +389,7 @@
by (REPEAT (blast_tac (!claset addSEs partsEs
addDs [Notes_Crypt_parts_sees,
impOfSubs analz_subset_parts,
- Says_imp_sees_Spy' RS analz.Inj]) 1));
+ Says_imp_sees_Spy RS analz.Inj]) 1));
bind_thm ("Spy_not_see_premaster_secret", result() RSN (2, rev_mp));
@@ -395,13 +402,13 @@
Converse doesn't hold; betraying M doesn't force the keys to be sent!*)
goal thy
- "!!evs. [| Nonce M ~: analz (sees lost Spy evs); evs : tls |] \
-\ ==> Key (clientK(NA,NB,M)) ~: parts (sees lost Spy evs)";
+ "!!evs. [| Nonce M ~: analz (sees Spy evs); evs : tls |] \
+\ ==> Key (clientK(NA,NB,M)) ~: parts (sees Spy 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_sees_Spy RS analz.Inj]) 3);
(*Fake*)
by (spy_analz_tac 2);
(*Base*)
@@ -412,13 +419,13 @@
AddSEs [clientK_notin_parts RSN (2, rev_notE)];
goal thy
- "!!evs. [| Nonce M ~: analz (sees lost Spy evs); evs : tls |] \
-\ ==> Key (serverK(NA,NB,M)) ~: parts (sees lost Spy evs)";
+ "!!evs. [| Nonce M ~: analz (sees Spy evs); evs : tls |] \
+\ ==> Key (serverK(NA,NB,M)) ~: parts (sees Spy 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_sees_Spy RS analz.Inj]) 3);
(*Fake*)
by (spy_analz_tac 2);
(*Base*)
@@ -434,7 +441,7 @@
goal thy
"!!evs. [| Nonce M ~: used evs; evs : tls |] \
-\ ==> Crypt (clientK(NA,NB,M)) Y ~: parts (sees lost Spy evs)";
+\ ==> Crypt (clientK(NA,NB,M)) Y ~: parts (sees Spy evs)";
by (etac rev_mp 1);
by (analz_induct_tac 1);
(*ClientFinished: since M is fresh, a different instance of clientK was used.*)
@@ -450,7 +457,7 @@
goal thy
"!!evs. [| Nonce M ~: used evs; evs : tls |] \
-\ ==> Crypt (serverK(NA,NB,M)) Y ~: parts (sees lost Spy evs)";
+\ ==> Crypt (serverK(NA,NB,M)) Y ~: parts (sees Spy evs)";
by (etac rev_mp 1);
by (analz_induct_tac 1);
(*ServerFinished: since M is fresh, a different instance of serverK was used.*)
@@ -465,10 +472,10 @@
AddEs [Crypt_serverK_notin_parts RSN (2, rev_notE)];
-(*Weakening A~:lost to A~=Spy would complicate later uses of the rule*)
+(*NEEDED??*)
goal thy
"!!evs. [| Says A B {|certA, Crypt KB (Nonce M)|} : set evs; \
-\ A ~: lost; evs : tls |] ==> KB = pubK B";
+\ A ~= Spy; evs : tls |] ==> KB = pubK B";
be rev_mp 1;
by (analz_induct_tac 1);
qed "A_Crypt_pubB";
@@ -476,36 +483,25 @@
(*** Unicity results for M, the pre-master-secret ***)
-(*Induction for theorems of the form X ~: analz (sees lost Spy evs) --> ...
- It simplifies the proof by discarding needless information about
- analz (insert X (sees lost Spy evs))
-*)
-fun analz_mono_parts_induct_tac i =
- etac tls.induct i THEN
- ClientCertKeyEx_tac (i+5) THEN (*ClientCertKeyEx*)
- REPEAT_FIRST analz_mono_contra_tac;
-
-
(*M determines B. Proof borrowed from NS_Public/unique_NA and from Yahalom*)
goal thy
- "!!evs. [| Nonce M ~: analz (sees lost Spy evs); evs : tls |] \
+ "!!evs. [| Nonce M ~: analz (sees Spy evs); evs : tls |] \
\ ==> EX B'. ALL B. \
-\ Crypt (pubK B) (Nonce M) : parts (sees lost Spy evs) --> B=B'";
+\ Crypt (pubK B) (Nonce M) : parts (sees Spy evs) --> B=B'";
by (etac rev_mp 1);
-by (analz_mono_parts_induct_tac 1);
-by (prove_simple_subgoals_tac 1);
-by (asm_simp_tac (!simpset addsimps [all_conj_distrib]
- setloop split_tac [expand_if]) 2);
+by (parts_induct_tac 1);
+by (Fake_parts_insert_tac 1);
(*ClientCertKeyEx*)
-by (expand_case_tac "M = ?y" 2 THEN
- REPEAT (blast_tac (!claset addSEs partsEs) 2));
-by (Fake_parts_insert_tac 1);
+by (ClientCertKeyEx_tac 1);
+by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
+by (expand_case_tac "M = ?y" 1 THEN
+ blast_tac (!claset addSEs partsEs) 1);
val lemma = result();
goal thy
- "!!evs. [| Crypt(pubK B) (Nonce M) : parts (sees lost Spy evs); \
-\ Crypt(pubK B') (Nonce M) : parts (sees lost Spy evs); \
-\ Nonce M ~: analz (sees lost Spy evs); \
+ "!!evs. [| Crypt(pubK B) (Nonce M) : parts (sees Spy evs); \
+\ Crypt(pubK B') (Nonce M) : parts (sees Spy evs); \
+\ Nonce M ~: analz (sees Spy evs); \
\ evs : tls |] \
\ ==> B=B'";
by (prove_unique_tac lemma 1);
@@ -514,12 +510,11 @@
(*In A's note to herself, M determines A and B.*)
goal thy
- "!!evs. [| Nonce M ~: analz (sees lost Spy evs); evs : tls |] \
+ "!!evs. [| Nonce M ~: analz (sees Spy evs); evs : tls |] \
\ ==> EX A' B'. ALL A B. \
\ Notes A {|Agent B, Nonce M|} : set evs --> A=A' & B=B'";
by (etac rev_mp 1);
-by (analz_mono_parts_induct_tac 1);
-by (prove_simple_subgoals_tac 1);
+by (parts_induct_tac 1);
by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
(*ClientCertKeyEx: if M is fresh, then it can't appear in Notes A X.*)
by (expand_case_tac "M = ?y" 1 THEN
@@ -529,7 +524,7 @@
goal thy
"!!evs. [| Notes A {|Agent B, Nonce M|} : set evs; \
\ Notes A' {|Agent B', Nonce M|} : set evs; \
-\ Nonce M ~: analz (sees lost Spy evs); \
+\ Nonce M ~: analz (sees Spy evs); \
\ evs : tls |] \
\ ==> A=A' & B=B'";
by (prove_unique_tac lemma 1);
@@ -550,13 +545,13 @@
\ Nonce NB, Agent XB, certificate B (pubK B)|}); \
\ evs : tls; A ~: lost; B ~: lost |] \
\ ==> Notes A {|Agent B, Nonce M|} : set evs --> \
-\ X : parts (sees lost Spy evs) --> Says B A X : set evs";
+\ X : parts (sees Spy evs) --> Says B A X : set evs";
by (hyp_subst_tac 1);
by (analz_induct_tac 1);
by (REPEAT_FIRST (rtac impI));
(*Fake: the Spy doesn't have the critical session key!*)
by (REPEAT (rtac impI 1));
-by (subgoal_tac "Key (serverK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1);
+by (subgoal_tac "Key (serverK(NA,NB,M)) ~: analz (sees Spy evsa)" 1);
by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret,
not_parts_not_analz]) 2);
by (Fake_parts_insert_tac 1);
@@ -566,16 +561,17 @@
(*This version refers not to SERVER FINISHED but to any message from B.
We don't assume B has received CERTIFICATE VERIFY, and an intruder could
have changed A's identity in all other messages, so we can't be sure
- that B sends his message to A.*)
+ that B sends his message to A. If CLIENT KEY EXCHANGE were augmented
+ to bind A's identify with M, then we could replace A' by A below.*)
goal thy
- "!!evs. [| evs : tls; A ~: lost; B ~: lost |] \
-\ ==> Notes A {|Agent B, Nonce M|} : set evs --> \
-\ Crypt (serverK(NA,NB,M)) Y : parts (sees lost Spy evs) --> \
+ "!!evs. [| evs : tls; A ~: lost; B ~: lost |] \
+\ ==> Notes A {|Agent B, Nonce M|} : set evs --> \
+\ Crypt (serverK(NA,NB,M)) Y : parts (sees Spy evs) --> \
\ (EX A'. Says B A' (Crypt (serverK(NA,NB,M)) Y) : set evs)";
by (analz_induct_tac 1);
by (REPEAT_FIRST (rtac impI));
(*Fake: the Spy doesn't have the critical session key!*)
-by (subgoal_tac "Key (serverK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1);
+by (subgoal_tac "Key (serverK(NA,NB,M)) ~: analz (sees Spy evsa)" 1);
by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret,
not_parts_not_analz]) 2);
by (Fake_parts_insert_tac 1);
@@ -584,11 +580,11 @@
(*...otherwise delete induction hyp and use unicity of M.*)
by (thin_tac "?PP-->?QQ" 1);
by (Step_tac 1);
-by (subgoal_tac "Nonce M ~: analz (sees lost Spy evsa)" 1);
+by (subgoal_tac "Nonce M ~: analz (sees Spy evsa)" 1);
by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret]) 2);
by (blast_tac (!claset addSEs [MPair_parts]
addDs [Notes_Crypt_parts_sees,
- Says_imp_sees_Spy' RS parts.Inj,
+ Says_imp_sees_Spy RS parts.Inj,
unique_M]) 1);
qed_spec_mp "TrustServerMsg";
@@ -601,18 +597,18 @@
goal thy
"!!evs. [| evs : tls; A ~: lost; B ~: lost |] \
\ ==> Notes A {|Agent B, Nonce M|} : set evs --> \
-\ Crypt (clientK(NA,NB,M)) Y : parts (sees lost Spy evs) --> \
+\ Crypt (clientK(NA,NB,M)) Y : parts (sees Spy evs) --> \
\ Says A B (Crypt (clientK(NA,NB,M)) Y) : set evs";
by (analz_induct_tac 1);
by (REPEAT_FIRST (rtac impI));
(*Fake: the Spy doesn't have the critical session key!*)
-by (subgoal_tac "Key (clientK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1);
+by (subgoal_tac "Key (clientK(NA,NB,M)) ~: analz (sees Spy evsa)" 1);
by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret,
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 M ~: analz (sees lost Spy evsa)" 1);
+by (subgoal_tac "Nonce M ~: analz (sees Spy evsa)" 1);
by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret]) 2);
by (blast_tac (!claset addSEs [MPair_parts]
addDs [Notes_unique_M]) 1);
--- a/src/HOL/Auth/TLS.thy Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/TLS.thy Mon Jul 14 12:47:21 1997 +0200
@@ -13,7 +13,7 @@
Server, who is in charge of all public keys.
The model assumes that no fraudulent certificates are present, but it does
-assume that some private keys are lost to the spy.
+assume that some private keys are to the spy.
Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher
Allen, Transport Layer Security Working Group, 21 May 1997,
@@ -56,14 +56,8 @@
(*Clashes with pubK and priK are impossible, but this axiom is needed.*)
clientK_range "range clientK <= Compl (range serverK)"
- (*Spy has access to his own key for spoof messages, but Server is secure*)
- Spy_in_lost "Spy: lost"
- Server_not_lost "Server ~: lost"
-
-consts lost :: agent set (*No need for it to be a variable*)
- tls :: event list set
-
+consts tls :: event list set
inductive tls
intrs
Nil (*Initial trace is empty*)
@@ -71,7 +65,7 @@
Fake (*The spy, an active attacker, MAY say anything he CAN say.*)
"[| evs: tls; B ~= Spy;
- X: synth (analz (sees lost Spy evs)) |]
+ X: synth (analz (sees Spy evs)) |]
==> Says Spy B X # evs : tls"
SpyKeys (*The spy may apply clientK & serverK to nonces he's found*)
--- a/src/HOL/Auth/WooLam.ML Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/WooLam.ML Mon Jul 14 12:47:21 1997 +0200
@@ -41,41 +41,38 @@
(** For reasoning about the encrypted portion of messages **)
-goal thy "!!evs. Says A' B X : set evs \
-\ ==> X : analz (sees lost Spy evs)";
+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";
bind_thm ("WL4_parts_sees_Spy",
WL4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
-val parts_induct_tac =
- etac woolam.induct 1 THEN
- forward_tac [WL4_parts_sees_Spy] 6 THEN
+(*For proving the easier theorems about X ~: parts (sees Spy evs) *)
+fun parts_induct_tac i =
+ etac woolam.induct i THEN
+ forward_tac [WL4_parts_sees_Spy] (i+5) THEN
prove_simple_subgoals_tac 1;
-(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
+(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
sends messages containing X! **)
(*Spy never sees another agent's shared key! (unless it's lost at start)*)
goal thy
- "!!evs. evs : woolam \
-\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by parts_induct_tac;
+ "!!evs. evs : woolam ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
+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 lost Spy evs)) = (A : lost)";
+ "!!evs. evs : woolam ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
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 lost Spy evs); \
+goal thy "!!A. [| Key (shrK A) : parts (sees Spy evs); \
\ evs : woolam |] ==> A:lost";
by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
qed "Spy_see_shrK_D";
@@ -91,10 +88,10 @@
(*If the encrypted message appears then it originated with Alice*)
goal thy
- "!!evs. [| A ~: lost; evs : woolam |] \
-\ ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs) \
-\ --> (EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs)";
-by parts_induct_tac;
+ "!!evs. [| A ~: lost; evs : woolam |] \
+\ ==> Crypt (shrK A) (Nonce NB) : parts (sees Spy evs) \
+\ --> (EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs)";
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (Blast_tac 1);
qed_spec_mp "NB_Crypt_imp_Alice_msg";
@@ -121,7 +118,7 @@
\ Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs \
\ --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \
\ : set evs)";
-by parts_induct_tac;
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (ALLGOALS Blast_tac);
bind_thm ("Server_sent_WL5", result() RSN (2, rev_mp));
@@ -129,10 +126,10 @@
(*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 lost Spy evs) \
+ "!!evs. [| B ~: lost; evs : woolam |] \
+\ ==> Crypt (shrK B) {|Agent A, NB|} : parts (sees Spy evs) \
\ --> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs";
-by parts_induct_tac;
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
qed_spec_mp "NB_Crypt_imp_Server_msg";
@@ -161,10 +158,10 @@
(*B only issues challenges in response to WL1. Useful??*)
goal thy
- "!!evs. [| B ~= Spy; evs : woolam |] \
+ "!!evs. [| B ~= Spy; evs : woolam |] \
\ ==> Says B A (Nonce NB) : set evs \
\ --> (EX A'. Says A' B (Agent A) : set evs)";
-by parts_induct_tac;
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (ALLGOALS Blast_tac);
bind_thm ("B_said_WL2", result() RSN (2, rev_mp));
@@ -172,11 +169,11 @@
(**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 lost Spy evs) & \
-\ Says B A (Nonce NB) : set evs \
+ "!!evs. [| A ~: lost; B ~= Spy; evs : woolam |] \
+\ ==> Crypt (shrK A) (Nonce NB) : parts (sees Spy evs) & \
+\ Says B A (Nonce NB) : set evs \
\ --> Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
-by parts_induct_tac;
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (Step_tac 1);
by (blast_tac (!claset addSEs partsEs) 1);
--- a/src/HOL/Auth/WooLam.thy Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/WooLam.thy Mon Jul 14 12:47:21 1997 +0200
@@ -16,8 +16,7 @@
WooLam = Shared +
-consts lost :: agent set (*No need for it to be a variable*)
- woolam :: event list set
+consts woolam :: event list set
inductive woolam
intrs
(*Initial trace is empty*)
@@ -27,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 lost Spy evs)) |]
+ X: synth (analz (sees Spy evs)) |]
==> Says Spy B X # evs : woolam"
(*Alice initiates a protocol run*)
--- a/src/HOL/Auth/Yahalom.ML Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/Yahalom.ML Mon Jul 14 12:47:21 1997 +0200
@@ -16,14 +16,11 @@
HOL_quantifiers := false;
Pretty.setdepth 25;
-(*Replacing the variable by a constant improves speed*)
-val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy;
-
(*A "possibility property": there are traces that reach the end*)
goal thy
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
-\ ==> EX X NB K. EX evs: yahalom lost. \
+\ ==> EX X NB K. EX evs: yahalom. \
\ Says A B {|X, Crypt K (Nonce NB)|} : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS
@@ -35,7 +32,7 @@
(**** Inductive proofs about yahalom ****)
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set evs";
+goal thy "!!evs. evs: yahalom ==> ALL A X. Says A A X ~: set evs";
by (etac yahalom.induct 1);
by (Auto_tac());
qed_spec_mp "not_Says_to_self";
@@ -47,8 +44,8 @@
(*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 lost Spy evs)";
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
+\ X : analz (sees Spy evs)";
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "YM4_analz_sees_Spy";
bind_thm ("YM4_parts_sees_Spy",
@@ -56,45 +53,47 @@
(*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 lost Spy evs)";
+\ K : parts (sees Spy evs)";
by (blast_tac (!claset addSEs partsEs
- addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
+ addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
qed "YM4_Key_parts_sees_Spy";
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
- We instantiate the variable to "lost" since leaving it as a Var would
- interfere with simplification.*)
-val parts_sees_tac =
- forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6 THEN
- forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7 THEN
- prove_simple_subgoals_tac 1;
+(*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
+ prove_simple_subgoals_tac i;
-val parts_induct_tac =
- etac yahalom.induct 1 THEN parts_sees_tac;
+(*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)) *)
+fun parts_induct_tac i =
+ etac yahalom.induct i
+ THEN
+ REPEAT (FIRSTGOAL analz_mono_contra_tac)
+ THEN parts_sees_tac i;
-(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
+(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
sends messages containing X! **)
(*Spy never sees another agent's shared key! (unless it's lost at start)*)
goal thy
- "!!evs. evs : yahalom lost \
-\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by parts_induct_tac;
+ "!!evs. evs : yahalom ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (Blast_tac 1);
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
goal thy
- "!!evs. evs : yahalom lost \
-\ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
+ "!!evs. evs : yahalom ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
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 lost Spy evs); \
-\ evs : yahalom lost |] ==> A:lost";
+goal thy "!!A. [| Key (shrK A) : parts (sees Spy evs); \
+\ evs : yahalom |] ==> A:lost";
by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
qed "Spy_see_shrK_D";
@@ -103,9 +102,9 @@
(*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*)
-goal thy "!!evs. evs : yahalom lost ==> \
-\ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
-by parts_induct_tac;
+goal thy "!!evs. evs : yahalom ==> \
+\ Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
+by (parts_induct_tac 1);
(*YM4: Key K is not fresh!*)
by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
(*YM3*)
@@ -130,7 +129,7 @@
goal thy
"!!evs. [| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \
\ : set evs; \
-\ evs : yahalom lost |] \
+\ evs : yahalom |] \
\ ==> K ~: range shrK";
by (etac rev_mp 1);
by (etac yahalom.induct 1);
@@ -139,18 +138,18 @@
qed "Says_Server_message_form";
-(*For proofs involving analz. We again instantiate the variable to "lost".*)
+(*For proofs involving analz.*)
val analz_sees_tac =
- forw_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
- forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
+ forward_tac [YM4_analz_sees_Spy] 6 THEN
+ forward_tac [Says_Server_message_form] 7 THEN
assume_tac 7 THEN REPEAT ((etac exE ORELSE' hyp_subst_tac) 7);
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
- Key K : analz (sees lost Spy evs)
+ Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
+ Key K : analz (sees Spy evs)
A more general formula must be proved inductively.
****)
@@ -158,10 +157,10 @@
(** Session keys are not used to encrypt other session keys **)
goal thy
- "!!evs. evs : yahalom lost ==> \
+ "!!evs. evs : yahalom ==> \
\ ALL K KK. KK <= Compl (range shrK) --> \
-\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
-\ (K : KK | Key K : analz (sees lost Spy evs))";
+\ (Key K : analz (Key``KK Un (sees Spy evs))) = \
+\ (K : KK | Key K : analz (sees Spy evs))";
by (etac yahalom.induct 1);
by analz_sees_tac;
by (REPEAT_FIRST (resolve_tac [allI, impI]));
@@ -174,9 +173,9 @@
qed_spec_mp "analz_image_freshK";
goal thy
- "!!evs. [| evs : yahalom lost; KAB ~: range shrK |] ==> \
-\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
-\ (K = KAB | Key K : analz (sees lost Spy evs))";
+ "!!evs. [| evs : yahalom; KAB ~: range shrK |] ==> \
+\ Key K : analz (insert (Key KAB) (sees Spy evs)) = \
+\ (K = KAB | Key K : analz (sees Spy evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
qed "analz_insert_freshK";
@@ -184,7 +183,7 @@
(*** The Key K uniquely identifies the Server's message. **)
goal thy
- "!!evs. evs : yahalom lost ==> \
+ "!!evs. evs : yahalom ==> \
\ EX A' B' na' nb' X'. ALL A B na nb X. \
\ Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \
@@ -209,7 +208,7 @@
\ Says Server A' \
\ {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} \
\ : set evs; \
-\ evs : yahalom lost |] \
+\ evs : yahalom |] \
\ ==> A=A' & B=B' & na=na' & nb=nb'";
by (prove_unique_tac lemma 1);
qed "unique_session_keys";
@@ -218,13 +217,13 @@
(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
goal thy
- "!!evs. [| A ~: lost; B ~: lost; evs : yahalom lost |] \
+ "!!evs. [| A ~: lost; B ~: lost; 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 lost Spy evs)";
+\ Key K ~: analz (sees Spy evs)";
by (etac yahalom.induct 1);
by analz_sees_tac;
by (ALLGOALS
@@ -250,37 +249,26 @@
\ Crypt (shrK B) {|Agent A, Key K|}|} \
\ : set evs; \
\ Says A Spy {|na, nb, Key K|} ~: set evs; \
-\ A ~: lost; B ~: lost; evs : yahalom lost |] \
-\ ==> Key K ~: analz (sees lost Spy evs)";
+\ A ~: lost; B ~: lost; evs : yahalom |] \
+\ ==> Key K ~: analz (sees Spy 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";
-(*Induction for theorems of the form X ~: analz (sees lost Spy evs) --> ...
- It simplifies the proof by discarding needless information about
- analz (insert X (sees lost Spy evs))
-*)
-fun analz_mono_parts_induct_tac i =
- etac yahalom.induct i
- THEN
- REPEAT_FIRST analz_mono_contra_tac
- THEN parts_sees_tac;
-
-
(** Security Guarantee for A upon receiving YM3 **)
(*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 lost Spy evs); \
-\ A ~: lost; evs : yahalom lost |] \
+\ : parts (sees Spy evs); \
+\ A ~: lost; evs : yahalom |] \
\ ==> Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \
\ Crypt (shrK B) {|Agent A, Key K|}|} \
\ : set evs";
by (etac rev_mp 1);
-by parts_induct_tac;
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
qed "A_trusts_YM3";
@@ -290,15 +278,15 @@
(*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 lost Spy evs); \
-\ B ~: lost; evs : yahalom lost |] \
+ "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (sees Spy evs); \
+\ B ~: lost; evs : yahalom |] \
\ ==> EX NA NB. Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, \
\ Nonce NA, Nonce NB|}, \
\ Crypt (shrK B) {|Agent A, Key K|}|} \
\ : set evs";
by (etac rev_mp 1);
-by parts_induct_tac;
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
(*YM3*)
by (Blast_tac 1);
@@ -308,15 +296,15 @@
the key quoting nonce NB. This part says nothing about agent names.
Secrecy of NB is crucial.*)
goal thy
- "!!evs. evs : yahalom lost \
-\ ==> Nonce NB ~: analz (sees lost Spy evs) --> \
-\ Crypt K (Nonce NB) : parts (sees lost Spy evs) --> \
+ "!!evs. evs : yahalom \
+\ ==> Nonce NB ~: analz (sees Spy evs) --> \
+\ Crypt K (Nonce NB) : parts (sees Spy evs) --> \
\ (EX A B NA. Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, \
\ Nonce NA, Nonce NB|}, \
\ Crypt (shrK B) {|Agent A, Key K|}|} \
\ : set evs)";
-by (analz_mono_parts_induct_tac 1);
+by (parts_induct_tac 1);
(*YM3 & Fake*)
by (Blast_tac 2);
by (Fake_parts_insert_tac 1);
@@ -325,7 +313,7 @@
(*A is uncompromised because NB is secure*)
by (not_lost_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_sees_Spy RS parts.Inj RS parts.Fst RS
A_trusts_YM3]) 1);
bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp));
@@ -364,7 +352,7 @@
"!!evs. [| Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|} \
\ : set evs; \
-\ NB ~= NB'; evs : yahalom lost |] \
+\ NB ~= NB'; evs : yahalom |] \
\ ==> ~ KeyWithNonce K NB evs";
by (blast_tac (!claset addDs [unique_session_keys]) 1);
qed "Says_Server_KeyWithNonce";
@@ -384,11 +372,11 @@
val lemma = result();
goal thy
- "!!evs. evs : yahalom lost ==> \
+ "!!evs. evs : yahalom ==> \
\ (ALL KK. KK <= Compl (range shrK) --> \
\ (ALL K: KK. ~ KeyWithNonce K NB evs) --> \
-\ (Nonce NB : analz (Key``KK Un (sees lost Spy evs))) = \
-\ (Nonce NB : analz (sees lost Spy evs)))";
+\ (Nonce NB : analz (Key``KK Un (sees Spy evs))) = \
+\ (Nonce NB : analz (sees Spy evs)))";
by (etac yahalom.induct 1);
by analz_sees_tac;
by (REPEAT_FIRST (resolve_tac [impI RS allI]));
@@ -410,7 +398,7 @@
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 (dtac (Says_imp_sees_Spy 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";
@@ -423,9 +411,9 @@
"!!evs. [| Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|} \
\ : set evs; \
-\ NB ~= NB'; KAB ~: range shrK; evs : yahalom lost |] \
-\ ==> (Nonce NB : analz (insert (Key KAB) (sees lost Spy evs))) = \
-\ (Nonce NB : analz (sees lost Spy evs))";
+\ NB ~= NB'; KAB ~: range shrK; evs : yahalom |] \
+\ ==> (Nonce NB : analz (insert (Key KAB) (sees Spy evs))) = \
+\ (Nonce NB : analz (sees Spy evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps
[Nonce_secrecy, Says_Server_KeyWithNonce]) 1);
qed "single_Nonce_secrecy";
@@ -434,11 +422,11 @@
(*** The Nonce NB uniquely identifies B's message. ***)
goal thy
- "!!evs. evs : yahalom lost ==> \
+ "!!evs. evs : yahalom ==> \
\ EX NA' A' B'. ALL NA A B. \
-\ Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts(sees lost Spy evs) \
+\ Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts(sees Spy evs) \
\ --> B ~: lost --> NA = NA' & A = A' & B = B'";
-by parts_induct_tac;
+by (parts_induct_tac 1);
(*Fake*)
by (REPEAT (etac (exI RSN (2,exE)) 1) (*stripping EXs makes proof faster*)
THEN Fake_parts_insert_tac 1);
@@ -451,10 +439,10 @@
goal thy
"!!evs.[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} \
-\ : parts (sees lost Spy evs); \
+\ : parts (sees Spy evs); \
\ Crypt (shrK B') {|Agent A', Nonce NA', nb|} \
-\ : parts (sees lost Spy evs); \
-\ evs : yahalom lost; B ~: lost; B' ~: lost |] \
+\ : parts (sees Spy evs); \
+\ evs : yahalom; B ~: lost; B' ~: lost |] \
\ ==> NA' = NA & A' = A & B' = B";
by (prove_unique_tac lemma 1);
qed "unique_NB";
@@ -467,29 +455,27 @@
\ : set evs; B ~: lost; \
\ Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|} \
\ : set evs; \
-\ nb ~: analz (sees lost Spy evs); evs : yahalom lost |] \
+\ nb ~: analz (sees Spy 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 (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
addSEs [MPair_parts]
addDs [unique_NB]) 1);
qed "Says_unique_NB";
-val Says_unique_NB' = read_instantiate [("lost","lost")] Says_unique_NB;
-
(** A nonce value is never used both as NA and as NB **)
goal thy
- "!!evs. [| B ~: lost; evs : yahalom lost |] \
-\ ==> Nonce NB ~: analz (sees lost Spy evs) --> \
+ "!!evs. [| B ~: lost; evs : yahalom |] \
+\ ==> Nonce NB ~: analz (sees Spy evs) --> \
\ Crypt (shrK B') {|Agent A', Nonce NB, nb'|} \
-\ : parts(sees lost Spy evs) \
+\ : parts(sees Spy evs) \
\ --> Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} \
-\ ~: parts(sees lost Spy evs)";
-by (analz_mono_parts_induct_tac 1);
+\ ~: parts(sees Spy 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_sees_Spy 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));
@@ -498,7 +484,7 @@
goal thy
"!!evs. [| Says Server A \
\ {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set evs; \
-\ evs : yahalom lost |] \
+\ evs : yahalom |] \
\ ==> EX B'. Says B' Server \
\ {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} \
\ : set evs";
@@ -509,15 +495,14 @@
qed "Says_Server_imp_YM2";
-(*A vital theorem for B, that nonce NB remains secure from the Spy.
- Unusually, the Fake case requires Spy:lost.*)
+(*A vital theorem for B, that nonce NB remains secure from the Spy.*)
goal thy
- "!!evs. [| A ~: lost; B ~: lost; Spy: lost; evs : yahalom lost |] \
+ "!!evs. [| A ~: lost; B ~: lost; 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 lost Spy evs)";
+\ Nonce NB ~: analz (sees Spy evs)";
by (etac yahalom.induct 1);
by analz_sees_tac;
by (ALLGOALS
@@ -526,13 +511,13 @@
analz_insert_freshK] @ pushes)
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_sees_Spy RS parts.Inj]
addSEs [MPair_parts]
- addDs [no_nonce_YM1_YM2, Says_unique_NB']) 4
+ 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_sees_Spy 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]
@@ -543,12 +528,12 @@
(*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 (dtac (Says_imp_sees_Spy 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]));
-(* use Says_unique_NB' to identify message components: Aa=A, Ba=B, NAa=NA *)
-by (blast_tac (!claset addDs [Says_unique_NB', Spy_not_see_encrypted_key,
+(* use Says_unique_NB to identify message components: Aa=A, Ba=B, NAa=NA *)
+by (blast_tac (!claset addDs [Says_unique_NB, Spy_not_see_encrypted_key,
impOfSubs Fake_analz_insert]) 1);
(** LEVEL 14 **)
(*Oops case: if the nonce is betrayed now, show that the Oops event is
@@ -558,11 +543,11 @@
by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
by (expand_case_tac "NB = NBa" 1);
(*If NB=NBa then all other components of the Oops message agree*)
-by (blast_tac (!claset addDs [Says_unique_NB']) 1 THEN flexflex_tac);
+by (blast_tac (!claset addDs [Says_unique_NB]) 1 THEN flexflex_tac);
(*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_sees_Spy 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));
@@ -579,20 +564,20 @@
\ 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; Spy: lost; evs : yahalom lost |] \
+\ A ~: lost; B ~: lost; 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_sees_Spy 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]));
by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1);
by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1));
-by (blast_tac (!claset addDs [Says_unique_NB']) 1);
+by (blast_tac (!claset addDs [Says_unique_NB]) 1);
qed "B_trusts_YM4";
@@ -601,19 +586,19 @@
(*The encryption in message YM2 tells us it cannot be faked.*)
goal thy
- "!!evs. evs : yahalom lost \
-\ ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|} \
-\ : parts (sees lost Spy evs) --> \
-\ B ~: lost --> \
+ "!!evs. evs : yahalom \
+\ ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|} \
+\ : parts (sees Spy evs) --> \
+\ B ~: lost --> \
\ Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
\ : set evs";
-by parts_induct_tac;
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
bind_thm ("B_Said_YM2", result() RSN (2, rev_mp) RS mp);
(*If the server sends YM3 then B sent YM2*)
goal thy
- "!!evs. evs : yahalom lost \
+ "!!evs. evs : yahalom \
\ ==> Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
\ : set evs --> \
\ B ~: lost --> \
@@ -624,7 +609,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_sees_Spy RS parts.Inj]
addSEs [MPair_parts]) 1);
val lemma = result() RSN (2, rev_mp) RS mp |> standard;
@@ -632,7 +617,7 @@
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 lost |] \
+\ A ~: lost; B ~: lost; 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]
@@ -646,14 +631,14 @@
A has said NB. We can't be sure about the rest of A's message, but only
NB matters for freshness.*)
goal thy
- "!!evs. evs : yahalom lost \
-\ ==> Key K ~: analz (sees lost Spy evs) --> \
-\ Crypt K (Nonce NB) : parts (sees lost Spy evs) --> \
-\ Crypt (shrK B) {|Agent A, Key K|} \
-\ : parts (sees lost Spy evs) --> \
-\ B ~: lost --> \
+ "!!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)";
-by (analz_mono_parts_induct_tac 1);
+by (parts_induct_tac 1);
(*Fake*)
by (Fake_parts_insert_tac 1);
(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
@@ -664,7 +649,7 @@
by (not_lost_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_sees_Spy RS parts.Inj,
unique_session_keys]) 1);
val lemma = normalize_thm [RSspec, RSmp] (result()) |> standard;
@@ -678,14 +663,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; Spy: lost; evs : yahalom lost |] \
+\ A ~: lost; B ~: lost; 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_sees_Spy 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_sees_Spy RS parts.Inj]) 1);
qed_spec_mp "YM4_imp_A_Said_YM3";
--- a/src/HOL/Auth/Yahalom.thy Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/Yahalom.thy Mon Jul 14 12:47:21 1997 +0200
@@ -12,58 +12,58 @@
Yahalom = Shared +
-consts yahalom :: agent set => event list set
-inductive "yahalom lost"
+consts yahalom :: event list set
+inductive "yahalom"
intrs
(*Initial trace is empty*)
- Nil "[]: yahalom lost"
+ Nil "[]: yahalom"
(*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: yahalom lost; B ~= Spy;
- X: synth (analz (sees lost Spy evs)) |]
- ==> Says Spy B X # evs : yahalom lost"
+ Fake "[| evs: yahalom; B ~= Spy;
+ X: synth (analz (sees Spy evs)) |]
+ ==> Says Spy B X # evs : yahalom"
(*Alice initiates a protocol run*)
- YM1 "[| evs: yahalom lost; A ~= B; Nonce NA ~: used evs |]
- ==> Says A B {|Agent A, Nonce NA|} # evs : yahalom lost"
+ YM1 "[| evs: yahalom; A ~= B; Nonce NA ~: used evs |]
+ ==> Says A B {|Agent A, Nonce NA|} # evs : yahalom"
(*Bob's response to Alice's message. Bob doesn't know who
the sender is, hence the A' in the sender field.*)
- YM2 "[| evs: yahalom lost; B ~= Server; Nonce NB ~: used evs;
+ YM2 "[| evs: yahalom; B ~= Server; Nonce NB ~: used evs;
Says A' B {|Agent A, Nonce NA|} : set evs |]
==> Says B Server
{|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
- # evs : yahalom lost"
+ # evs : yahalom"
(*The Server receives Bob's message. He responds by sending a
new session key to Alice, with a packet for forwarding to Bob.*)
- YM3 "[| evs: yahalom lost; A ~= Server; Key KAB ~: used evs;
+ YM3 "[| evs: yahalom; A ~= Server; Key KAB ~: used evs;
Says B' Server
{|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
: set evs |]
==> Says Server A
{|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|},
Crypt (shrK B) {|Agent A, Key KAB|}|}
- # evs : yahalom lost"
+ # evs : yahalom"
(*Alice receives the Server's (?) message, checks her Nonce, and
uses the new session key to send Bob his Nonce.*)
- YM4 "[| evs: yahalom lost; A ~= Server;
+ YM4 "[| evs: yahalom; A ~= Server;
Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
X|} : set evs;
Says A B {|Agent A, Nonce NA|} : set evs |]
- ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom lost"
+ ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom"
(*This message models possible leaks of session keys. The Nonces
identify the protocol run. Quoting Server here ensures they are
correct.*)
- Oops "[| evs: yahalom lost; A ~= Spy;
+ Oops "[| evs: yahalom; A ~= Spy;
Says Server A {|Crypt (shrK A)
{|Agent B, Key K, Nonce NA, Nonce NB|},
X|} : set evs |]
- ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost"
+ ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom"
constdefs
--- a/src/HOL/Auth/Yahalom2.ML Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/Yahalom2.ML Mon Jul 14 12:47:21 1997 +0200
@@ -18,13 +18,13 @@
HOL_quantifiers := false;
(*Replacing the variable by a constant improves speed*)
-val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy;
+val Says_imp_sees_Spy' = Says_imp_sees_Spy;
(*A "possibility property": there are traces that reach the end*)
goal thy
- "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
-\ ==> EX X NB K. EX evs: yahalom lost. \
+ "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
+\ ==> EX X NB K. EX evs: yahalom. \
\ Says A B {|X, Crypt K (Nonce NB)|} : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS
@@ -36,7 +36,7 @@
(**** Inductive proofs about yahalom ****)
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set evs";
+goal thy "!!evs. evs: yahalom ==> ALL A X. Says A A X ~: set evs";
by (etac yahalom.induct 1);
by (Auto_tac());
qed_spec_mp "not_Says_to_self";
@@ -48,7 +48,7 @@
(*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 lost Spy evs)";
+\ X : analz (sees Spy evs)";
by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
qed "YM4_analz_sees_Spy";
@@ -57,45 +57,47 @@
(*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 lost Spy evs)";
+\ K : parts (sees Spy evs)";
by (blast_tac (!claset addSEs partsEs
addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
qed "YM4_Key_parts_sees_Spy";
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
- We instantiate the variable to "lost" since leaving it as a Var would
- interfere with simplification.*)
-val parts_sees_tac =
- forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6 THEN
- forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7 THEN
- prove_simple_subgoals_tac 1;
+(*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
+ prove_simple_subgoals_tac i;
-val parts_induct_tac =
- etac yahalom.induct 1 THEN parts_sees_tac;
+(*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)) *)
+fun parts_induct_tac i =
+ etac yahalom.induct i
+ THEN
+ REPEAT (FIRSTGOAL analz_mono_contra_tac)
+ THEN parts_sees_tac i;
-(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
+(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
sends messages containing X! **)
(*Spy never sees another agent's shared key! (unless it's lost at start)*)
goal thy
- "!!evs. evs : yahalom lost \
-\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by parts_induct_tac;
+ "!!evs. evs : yahalom ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (Blast_tac 1);
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
goal thy
- "!!evs. evs : yahalom lost \
-\ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
+ "!!evs. evs : yahalom ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
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 lost Spy evs); \
-\ evs : yahalom lost |] ==> A:lost";
+goal thy "!!A. [| Key (shrK A) : parts (sees Spy evs); \
+\ evs : yahalom |] ==> A:lost";
by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
qed "Spy_see_shrK_D";
@@ -104,9 +106,9 @@
(*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*)
-goal thy "!!evs. evs : yahalom lost ==> \
-\ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
-by parts_induct_tac;
+goal thy "!!evs. evs : yahalom ==> \
+\ Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
+by (parts_induct_tac 1);
(*YM4: Key K is not fresh!*)
by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
(*YM3*)
@@ -129,8 +131,8 @@
Oops as well as main secrecy property.*)
goal thy
"!!evs. [| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|} \
-\ : set evs; \
-\ evs : yahalom lost |] \
+\ : set evs; \
+\ evs : yahalom |] \
\ ==> K ~: range shrK & A ~= B";
by (etac rev_mp 1);
by (etac yahalom.induct 1);
@@ -138,10 +140,10 @@
qed "Says_Server_message_form";
-(*For proofs involving analz. We again instantiate the variable to "lost".*)
+(*For proofs involving analz.*)
val analz_sees_tac =
- dres_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
- forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
+ dtac YM4_analz_sees_Spy 6 THEN
+ forward_tac [Says_Server_message_form] 7 THEN
assume_tac 7 THEN
REPEAT ((etac conjE ORELSE' hyp_subst_tac) 7);
@@ -149,8 +151,8 @@
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
- Key K : analz (sees lost Spy evs)
+ Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
+ Key K : analz (sees Spy evs)
A more general formula must be proved inductively.
@@ -159,10 +161,10 @@
(** Session keys are not used to encrypt other session keys **)
goal thy
- "!!evs. evs : yahalom lost ==> \
-\ ALL K KK. KK <= Compl (range shrK) --> \
-\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
-\ (K : KK | Key K : analz (sees lost Spy evs))";
+ "!!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))";
by (etac yahalom.induct 1);
by analz_sees_tac;
by (REPEAT_FIRST (resolve_tac [allI, impI]));
@@ -175,9 +177,9 @@
qed_spec_mp "analz_image_freshK";
goal thy
- "!!evs. [| evs : yahalom lost; KAB ~: range shrK |] ==> \
-\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
-\ (K = KAB | Key K : analz (sees lost Spy evs))";
+ "!!evs. [| evs : yahalom; KAB ~: range shrK |] ==> \
+\ Key K : analz (insert (Key KAB) (sees Spy evs)) = \
+\ (K = KAB | Key K : analz (sees Spy evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
qed "analz_insert_freshK";
@@ -185,10 +187,10 @@
(*** The Key K uniquely identifies the Server's message. **)
goal thy
- "!!evs. evs : yahalom lost ==> \
-\ EX A' B' na' nb' X'. ALL A B na nb X. \
-\ Says Server A \
-\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} \
+ "!!evs. evs : yahalom ==> \
+\ EX A' B' na' nb' X'. ALL A B na nb X. \
+\ Says Server A \
+\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} \
\ : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
by (etac yahalom.induct 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
@@ -198,8 +200,8 @@
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
- delrules [conjI] (*prevent split-up into 4 subgoals*)
- addss (!simpset addsimps [parts_insertI])) 1);
+ delrules [conjI] (*prevent split-up into 4 subgoals*)
+ addss (!simpset addsimps [parts_insertI])) 1);
val lemma = result();
goal thy
@@ -209,7 +211,7 @@
\ Says Server A' \
\ {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|} \
\ : set evs; \
-\ evs : yahalom lost |] \
+\ evs : yahalom |] \
\ ==> A=A' & B=B' & na=na' & nb=nb'";
by (prove_unique_tac lemma 1);
qed "unique_session_keys";
@@ -218,14 +220,14 @@
(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
goal thy
- "!!evs. [| A ~: lost; B ~: lost; A ~= B; \
-\ evs : yahalom lost |] \
-\ ==> 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 lost Spy evs)";
+ "!!evs. [| A ~: lost; B ~: lost; 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)";
by (etac yahalom.induct 1);
by analz_sees_tac;
by (ALLGOALS
@@ -246,13 +248,13 @@
(*Final version*)
goal thy
- "!!evs. [| 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; \
-\ A ~: lost; B ~: lost; evs : yahalom lost |] \
-\ ==> Key K ~: analz (sees lost Spy evs)";
+ "!!evs. [| 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; \
+\ A ~: lost; B ~: lost; evs : yahalom |] \
+\ ==> Key K ~: analz (sees Spy 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";
@@ -264,14 +266,14 @@
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 lost Spy evs); \
-\ A ~: lost; evs : yahalom lost |] \
+\ : parts (sees Spy evs); \
+\ A ~: lost; evs : yahalom |] \
\ ==> EX nb. Says Server A \
\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \
\ Crypt (shrK B) {|nb, Key K, Agent A|}|} \
\ : set evs";
by (etac rev_mp 1);
-by parts_induct_tac;
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (Blast_tac 1);
qed "A_trusts_YM3";
@@ -283,15 +285,15 @@
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 lost Spy evs); \
-\ B ~: lost; evs : yahalom lost |] \
+\ : parts (sees Spy evs); \
+\ B ~: lost; 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 rev_mp 1);
-by parts_induct_tac;
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
(*YM3*)
by (Blast_tac 1);
@@ -306,7 +308,7 @@
goal thy
"!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|}, X|} \
\ : set evs; \
-\ A ~: lost; B ~: lost; evs : yahalom lost |] \
+\ A ~: lost; B ~: lost; evs : yahalom |] \
\ ==> EX NA. Says Server A \
\ {|Nonce NB, \
\ Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, \
@@ -322,13 +324,13 @@
(*The encryption in message YM2 tells us it cannot be faked.*)
goal thy
- "!!evs. evs : yahalom lost \
-\ ==> Crypt (shrK B) {|Agent A, Nonce NA|} : parts (sees lost Spy evs) --> \
-\ B ~: lost --> \
-\ (EX NB. Says B Server {|Agent B, Nonce NB, \
-\ Crypt (shrK B) {|Agent A, Nonce NA|}|} \
+ "!!evs. evs : yahalom \
+\ ==> Crypt (shrK B) {|Agent A, Nonce NA|} : parts (sees Spy evs) --> \
+\ B ~: lost --> \
+\ (EX NB. Says B Server {|Agent B, Nonce NB, \
+\ Crypt (shrK B) {|Agent A, Nonce NA|}|} \
\ : set evs)";
-by parts_induct_tac;
+by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
(*YM2*)
by (Blast_tac 1);
@@ -336,7 +338,7 @@
(*If the server sends YM3 then B sent YM2, perhaps with a different NB*)
goal thy
- "!!evs. evs : yahalom lost \
+ "!!evs. evs : yahalom \
\ ==> Says Server A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
\ : set evs --> \
\ B ~: lost --> \
@@ -357,7 +359,7 @@
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 lost |] \
+\ A ~: lost; B ~: lost; evs : yahalom |] \
\ ==> EX nb'. Says B Server \
\ {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|} \
\ : set evs";
@@ -368,29 +370,18 @@
(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
-(*Induction for theorems of the form X ~: analz (sees lost Spy evs) --> ...
- It simplifies the proof by discarding needless information about
- analz (insert X (sees lost Spy evs))
-*)
-fun analz_mono_parts_induct_tac i =
- etac yahalom.induct i
- THEN
- REPEAT_FIRST analz_mono_contra_tac
- THEN parts_sees_tac;
-
-
(*Assuming the session key is secure, if both certificates are present then
A has said NB. We can't be sure about the rest of A's message, but only
NB matters for freshness.*)
goal thy
- "!!evs. evs : yahalom lost \
-\ ==> Key K ~: analz (sees lost Spy evs) --> \
-\ Crypt K (Nonce NB) : parts (sees lost Spy evs) --> \
-\ Crypt (shrK B) {|Nonce NB, Key K, Agent A|} \
-\ : parts (sees lost Spy evs) --> \
-\ B ~: lost --> \
+ "!!evs. evs : yahalom \
+\ ==> Key K ~: analz (sees Spy evs) --> \
+\ Crypt K (Nonce NB) : parts (sees Spy 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)";
-by (analz_mono_parts_induct_tac 1);
+by (parts_induct_tac 1);
(*Fake*)
by (Fake_parts_insert_tac 1);
(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
@@ -412,7 +403,7 @@
"!!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 lost |] \
+\ A ~: lost; B ~: lost; 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 (dtac B_trusts_YM4_shrK 1);
--- a/src/HOL/Auth/Yahalom2.thy Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/Yahalom2.thy Mon Jul 14 12:47:21 1997 +0200
@@ -15,35 +15,35 @@
Yahalom2 = Shared +
-consts yahalom :: agent set => event list set
-inductive "yahalom lost"
+consts yahalom :: event list set
+inductive "yahalom"
intrs
(*Initial trace is empty*)
- Nil "[]: yahalom lost"
+ Nil "[]: yahalom"
(*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: yahalom lost; B ~= Spy;
- X: synth (analz (sees lost Spy evs)) |]
- ==> Says Spy B X # evs : yahalom lost"
+ Fake "[| evs: yahalom; B ~= Spy;
+ X: synth (analz (sees Spy evs)) |]
+ ==> Says Spy B X # evs : yahalom"
(*Alice initiates a protocol run*)
- YM1 "[| evs: yahalom lost; A ~= B; Nonce NA ~: used evs |]
- ==> Says A B {|Agent A, Nonce NA|} # evs : yahalom lost"
+ YM1 "[| evs: yahalom; A ~= B; Nonce NA ~: used evs |]
+ ==> Says A B {|Agent A, Nonce NA|} # evs : yahalom"
(*Bob's response to Alice's message. Bob doesn't know who
the sender is, hence the A' in the sender field.*)
- YM2 "[| evs: yahalom lost; B ~= Server; Nonce NB ~: used evs;
+ YM2 "[| evs: yahalom; B ~= Server; Nonce NB ~: used evs;
Says A' B {|Agent A, Nonce NA|} : set evs |]
==> Says B Server
{|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
- # evs : yahalom lost"
+ # evs : yahalom"
(*The Server receives Bob's message. He responds by sending a
new session key to Alice, with a packet for forwarding to Bob.
!! Fields are reversed in the 2nd packet to prevent attacks!! *)
- YM3 "[| evs: yahalom lost; A ~= B; A ~= Server; Key KAB ~: used evs;
+ YM3 "[| evs: yahalom; A ~= B; A ~= Server; Key KAB ~: used evs;
Says B' Server {|Agent B, Nonce NB,
Crypt (shrK B) {|Agent A, Nonce NA|}|}
: set evs |]
@@ -51,23 +51,23 @@
{|Nonce NB,
Crypt (shrK A) {|Agent B, Key KAB, Nonce NA|},
Crypt (shrK B) {|Nonce NB, Key KAB, Agent A|}|}
- # evs : yahalom lost"
+ # evs : yahalom"
(*Alice receives the Server's (?) message, checks her Nonce, and
uses the new session key to send Bob his Nonce.*)
- YM4 "[| evs: yahalom lost; A ~= Server;
+ YM4 "[| evs: yahalom; A ~= Server;
Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
X|} : set evs;
Says A B {|Agent A, Nonce NA|} : set evs |]
- ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom lost"
+ ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom"
(*This message models possible leaks of session keys. The nonces
identify the protocol run. Quoting Server here ensures they are
correct. *)
- Oops "[| evs: yahalom lost; A ~= Spy;
+ Oops "[| evs: yahalom; A ~= Spy;
Says Server A {|Nonce NB,
Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
X|} : set evs |]
- ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost"
+ ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom"
end