--- a/src/HOL/Auth/Message.ML Wed May 07 12:50:26 1997 +0200
+++ b/src/HOL/Auth/Message.ML Wed May 07 13:01:43 1997 +0200
@@ -35,7 +35,7 @@
goalw thy [keysFor_def] "keysFor (UN i. H i) = (UN i. keysFor (H i))";
by (Blast_tac 1);
-qed "keysFor_UN";
+qed "keysFor_UN1";
(*Monotonicity*)
goalw thy [keysFor_def] "!!G H. G<=H ==> keysFor(G) <= keysFor(H)";
@@ -67,9 +67,11 @@
by (Auto_tac());
qed "keysFor_insert_Crypt";
-Addsimps [keysFor_empty, keysFor_Un, keysFor_UN,
+Addsimps [keysFor_empty, keysFor_Un, keysFor_UN1,
keysFor_insert_Agent, keysFor_insert_Nonce, keysFor_insert_Key,
keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt];
+AddSEs [keysFor_Un RS equalityD1 RS subsetD RS UnE,
+ keysFor_UN1 RS equalityD1 RS subsetD RS UN1_E];
goalw thy [keysFor_def] "!!H. Crypt K X : H ==> invKey K : keysFor H";
by (Blast_tac 1);
@@ -173,8 +175,12 @@
by (simp_tac (!simpset addsimps [UNION1_def, parts_UN]) 1);
qed "parts_UN1";
-(*Added to simplify arguments to parts, analz and synth*)
+(*Added to simplify arguments to parts, analz and synth.
+ NOTE: the UN versions are no longer used!*)
Addsimps [parts_Un, parts_UN, parts_UN1];
+AddSEs [parts_Un RS equalityD1 RS subsetD RS UnE,
+ parts_UN RS equalityD1 RS subsetD RS UN_E,
+ parts_UN1 RS equalityD1 RS subsetD RS UN1_E];
goal thy "insert X (parts H) <= parts(insert X H)";
by (blast_tac (!claset addIs [impOfSubs parts_mono]) 1);
@@ -809,6 +815,21 @@
(*Cannot be added with Addsimps -- we don't always want to re-order messages*)
val pushes = pushKeys@pushCrypts;
+
+(*** Tactics useful for many protocol proofs ***)
+
+(*Prove base case (subgoal i) and simplify others*)
+fun prove_simple_subgoals_tac i =
+ fast_tac (!claset addss (!simpset)) i THEN
+ ALLGOALS Asm_simp_tac;
+
+fun Fake_parts_insert_tac i =
+ blast_tac (!claset addDs [impOfSubs analz_subset_parts,
+ impOfSubs Fake_parts_insert]) i;
+
+(*Apply rules to break down assumptions of the form
+ Y : parts(insert X H) and Y : analz(insert X H)
+*)
val Fake_insert_tac =
dresolve_tac [impOfSubs Fake_analz_insert,
impOfSubs Fake_parts_insert] THEN'
--- a/src/HOL/Auth/NS_Public.ML Wed May 07 12:50:26 1997 +0200
+++ b/src/HOL/Auth/NS_Public.ML Wed May 07 13:01:43 1997 +0200
@@ -12,15 +12,12 @@
proof_timing:=true;
HOL_quantifiers := false;
-val op addss = op unsafe_addss;
-
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. \
@@ -42,17 +39,6 @@
AddSEs [not_Says_to_self RSN (2, rev_notE)];
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
-fun parts_induct_tac i = SELECT_GOAL
- (DETERM (etac ns_public.induct 1 THEN
- (*Fake message*)
- TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]
- addss (!simpset)) 2)) THEN
- (*Base case*)
- fast_tac (!claset addss (!simpset)) 1 THEN
- ALLGOALS Asm_simp_tac) i;
-
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
sends messages containing X! **)
@@ -60,8 +46,9 @@
goal thy
"!!evs. evs : ns_public \
\ ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)";
-by (parts_induct_tac 1);
-by (Auto_tac());
+by (etac ns_public.induct 1);
+by (prove_simple_subgoals_tac 1);
+by (Fake_parts_insert_tac 1);
qed "Spy_see_priK";
Addsimps [Spy_see_priK];
@@ -74,7 +61,7 @@
goal thy "!!A. [| Key (priK A) : parts (sees lost Spy evs); \
\ evs : ns_public |] ==> A:lost";
-by (fast_tac (!claset addDs [Spy_see_priK]) 1);
+by (blast_tac (!claset addDs [Spy_see_priK]) 1);
qed "Spy_see_priK_D";
bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D);
@@ -82,7 +69,7 @@
fun analz_induct_tac i =
- etac ns_public.induct i THEN
+ etac ns_public.induct i THEN
ALLGOALS (asm_simp_tac
(!simpset addsimps [not_parts_not_analz]
setloop split_tac [expand_if]));
@@ -100,16 +87,15 @@
by (etac rev_mp 1);
by (analz_induct_tac 1);
(*NS3*)
-by (fast_tac (!claset addSEs partsEs) 4);
+by (blast_tac (!claset addSEs partsEs) 4);
(*NS2*)
-by (fast_tac (!claset addSEs partsEs) 3);
+by (blast_tac (!claset addSEs partsEs) 3);
(*Fake*)
-by (deepen_tac (!claset addSIs [analz_insertI]
+by (blast_tac (!claset addSIs [analz_insertI]
addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]
- addss (!simpset)) 0 2);
+ impOfSubs Fake_parts_insert]) 2);
(*Base*)
-by (fast_tac (!claset addss (!simpset)) 1);
+by (Blast_tac 1);
qed "no_nonce_NS1_NS2";
@@ -124,17 +110,16 @@
(*NS1*)
by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
by (expand_case_tac "NA = ?y" 3 THEN
- REPEAT (fast_tac (!claset addSEs partsEs) 3));
+ REPEAT (blast_tac (!claset addSEs partsEs) 3));
(*Base*)
-by (fast_tac (!claset addss (!simpset)) 1);
+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 (best_tac (!claset delrules [conjI]
+by (blast_tac (!claset delrules [conjI]
addSDs [impOfSubs Fake_parts_insert]
- addDs [impOfSubs analz_subset_parts]
- addss (!simpset)) 1);
+ addDs [impOfSubs analz_subset_parts]) 1);
val lemma = result();
goal thy
@@ -155,14 +140,14 @@
by (etac rev_mp 1);
by (analz_induct_tac 1);
(*NS3*)
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
- addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
+by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj]
+ addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
(*NS2*)
-by (deepen_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
- addSEs [MPair_parts]
- addDs [parts.Body, unique_NA]) 0 3);
+by (blast_tac (!claset addSEs [MPair_parts]
+ addDs [Says_imp_sees_Spy' RS parts.Inj,
+ parts.Body, unique_NA]) 3);
(*NS1*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs
+by (blast_tac (!claset addSEs sees_Spy_partsEs
addIs [impOfSubs analz_subset_parts]) 2);
(*Fake*)
by (spy_analz_tac 1);
@@ -184,15 +169,11 @@
by (etac ns_public.induct 1);
by (ALLGOALS Asm_simp_tac);
(*NS1*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 2);
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
(*Fake*)
-by (REPEAT_FIRST (resolve_tac [impI, conjI]));
-by (fast_tac (!claset addss (!simpset)) 1);
-by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1));
-by (best_tac (!claset addSIs [disjI2]
- addSDs [impOfSubs Fake_parts_insert]
- addDs [impOfSubs analz_subset_parts]
- addss (!simpset)) 1);
+by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
+ addDs [Spy_not_see_NA,
+ impOfSubs analz_subset_parts]) 1);
qed "A_trusts_NS2";
(*If the encrypted message appears then it originated with Alice in NS1*)
@@ -205,13 +186,11 @@
by (etac rev_mp 1);
by (analz_induct_tac 1);
(*Fake*)
-by (best_tac (!claset addSIs [disjI2]
- addSDs [impOfSubs Fake_parts_insert]
- addIs [analz_insertI]
- addDs [impOfSubs analz_subset_parts]
- addss (!simpset)) 2);
+by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
+ addIs [analz_insertI]
+ addDs [impOfSubs analz_subset_parts]) 2);
(*Base*)
-by (fast_tac (!claset addss (!simpset)) 1);
+by (Blast_tac 1);
qed "B_trusts_NS1";
@@ -231,17 +210,16 @@
(*NS2*)
by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
by (expand_case_tac "NB = ?y" 3 THEN
- REPEAT (fast_tac (!claset addSEs partsEs) 3));
+ REPEAT (blast_tac (!claset addSEs partsEs) 3));
(*Base*)
-by (fast_tac (!claset addss (!simpset)) 1);
+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 (best_tac (!claset delrules [conjI]
+by (blast_tac (!claset delrules [conjI]
addSDs [impOfSubs Fake_parts_insert]
- addDs [impOfSubs analz_subset_parts]
- addss (!simpset)) 1);
+ addDs [impOfSubs analz_subset_parts]) 1);
val lemma = result();
goal thy
@@ -265,26 +243,21 @@
by (etac rev_mp 1);
by (analz_induct_tac 1);
(*NS3*)
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
- addDs [unique_NB]) 4);
+by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj,
+ unique_NB]) 4);
(*NS1*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 2);
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
(*Fake*)
by (spy_analz_tac 1);
(*NS2*)
by (Step_tac 1);
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 3);
-by (best_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
- addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 2);
-by (fast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1);
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
+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";
-(*Matches only NS2, not NS1 (or NS3)*)
-val Says_imp_sees_Spy'' =
- read_instantiate [("X","Crypt ?K {|?XX,?YY,?ZZ|}")] Says_imp_sees_Spy';
-
-
(*Authentication for B: if he receives message 3 and has used NB
in message 2, then A has sent message 3.*)
goal thy
@@ -296,28 +269,27 @@
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 ns_public.induct 1);
-by (ALLGOALS Asm_simp_tac);
+by (analz_induct_tac 1);
(*NS1*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 2);
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
(*Fake*)
-by (REPEAT_FIRST (resolve_tac [impI, conjI]));
-by (fast_tac (!claset addss (!simpset)) 1);
-by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
-by (best_tac (!claset addSIs [disjI2]
- addSDs [impOfSubs Fake_parts_insert]
- addDs [impOfSubs analz_subset_parts]
- addss (!simpset)) 1);
-(*NS3*)
+by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
+ addDs [Spy_not_see_NB,
+ impOfSubs analz_subset_parts]) 1);
+(*NS3; not clear why blast_tac needs to be preceeded by Step_tac*)
by (Step_tac 1);
-by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
-by (best_tac (!claset addSDs [Says_imp_sees_Spy'' RS parts.Inj]
- addDs [unique_NB]) 1);
+by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj,
+ Spy_not_see_NB, unique_NB]) 1);
qed "B_trusts_NS3";
(**** 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';
+
+
(*If B receives NS3 and the nonce NB agrees with the nonce he joined with
NA, then A initiated the run using NA. SAME proof as B_trusts_NS3!*)
goal thy
@@ -333,19 +305,18 @@
by (ALLGOALS Asm_simp_tac);
(*Fake, NS2, NS3*)
(*NS1*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 2);
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
(*Fake*)
by (REPEAT_FIRST (resolve_tac [impI, conjI]));
-by (fast_tac (!claset addss (!simpset)) 1);
+by (Blast_tac 1);
by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
-by (best_tac (!claset addSIs [disjI2]
+by (blast_tac (!claset addSIs [disjI2]
addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]
- addss (!simpset)) 1);
+ impOfSubs Fake_parts_insert]) 1);
(*NS3*)
by (Step_tac 1);
by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
-by (best_tac (!claset addSDs [Says_imp_sees_Spy'' RS parts.Inj]
- addDs [unique_NB]) 1);
+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_Bad.ML Wed May 07 12:50:26 1997 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.ML Wed May 07 13:01:43 1997 +0200
@@ -16,15 +16,12 @@
proof_timing:=true;
HOL_quantifiers := false;
-val op addss = op unsafe_addss;
-
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. \
@@ -46,17 +43,6 @@
AddSEs [not_Says_to_self RSN (2, rev_notE)];
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
-fun parts_induct_tac i = SELECT_GOAL
- (DETERM (etac ns_public.induct 1 THEN
- (*Fake message*)
- TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]
- addss (!simpset)) 2)) THEN
- (*Base case*)
- fast_tac (!claset addss (!simpset)) 1 THEN
- ALLGOALS Asm_simp_tac) i;
-
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
sends messages containing X! **)
@@ -64,8 +50,9 @@
goal thy
"!!evs. evs : ns_public \
\ ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)";
-by (parts_induct_tac 1);
-by (Auto_tac());
+by (etac ns_public.induct 1);
+by (prove_simple_subgoals_tac 1);
+by (Fake_parts_insert_tac 1);
qed "Spy_see_priK";
Addsimps [Spy_see_priK];
@@ -78,7 +65,7 @@
goal thy "!!A. [| Key (priK A) : parts (sees lost Spy evs); \
\ evs : ns_public |] ==> A:lost";
-by (fast_tac (!claset addDs [Spy_see_priK]) 1);
+by (blast_tac (!claset addDs [Spy_see_priK]) 1);
qed "Spy_see_priK_D";
bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D);
@@ -86,7 +73,7 @@
fun analz_induct_tac i =
- etac ns_public.induct i THEN
+ etac ns_public.induct i THEN
ALLGOALS (asm_simp_tac
(!simpset addsimps [not_parts_not_analz]
setloop split_tac [expand_if]));
@@ -105,16 +92,15 @@
by (etac rev_mp 1);
by (analz_induct_tac 1);
(*NS3*)
-by (fast_tac (!claset addSEs partsEs) 4);
+by (blast_tac (!claset addSEs partsEs) 4);
(*NS2*)
-by (fast_tac (!claset addSEs partsEs) 3);
+by (blast_tac (!claset addSEs partsEs) 3);
(*Fake*)
-by (deepen_tac (!claset addSIs [analz_insertI]
+by (blast_tac (!claset addSIs [analz_insertI]
addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]
- addss (!simpset)) 0 2);
+ impOfSubs Fake_parts_insert]) 2);
(*Base*)
-by (fast_tac (!claset addss (!simpset)) 1);
+by (Blast_tac 1);
qed "no_nonce_NS1_NS2";
@@ -129,17 +115,16 @@
(*NS1*)
by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
by (expand_case_tac "NA = ?y" 3 THEN
- REPEAT (fast_tac (!claset addSEs partsEs) 3));
+ REPEAT (blast_tac (!claset addSEs partsEs) 3));
(*Base*)
-by (fast_tac (!claset addss (!simpset)) 1);
+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 (best_tac (!claset delrules [conjI]
+by (blast_tac (!claset delrules [conjI]
addSDs [impOfSubs Fake_parts_insert]
- addDs [impOfSubs analz_subset_parts]
- addss (!simpset)) 1);
+ addDs [impOfSubs analz_subset_parts]) 1);
val lemma = result();
goal thy
@@ -160,15 +145,15 @@
by (etac rev_mp 1);
by (analz_induct_tac 1);
(*NS3*)
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
- addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
+by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj]
+ addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
(*NS2*)
-by (deepen_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
- addSEs [MPair_parts]
- addDs [parts.Body, unique_NA]) 0 3);
+by (blast_tac (!claset addSEs [MPair_parts]
+ addDs [Says_imp_sees_Spy' RS parts.Inj,
+ parts.Body, unique_NA]) 3);
(*NS1*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs
- addIs [impOfSubs analz_subset_parts]) 2);
+by (blast_tac (!claset addSEs sees_Spy_partsEs
+ addIs [impOfSubs analz_subset_parts]) 2);
(*Fake*)
by (spy_analz_tac 1);
qed "Spy_not_see_NA";
@@ -187,20 +172,15 @@
by (etac ns_public.induct 1);
by (ALLGOALS Asm_simp_tac);
(*NS1*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 2);
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
(*Fake*)
-by (REPEAT_FIRST (resolve_tac [impI, conjI]));
-by (fast_tac (!claset addss (!simpset)) 1);
-by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1));
-by (best_tac (!claset addSIs [disjI2]
- addSDs [impOfSubs Fake_parts_insert]
- addDs [impOfSubs analz_subset_parts]
- addss (!simpset)) 1);
-(*NS2*)
+by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
+ addDs [Spy_not_see_NA,
+ impOfSubs analz_subset_parts]) 1);
+(*NS2; not clear why blast_tac needs to be preceeded by Step_tac*)
by (Step_tac 1);
-by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1));
-by (deepen_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
- addDs [unique_NA]) 1 1);
+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*)
@@ -213,14 +193,12 @@
by (etac rev_mp 1);
by (analz_induct_tac 1);
(*Fake*)
-by (best_tac (!claset addSIs [disjI2]
- addSDs [impOfSubs Fake_parts_insert]
- addIs [analz_insertI]
- addDs [impOfSubs analz_subset_parts]
- addss (!simpset)) 2);
+by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
+ addIs [analz_insertI]
+ addDs [impOfSubs analz_subset_parts]) 2);
(*Base*)
-by (fast_tac (!claset addss (!simpset)) 1);
-qed_spec_mp "B_trusts_NS1";
+by (Blast_tac 1);
+qed "B_trusts_NS1";
@@ -238,17 +216,16 @@
(*NS2*)
by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
by (expand_case_tac "NB = ?y" 3 THEN
- REPEAT (fast_tac (!claset addSEs partsEs) 3));
+ REPEAT (blast_tac (!claset addSEs partsEs) 3));
(*Base*)
-by (fast_tac (!claset addss (!simpset)) 1);
+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 (best_tac (!claset delrules [conjI]
+by (blast_tac (!claset delrules [conjI]
addSDs [impOfSubs Fake_parts_insert]
- addDs [impOfSubs analz_subset_parts]
- addss (!simpset)) 1);
+ addDs [impOfSubs analz_subset_parts]) 1);
val lemma = result();
goal thy
@@ -271,22 +248,21 @@
by (etac rev_mp 1);
by (analz_induct_tac 1);
(*NS1*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 2);
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
(*Fake*)
by (spy_analz_tac 1);
(*NS2 and NS3*)
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
by (step_tac (!claset delrules [allI]) 1);
-by (Fast_tac 5);
-by (fast_tac (!claset addSIs [impOfSubs analz_subset_parts]) 1);
+by (Blast_tac 5);
+(*NS3*)
+by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj,
+ Spy_not_see_NB, unique_NB]) 4);
(*NS2*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 2);
-by (fast_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 (Fast_tac 1);
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
+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";
@@ -305,22 +281,15 @@
by (analz_induct_tac 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
(*NS1*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 2);
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
(*Fake*)
-by (REPEAT_FIRST (resolve_tac [impI, conjI]));
-by (fast_tac (!claset addss (!simpset)) 1);
-by (rtac (ccontr RS disjI2) 1);
-by (forward_tac [Spy_not_see_NB] 1 THEN (REPEAT_FIRST assume_tac)
- THEN Fast_tac 1);
-by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert]
- addDs [impOfSubs analz_subset_parts]
- addss (!simpset)) 1);
-(*NS3*)
+by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
+ addDs [Spy_not_see_NB,
+ impOfSubs analz_subset_parts]) 1);
+(*NS3; not clear why blast_tac needs to be preceeded by Step_tac*)
by (Step_tac 1);
-by (forward_tac [Spy_not_see_NB] 1 THEN (REPEAT_FIRST assume_tac)
- THEN Fast_tac 1);
-by (best_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
- addDs [unique_NB]) 1);
+by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj,
+ Spy_not_see_NB, unique_NB]) 1);
qed "B_trusts_NS3";
@@ -331,18 +300,18 @@
\ --> Nonce NB ~: analz (sees lost Spy evs)";
by (analz_induct_tac 1);
(*NS1*)
-by (fast_tac (!claset addSEs partsEs
- addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
+by (blast_tac (!claset addSEs partsEs
+ addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
(*Fake*)
by (spy_analz_tac 1);
(*NS2 and NS3*)
by (Step_tac 1);
-by (fast_tac (!claset addSIs [impOfSubs analz_subset_parts, usedI]) 1);
+by (blast_tac (!claset addSIs [impOfSubs analz_subset_parts, usedI]) 1);
(*NS2*)
-by (fast_tac (!claset addSEs partsEs
- addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
- addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1);
+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]
+ 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));
--- a/src/HOL/Auth/NS_Shared.ML Wed May 07 12:50:26 1997 +0200
+++ b/src/HOL/Auth/NS_Shared.ML Wed May 07 13:01:43 1997 +0200
@@ -15,6 +15,9 @@
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
@@ -35,7 +38,7 @@
by (rtac subsetI 1);
by (etac ns_shared.induct 1);
by (REPEAT_FIRST
- (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
+ (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
:: ns_shared.intrs))));
qed "ns_shared_mono";
@@ -51,29 +54,23 @@
(*For reasoning about the encrypted portion of message NS3*)
goal thy "!!evs. Says S A (Crypt KA {|N, B, K, X|}) : set_of_list evs \
\ ==> X : parts (sees lost Spy evs)";
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
+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_of_list evs \
\ ==> K : parts (sees lost Spy evs)";
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
qed "Oops_parts_sees_Spy";
-val parts_Fake_tac =
- dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5 THEN
- forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 8;
-
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
-fun parts_induct_tac i = SELECT_GOAL
- (DETERM (etac ns_shared.induct 1 THEN parts_Fake_tac THEN
- (*Fake message*)
- TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]
- addss (!simpset)) 2)) THEN
- (*Base case*)
- fast_tac (!claset addss (!simpset)) 1 THEN
- ALLGOALS Asm_simp_tac) i;
+(*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;
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
@@ -83,8 +80,9 @@
goal thy
"!!evs. evs : ns_shared lost \
\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by (parts_induct_tac 1);
-by (Auto_tac());
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
@@ -97,7 +95,7 @@
goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \
\ evs : ns_shared lost |] ==> A:lost";
-by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
+by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
qed "Spy_see_shrK_D";
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
@@ -107,15 +105,15 @@
(*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 1);
+by parts_induct_tac;
(*Fake*)
by (best_tac
(!claset addIs [impOfSubs analz_subset_parts]
addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
- unsafe_addss (!simpset)) 1);
+ addss (!simpset)) 1);
(*NS2, NS4, NS5*)
-by (REPEAT (fast_tac (!claset addSEs sees_Spy_partsEs addss (!simpset)) 1));
+by (ALLGOALS (blast_tac (!claset addSEs sees_Spy_partsEs)));
qed_spec_mp "new_keys_not_used";
bind_thm ("new_keys_not_analzd",
@@ -152,7 +150,8 @@
\ Crypt (shrK B) {|Key K, Agent A|}|}) \
\ : set_of_list evs";
by (etac rev_mp 1);
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
by (Auto_tac());
qed "A_trusts_NS2";
@@ -163,20 +162,19 @@
goal thy
"!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) \
\ : set_of_list evs; evs : ns_shared lost |] \
-\ ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|})) \
+\ ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|})) \
\ | X : analz (sees lost Spy evs)";
by (case_tac "A : lost" 1);
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
- unsafe_addss (!simpset)) 1);
+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 (fast_tac (!claset addEs partsEs
- addSDs [A_trusts_NS2, Says_Server_message_form]
- addss (!simpset)) 1);
+by (blast_tac (!claset addEs partsEs
+ addSDs [A_trusts_NS2, Says_Server_message_form]) 1);
qed "Says_S_message_form";
(*For proofs involving analz. We again instantiate the variable to "lost".*)
-val analz_Fake_tac =
+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
REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac);
@@ -200,15 +198,12 @@
"!!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 (etac ns_shared.induct 1);
-by parts_Fake_tac;
-by (ALLGOALS Asm_simp_tac);
+by parts_induct_tac;
(*Deals with Faked messages*)
-by (best_tac (!claset addSEs partsEs
- addDs [impOfSubs parts_insert_subset_Un]
- addss (!simpset)) 2);
+by (blast_tac (!claset addSEs partsEs
+ addDs [impOfSubs parts_insert_subset_Un]) 1);
(*Base, NS4 and NS5*)
-by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+by (Auto_tac());
result();
@@ -221,7 +216,7 @@
\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
\ (K : KK | Key K : analz (sees lost Spy evs))";
by (etac ns_shared.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
by (REPEAT_FIRST (resolve_tac [allI, impI]));
by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
(*Takes 24 secs*)
@@ -229,7 +224,7 @@
(*NS4, Fake*)
by (EVERY (map spy_analz_tac [3,2]));
(*Base*)
-by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
+by (Blast_tac 1);
qed_spec_mp "analz_image_freshK";
@@ -253,13 +248,12 @@
by (Step_tac 1);
(*NS3*)
by (ex_strip_tac 2);
-by (Fast_tac 2);
+by (Blast_tac 2);
(*NS2: it can't be a new key*)
by (expand_case_tac "K = ?y" 1);
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
-by (fast_tac (!claset delrules [conjI] (*prevent split-up into 4 subgoals*)
- addSEs sees_Spy_partsEs
- addss (!simpset addsimps [parts_insertI])) 1);
+by (blast_tac (!claset delrules [conjI] (*prevent split-up into 4 subgoals*)
+ addSEs sees_Spy_partsEs) 1);
val lemma = result();
(*In messages of this form, the session key uniquely identifies the rest*)
@@ -286,7 +280,7 @@
\ (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs) --> \
\ Key K ~: analz (sees lost Spy evs)";
by (etac ns_shared.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
by (ALLGOALS
(asm_simp_tac
(!simpset addsimps ([not_parts_not_analz, analz_insert_freshK] @ pushes)
@@ -294,17 +288,16 @@
(*NS4, Fake*)
by (EVERY (map spy_analz_tac [4,1]));
(*NS2*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs
- addIs [parts_insertI, impOfSubs analz_subset_parts]
- addss (!simpset)) 1);
+by (blast_tac (!claset addSEs sees_Spy_partsEs
+ addIs [parts_insertI, impOfSubs analz_subset_parts]) 1);
(*Oops*)
-by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 2);
+by (blast_tac (!claset addDs [unique_session_keys]) 2);
(*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 (fast_tac (!claset addSEs [Says_Crypt_not_lost]) 1);
-by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
+by (blast_tac (!claset addSDs [Says_Crypt_not_lost]) 1);
+by (blast_tac (!claset addDs [unique_session_keys]) 1);
val lemma = result() RS mp RS mp RSN(2,rev_notE);
@@ -316,7 +309,7 @@
\ A ~: lost; B ~: lost; evs : ns_shared lost \
\ |] ==> Key K ~: analz (sees lost Spy evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
-by (fast_tac (!claset addSEs [lemma]) 1);
+by (blast_tac (!claset addSDs [lemma]) 1);
qed "Spy_not_see_encrypted_key";
@@ -330,7 +323,7 @@
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
-by (REPEAT_FIRST (fast_tac (!claset addIs [ns_shared_mono RS subsetD])));
+by (REPEAT_FIRST (blast_tac (!claset addIs [ns_shared_mono RS subsetD])));
qed "Agent_not_see_encrypted_key";
@@ -349,13 +342,10 @@
\ Crypt (shrK B) {|Key K, Agent A|}|}) \
\ : set_of_list evs";
by (etac rev_mp 1);
-by (etac ns_shared.induct 1);
-by parts_Fake_tac;
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
(*Fake case*)
-by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert]
- addDs [impOfSubs analz_subset_parts]
- addss (!simpset)) 2);
-by (Auto_tac());
+by (ALLGOALS Blast_tac);
qed "B_trusts_NS3";
@@ -368,28 +358,28 @@
\ Says B A (Crypt K (Nonce NB)) : set_of_list evs";
by (etac ns_shared.induct 1);
by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);
-by parts_Fake_tac;
+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 (TRYALL (rtac impI));
by (REPEAT_FIRST
(dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD)));
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
-(**LEVEL 6**)
-by (fast_tac (!claset addSDs [Crypt_Fake_parts_insert]
- addDs [impOfSubs analz_subset_parts]) 1);
-by (Fast_tac 2);
+(**LEVEL 7**)
+by (blast_tac (!claset addSDs [Crypt_Fake_parts_insert]
+ addDs [impOfSubs analz_subset_parts]) 1);
+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) *)
by (dtac Crypt_imp_invKey_keysFor 1);
-(**LEVEL 10**)
+(**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 (dtac Says_Crypt_lost 1 THEN assume_tac 1 THEN Fast_tac 1);
-by (dtac (Says_imp_sees_Spy RS parts.Inj RS B_trusts_NS3) 1 THEN
- REPEAT (assume_tac 1));
-by (best_tac (!claset addDs [unique_session_keys]) 1);
+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_Crypt_lost]) 1);
val lemma = result();
goal thy
@@ -399,6 +389,6 @@
\ ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs; \
\ A ~: lost; B ~: lost; evs : ns_shared lost |] \
\ ==> Says B A (Crypt K (Nonce NB)) : set_of_list evs";
-by (fast_tac (!claset addSIs [lemma RS mp RS mp RS mp]
- addSEs [Spy_not_see_encrypted_key RSN (2, rev_notE)]) 1);
+by (blast_tac (!claset addSIs [lemma RS mp RS mp RS mp]
+ addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1);
qed "A_trusts_NS4";
--- a/src/HOL/Auth/OtwayRees.ML Wed May 07 12:50:26 1997 +0200
+++ b/src/HOL/Auth/OtwayRees.ML Wed May 07 13:01:43 1997 +0200
@@ -18,8 +18,7 @@
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;
+val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy;
(*A "possibility property": there are traces that reach the end*)
@@ -81,35 +80,30 @@
bind_thm ("OR4_parts_sees_Spy",
OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
-(*We instantiate the variable to "lost". Leaving it as a Var makes proofs
- harder to complete, since simplification does less for us.*)
-val parts_Fake_tac =
+(*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 tac OR2_parts_sees_Spy 4 THEN
+ 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
+ tac Oops_parts_sees_Spy 7 THEN
+ prove_simple_subgoals_tac 1
end;
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
-fun parts_induct_tac i = SELECT_GOAL
- (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN
- (*Fake message*)
- TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]
- unsafe_addss (!simpset)) 2)) THEN
- (*Base case*)
- fast_tac (!claset unsafe_addss (!simpset)) 1 THEN
- ALLGOALS Asm_simp_tac) i;
(** Theorems of the form X ~: parts (sees lost 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 1);
-by (Auto_tac());
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
@@ -132,7 +126,7 @@
(*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 1);
+by parts_induct_tac;
(*Fake*)
by (best_tac
(!claset addIs [impOfSubs analz_subset_parts]
@@ -167,7 +161,7 @@
(*For proofs involving analz. We again instantiate the variable to "lost".*)
-val analz_Fake_tac =
+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
@@ -194,7 +188,7 @@
\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
\ (K : KK | Key K : analz (sees lost Spy evs))";
by (etac otway.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
by (REPEAT_FIRST (resolve_tac [allI, impI]));
by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
@@ -254,7 +248,8 @@
\ Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
\ : set_of_list evs";
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
qed_spec_mp "Crypt_imp_OR1";
@@ -265,7 +260,8 @@
\ ==> EX B'. ALL B. \
\ Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (sees lost Spy evs) \
\ --> B = B'";
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
by (simp_tac (!simpset addsimps [all_conj_distrib]) 1);
(*OR1: creation of new Nonce. Move assertion into global context*)
by (expand_case_tac "NA = ?y" 1);
@@ -290,7 +286,8 @@
\ : parts (sees lost Spy evs) --> \
\ Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \
\ ~: parts (sees lost Spy evs)";
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
by (REPEAT (blast_tac (!claset addSEs sees_Spy_partsEs
addSDs [impOfSubs parts_insert_subset_Un]) 1));
qed_spec_mp"no_nonce_OR1_OR2";
@@ -309,7 +306,8 @@
\ Crypt (shrK A) {|NA, Key K|}, \
\ Crypt (shrK B) {|NB, Key K|}|} \
\ : set_of_list evs)";
-by (parts_induct_tac 1);
+by parts_induct_tac;
+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);
(*OR3 and OR4*)
@@ -364,7 +362,7 @@
\ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs --> \
\ Key K ~: analz (sees lost Spy evs)";
by (etac otway.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
by (ALLGOALS
(asm_simp_tac (!simpset addcongs [conj_cong]
addsimps [not_parts_not_analz, analz_insert_freshK]
@@ -418,7 +416,8 @@
\ {|NA, Agent A, Agent B, X, \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \
\ : set_of_list evs)";
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
by (ALLGOALS Blast_tac);
bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE);
@@ -430,7 +429,8 @@
\ ==> EX NA' A'. ALL NA A. \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(sees lost Spy evs) \
\ --> NA = NA' & A = A'";
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
by (simp_tac (!simpset addsimps [all_conj_distrib]) 1);
(*OR2: creation of new Nonce. Move assertion into global context*)
by (expand_case_tac "NB = ?y" 1);
@@ -461,7 +461,8 @@
\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
\ Crypt (shrK B) {|NB, Key K|}|} \
\ : set_of_list evs)";
-by (parts_induct_tac 1);
+by parts_induct_tac;
+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);
(*OR4*)
--- a/src/HOL/Auth/OtwayRees_AN.ML Wed May 07 12:50:26 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML Wed May 07 13:01:43 1997 +0200
@@ -69,22 +69,17 @@
bind_thm ("OR4_parts_sees_Spy",
OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
-(*We instantiate the variable to "lost". Leaving it as a Var makes proofs
- harder to complete, since simplification does less for us.*)
-val parts_Fake_tac =
- forw_inst_tac [("lost","lost")] OR4_parts_sees_Spy 6 THEN
- forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 7;
+(*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 lost Spy evs) *)
-fun parts_induct_tac i = SELECT_GOAL
- (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN
- (*Fake message*)
- TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]
- addss (!simpset)) 2)) THEN
- (*Base case*)
- fast_tac (!claset addss (!simpset)) 1 THEN
- ALLGOALS Asm_simp_tac) i;
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
sends messages containing X! **)
@@ -93,8 +88,9 @@
goal thy
"!!evs. evs : otway lost \
\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by (parts_induct_tac 1);
-by (Auto_tac());
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
@@ -117,7 +113,7 @@
(*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 1);
+by parts_induct_tac;
(*Fake*)
by (best_tac
(!claset addIs [impOfSubs analz_subset_parts]
@@ -154,7 +150,7 @@
(*For proofs involving analz. We again instantiate the variable to "lost".*)
-val analz_Fake_tac =
+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
assume_tac 7 THEN
@@ -180,7 +176,7 @@
\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
\ (K : KK | Key K : analz (sees lost Spy evs))";
by (etac otway.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
by (REPEAT_FIRST (resolve_tac [allI, impI]));
by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
(*14 seconds*)
@@ -250,7 +246,8 @@
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
\ : set_of_list evs)";
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
(*OR3*)
by (Blast_tac 1);
@@ -285,7 +282,7 @@
\ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs --> \
\ Key K ~: analz (sees lost Spy evs)";
by (etac otway.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
by (ALLGOALS
(asm_simp_tac (!simpset addcongs [conj_cong]
addsimps [not_parts_not_analz,
@@ -340,7 +337,8 @@
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
\ : set_of_list evs)";
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
(*OR3*)
by (Blast_tac 1);
--- a/src/HOL/Auth/OtwayRees_Bad.ML Wed May 07 12:50:26 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Wed May 07 13:01:43 1997 +0200
@@ -20,9 +20,11 @@
proof_timing:=true;
HOL_quantifiers := false;
-(*No need to declare Says_imp_sees_Spy' because "lost" is a CONSTANT*)
+(*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;
-(*Weak liveness: there are traces that reach the end*)
+(*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. \
@@ -49,12 +51,12 @@
goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs ==> \
\ X : analz (sees lost Spy evs)";
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
+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_of_list evs ==> \
\ X : analz (sees lost Spy evs)";
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
+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_of_list evs \
@@ -72,21 +74,13 @@
bind_thm ("OR4_parts_sees_Spy",
OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
-val parts_Fake_tac =
+(*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;
-
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
-fun parts_induct_tac i = SELECT_GOAL
- (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN
- (*Fake message*)
- TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]
- addss (!simpset)) 2)) THEN
- (*Base case*)
- fast_tac (!claset addss (!simpset)) 1 THEN
- ALLGOALS Asm_simp_tac) i;
+ forward_tac [Oops_parts_sees_Spy] 7 THEN
+ prove_simple_subgoals_tac 1;
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
@@ -96,8 +90,9 @@
goal thy
"!!evs. evs : otway \
\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by (parts_induct_tac 1);
-by (Auto_tac());
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
@@ -120,7 +115,7 @@
(*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 1);
+by parts_induct_tac;
(*Fake*)
by (best_tac
(!claset addIs [impOfSubs analz_subset_parts]
@@ -128,7 +123,7 @@
impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
unsafe_addss (!simpset)) 1);
(*OR1-3*)
-by (REPEAT (fast_tac (!claset addss (!simpset)) 1));
+by (ALLGOALS Blast_tac);
qed_spec_mp "new_keys_not_used";
bind_thm ("new_keys_not_analzd",
@@ -150,12 +145,13 @@
\ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
by (etac rev_mp 1);
by (etac otway.induct 1);
-by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+by (prove_simple_subgoals_tac 1);
+by (Blast_tac 1);
qed "Says_Server_message_form";
(*For proofs involving analz.*)
-val analz_Fake_tac =
+val analz_sees_tac =
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
@@ -181,12 +177,12 @@
\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
\ (K : KK | Key K : analz (sees lost Spy evs))";
by (etac otway.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
by (REPEAT_FIRST (resolve_tac [allI, impI]));
by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
(*Base*)
-by (blast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
+by (Blast_tac 1);
(*Fake, OR2, OR4*)
by (REPEAT (spy_analz_tac 1));
qed_spec_mp "analz_image_freshK";
@@ -217,8 +213,7 @@
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] (*no split-up to 4 subgoals*)) 1);
val lemma = result();
goal thy
@@ -240,7 +235,7 @@
\ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs --> \
\ Key K ~: analz (sees lost Spy evs)";
by (etac otway.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
by (ALLGOALS
(asm_simp_tac (!simpset addcongs [conj_cong]
addsimps [not_parts_not_analz, analz_insert_freshK]
@@ -280,7 +275,8 @@
\ Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
\ : set_of_list evs";
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
by (Blast_tac 1);
qed_spec_mp "Crypt_imp_OR1";
@@ -300,7 +296,8 @@
\ Crypt (shrK A) {|NA, Key K|}, \
\ Crypt (shrK B) {|NB, Key K|}|} \
\ : set_of_list evs)";
-by (parts_induct_tac 1);
+by parts_induct_tac;
+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);
--- a/src/HOL/Auth/Public.ML Wed May 07 12:50:26 1997 +0200
+++ b/src/HOL/Auth/Public.ML Wed May 07 13:01:43 1997 +0200
@@ -80,7 +80,7 @@
(*Added for Yahalom/lost_tac*)
goal thy "!!A. [| Crypt (pubK A) X : analz (sees lost Spy evs); A: lost |] \
\ ==> X : analz (sees lost Spy evs)";
-by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
+by (blast_tac (!claset addSDs [analz.Decrypt]) 1);
qed "Crypt_Spy_analz_lost";
(** Specialized rewrite rules for (sees lost A (Says...#evs)) **)
@@ -120,8 +120,8 @@
by (Step_tac 1);
by (etac rev_mp 1); (*split_tac does not work on assumptions*)
by (ALLGOALS
- (fast_tac (!claset addss (!simpset addsimps [parts_Un, sees_Cons]
- setloop split_tac [expand_if]))));
+ (fast_tac (!claset unsafe_addss (!simpset addsimps [parts_Un, sees_Cons]
+ setloop split_tac [expand_if]))));
qed "UN_parts_sees_Says";
goal thy "Says A B X : set_of_list evs --> X : sees lost Spy evs";
@@ -136,16 +136,14 @@
goal thy
"!!evs. [| Says A B (Crypt (pubK C) X) : set_of_list evs; C : lost |] \
\ ==> X : analz (sees lost Spy evs)";
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
- addss (!simpset)) 1);
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "Says_Crypt_lost";
goal thy
"!!evs. [| Says A B (Crypt (pubK C) X) : set_of_list evs; \
\ X ~: analz (sees lost Spy evs) |] \
\ ==> C ~: lost";
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
- addss (!simpset)) 1);
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "Says_Crypt_not_lost";
Addsimps [sees_own, sees_Server, sees_Friend, sees_Spy];
--- a/src/HOL/Auth/ROOT.ML Wed May 07 12:50:26 1997 +0200
+++ b/src/HOL/Auth/ROOT.ML Wed May 07 13:01:43 1997 +0200
@@ -12,6 +12,9 @@
proof_timing := true;
goals_limit := 1;
+(*New version of addss isn't ready--too slow*)
+val op addss = op unsafe_addss;
+
(*Shared-key protocols*)
time_use_thy "NS_Shared";
time_use_thy "OtwayRees";
--- a/src/HOL/Auth/Recur.ML Wed May 07 12:50:26 1997 +0200
+++ b/src/HOL/Auth/Recur.ML Wed May 07 13:01:43 1997 +0200
@@ -82,7 +82,7 @@
by (rtac subsetI 1);
by (etac recur.induct 1);
by (REPEAT_FIRST
- (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
+ (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
:: recur.intrs))));
qed "recur_mono";
@@ -128,7 +128,7 @@
goal thy "!!evs. Says C' B {|Crypt K X, X', RA|} : set_of_list evs \
\ ==> RA : analz (sees lost Spy evs)";
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "RA4_analz_sees_Spy";
(*RA2_analz... and RA4_analz... let us treat those cases using the same
@@ -141,26 +141,19 @@
bind_thm ("RA4_parts_sees_Spy",
RA4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
-(*We instantiate the variable to "lost". Leaving it as a Var makes proofs
- harder to complete, since simplification does less for us.*)
-val parts_Fake_tac =
+(*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 tac RA2_parts_sees_Spy 4 THEN
+ 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
+ tac RA4_parts_sees_Spy 6 THEN
+ prove_simple_subgoals_tac 1
end;
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
-fun parts_induct_tac i = SELECT_GOAL
- (DETERM (etac recur.induct 1 THEN parts_Fake_tac THEN
- (*Fake message*)
- TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]
- unsafe_addss (!simpset)) 2)) THEN
- (*Base case*)
- fast_tac (!claset unsafe_addss (!simpset)) 1 THEN
- ALLGOALS Asm_simp_tac) i;
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
sends messages containing X! **)
@@ -171,14 +164,14 @@
goal thy
"!!evs. evs : recur lost \
\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by (parts_induct_tac 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
+by (ALLGOALS
+ (asm_simp_tac (!simpset addsimps [parts_insert2, parts_insert_sees])));
(*RA3*)
-by (fast_tac (!claset addDs [Key_in_parts_respond]
- addss (!simpset addsimps [parts_insert_sees])) 2);
+by (blast_tac (!claset addDs [Key_in_parts_respond]) 2);
(*RA2*)
-by (best_tac (!claset addSEs partsEs addSDs [parts_cut]
- unsafe_addss (!simpset)) 1);
+by (blast_tac (!claset addSEs partsEs addDs [parts_cut]) 1);
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
@@ -191,7 +184,7 @@
goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \
\ evs : recur lost |] ==> A:lost";
-by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
+by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
qed "Spy_see_shrK_D";
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
@@ -212,10 +205,10 @@
goal thy "!!evs. evs : recur lost ==> \
\ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
-by (parts_induct_tac 1);
+by parts_induct_tac;
(*RA3*)
by (best_tac (!claset addDs [Key_in_keysFor_parts]
- unsafe_addss (!simpset addsimps [parts_insert_sees])) 2);
+ unsafe_addss (!simpset addsimps [parts_insert_sees])) 2);
(*Fake*)
by (best_tac
(!claset addIs [impOfSubs analz_subset_parts]
@@ -236,7 +229,7 @@
(*** Proofs involving analz ***)
(*For proofs involving analz. We again instantiate the variable to "lost".*)
-val analz_Fake_tac =
+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
forward_tac [respond_imp_responses] 5 THEN
@@ -267,14 +260,14 @@
\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
\ (K : KK | Key K : analz (sees lost Spy evs))";
by (etac recur.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
by (REPEAT_FIRST (resolve_tac [allI, impI]));
by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
by (ALLGOALS
(asm_simp_tac
(analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
(*Base*)
-by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
+by (Blast_tac 1);
(*RA4, RA2, Fake*)
by (REPEAT (spy_analz_tac 1));
val raw_analz_image_freshK = result();
@@ -304,17 +297,13 @@
\ evs : recur lost; A ~: lost |] \
\ ==> X : parts (sees lost Spy evs)";
by (etac rev_mp 1);
-by (etac recur.induct 1);
-by parts_Fake_tac;
+by parts_induct_tac;
(*RA3 requires a further induction*)
-by (etac responses.induct 5);
+by (etac responses.induct 2);
by (ALLGOALS Asm_simp_tac);
(*Fake*)
-by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]
- addss (!simpset addsimps [parts_insert_sees])) 2);
-(*Two others*)
-by (REPEAT (fast_tac (!claset addss (!simpset)) 1));
+by (simp_tac (!simpset addsimps [parts_insert_sees]) 1);
+by (Fake_parts_insert_tac 1);
qed "Hash_imp_body";
@@ -329,14 +318,15 @@
\ ==> EX B' P'. ALL B P. \
\ Hash {|Key(shrK A), Agent A, B, NA, P|} : parts (sees lost Spy evs) \
\ --> B=B' & P=P'";
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
by (etac responses.induct 3);
by (ALLGOALS (simp_tac (!simpset addsimps [all_conj_distrib])));
by (step_tac (!claset addSEs partsEs) 1);
(*RA1,2: creation of new Nonce. Move assertion into global context*)
by (ALLGOALS (expand_case_tac "NA = ?y"));
by (REPEAT_FIRST (ares_tac [exI]));
-by (REPEAT (best_tac (!claset addSDs [Hash_imp_body]
+by (REPEAT (blast_tac (!claset addSDs [Hash_imp_body]
addSEs sees_Spy_partsEs) 1));
val lemma = result();
@@ -379,7 +369,7 @@
(analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
(*Simplification using two distinct treatments of "image"*)
by (simp_tac (!simpset addsimps [parts_insert2]) 1);
-by (fast_tac (!claset delrules [allE]) 1);
+by (blast_tac (!claset delrules [allE]) 1);
qed "resp_analz_insert_lemma";
bind_thm ("resp_analz_insert",
@@ -417,11 +407,11 @@
by (etac respond.induct 1);
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [all_conj_distrib])));
(*Base case*)
-by (Fast_tac 1);
+by (Blast_tac 1);
by (Step_tac 1);
by (expand_case_tac "K = KBC" 1);
by (dtac respond_Key_in_parts 1);
-by (best_tac (!claset addSIs [exI]
+by (blast_tac (!claset addSIs [exI]
addSEs partsEs
addDs [Key_in_parts_respond]) 1);
by (expand_case_tac "K = KAB" 1);
@@ -457,19 +447,18 @@
(analz_image_freshK_ss addsimps
[shrK_in_analz_respond, resp_analz_image_freshK, parts_insert2])));
by (ALLGOALS Simp_tac);
-by (fast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1);
+by (blast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1);
by (step_tac (!claset addSEs [MPair_parts]) 1);
(** LEVEL 7 **)
-by (fast_tac (!claset addSDs [resp_analz_insert, Key_in_parts_respond]
+by (blast_tac (!claset addSDs [resp_analz_insert, Key_in_parts_respond]
addDs [impOfSubs analz_subset_parts]) 4);
-by (fast_tac (!claset addSDs [respond_certificate]) 3);
-by (best_tac (!claset addSEs partsEs
- addDs [Key_in_parts_respond]
- addss (!simpset)) 2);
+by (blast_tac (!claset addSDs [respond_certificate]) 3);
+by (blast_tac (!claset addSEs partsEs
+ addDs [Key_in_parts_respond]) 2);
by (dtac unique_session_keys 1);
by (etac respond_certificate 1);
by (assume_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed_spec_mp "respond_Spy_not_see_session_key";
@@ -480,7 +469,7 @@
\ ==> Key K ~: analz (sees lost Spy evs)";
by (etac rev_mp 1);
by (etac recur.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
by (ALLGOALS
(asm_simp_tac
(!simpset addsimps [parts_insert_sees, analz_insert_freshK]
@@ -492,17 +481,16 @@
(*Fake*)
by (spy_analz_tac 2);
(*Base*)
-by (fast_tac (!claset addss (!simpset)) 1);
+by (Blast_tac 1);
(*RA3 remains*)
by (step_tac (!claset delrules [impCE]) 1);
(*RA3, case 2: K is an old key*)
-by (best_tac (!claset addSDs [resp_analz_insert]
- addSEs partsEs
- addDs [Key_in_parts_respond]
- addss (!simpset)) 2);
+by (blast_tac (!claset addSDs [resp_analz_insert]
+ addSEs partsEs
+ addDs [Key_in_parts_respond]) 2);
(*RA3, case 1: use lemma previously proved by induction*)
-by (fast_tac (!claset addSEs [respond_Spy_not_see_session_key RSN
- (2,rev_notE)]) 1);
+by (blast_tac (!claset addSEs [respond_Spy_not_see_session_key RSN
+ (2,rev_notE)]) 1);
qed "Spy_not_see_session_key";
@@ -516,8 +504,8 @@
by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
by (FIRSTGOAL (rtac Spy_not_see_session_key));
by (REPEAT_FIRST
- (deepen_tac
- (!claset addIs (map impOfSubs [recur_mono, parts_mono, sees_mono])) 0));
+ (blast_tac
+ (!claset addIs (map impOfSubs [recur_mono, parts_mono, sees_mono]))));
qed "Agent_not_see_session_key";
@@ -544,9 +532,10 @@
\ ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) \
\ : set_of_list evs";
by (etac rev_mp 1);
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
(*RA3*)
-by (fast_tac (!claset addSDs [Hash_in_parts_respond]) 1);
+by (blast_tac (!claset addSDs [Hash_in_parts_respond]) 1);
qed_spec_mp "Hash_auth_sender";
(** These two results subsume (for all agents) the guarantees proved
@@ -561,18 +550,15 @@
\ ==> EX C RC. Says Server C RC : set_of_list evs & \
\ Crypt (shrK A) Y : parts {RC}";
by (etac rev_mp 1);
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
(*RA4*)
-by (Fast_tac 4);
+by (Blast_tac 4);
(*RA3*)
by (full_simp_tac (!simpset addsimps [parts_insert_sees]) 3
- THEN Fast_tac 3);
+ THEN Blast_tac 3);
(*RA1*)
-by (Fast_tac 1);
+by (Blast_tac 1);
(*RA2: it cannot be a new Nonce, contradiction.*)
-by (deepen_tac (!claset delrules [impCE]
- addSIs [disjI2]
- addSEs [MPair_parts]
- addDs [parts.Body]
- unsafe_addss (!simpset)) 0 1);
+by (Blast_tac 1);
qed "Cert_imp_Server_msg";
--- a/src/HOL/Auth/Shared.ML Wed May 07 12:50:26 1997 +0200
+++ b/src/HOL/Auth/Shared.ML Wed May 07 13:01:43 1997 +0200
@@ -56,7 +56,7 @@
goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}";
by (agent.induct_tac "C" 1);
-by (auto_tac (!claset addIs [range_eqI], !simpset));
+by (Auto_tac ());
qed "keysFor_parts_initState";
Addsimps [keysFor_parts_initState];
@@ -210,14 +210,14 @@
(** Fresh keys never clash with long-term shared keys **)
goal thy "Key (shrK A) : used evs";
-by (Best_tac 1);
+by (Blast_tac 1);
qed "shrK_in_used";
AddIffs [shrK_in_used];
-(*Used in parts_Fake_tac and analz_Fake_tac to distinguish session keys
+(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
from long-term shared keys*)
goal thy "!!K. Key K ~: used evs ==> K ~: range shrK";
-by (Best_tac 1);
+by (Blast_tac 1);
qed "Key_not_used";
(*A session key cannot clash with a long-term shared key*)
@@ -237,7 +237,7 @@
by (list.induct_tac "l" 1);
by (event.induct_tac "a" 2);
by (ALLGOALS Asm_simp_tac);
-by (Best_tac 1);
+by (Blast_tac 1);
qed "used_nil_subset";
goal thy "used l <= used (l@l')";
@@ -245,7 +245,7 @@
by (simp_tac (!simpset addsimps [used_nil_subset]) 1);
by (event.induct_tac "a" 1);
by (Asm_simp_tac 1);
-by (Best_tac 1);
+by (Blast_tac 1);
qed "used_subset_append";
@@ -372,8 +372,8 @@
goal thy "sees lost A evs <= initState lost A Un sees lost Spy evs";
by (list.induct_tac "evs" 1);
by (event.induct_tac "a" 2);
-by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD]
- addss (!simpset))));
+by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (blast_tac (!claset addDs [sees_Says_subset_insert RS subsetD])));
qed "sees_agent_subset_sees_Spy";
(*The Spy can see more than anybody else who's lost their key!*)
@@ -381,7 +381,8 @@
by (list.induct_tac "evs" 1);
by (event.induct_tac "a" 2);
by (agent.induct_tac "A" 1);
-by (auto_tac (!claset addDs [sees_Says_subset_insert RS subsetD], (!simpset)));
+by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (blast_tac (!claset addDs [sees_Says_subset_insert RS subsetD])));
qed_spec_mp "sees_lost_agent_subset_sees_Spy";
--- a/src/HOL/Auth/WooLam.ML Wed May 07 12:50:26 1997 +0200
+++ b/src/HOL/Auth/WooLam.ML Wed May 07 13:01:43 1997 +0200
@@ -28,8 +28,7 @@
woolam.WL4 RS woolam.WL5) 2);
by (ALLGOALS (simp_tac (!simpset setSolver safe_solver)));
by (REPEAT_FIRST (resolve_tac [refl, conjI]));
-by (REPEAT_FIRST (fast_tac (!claset addSEs [Nonce_supply RS notE]
- addss (!simpset setSolver safe_solver))));
+by (REPEAT_FIRST (blast_tac (!claset addSEs [Nonce_supply RS notE])));
result();
@@ -54,18 +53,12 @@
bind_thm ("WL4_parts_sees_Spy",
WL4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
-val parts_Fake_tac = forward_tac [WL4_parts_sees_Spy] 6;
+(*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
+ prove_simple_subgoals_tac 1;
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
-fun parts_induct_tac i = SELECT_GOAL
- (DETERM (etac woolam.induct 1 THEN parts_Fake_tac THEN
- (*Fake message*)
- TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]
- addss (!simpset)) 2)) THEN
- (*Base case*)
- fast_tac (!claset addss (!simpset)) 1 THEN
- ALLGOALS Asm_simp_tac) i;
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
sends messages containing X! **)
@@ -74,8 +67,8 @@
goal thy
"!!evs. evs : woolam \
\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by (parts_induct_tac 1);
-by (Auto_tac());
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
@@ -88,7 +81,7 @@
goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \
\ evs : woolam |] ==> A:lost";
-by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
+by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
qed "Spy_see_shrK_D";
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
@@ -105,8 +98,9 @@
"!!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_of_list evs)";
-by (parts_induct_tac 1);
-by (Fast_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
qed_spec_mp "NB_Crypt_imp_Alice_msg";
(*Guarantee for Server: if it gets a message containing a certificate from
@@ -117,7 +111,7 @@
\ Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \
\ : set_of_list evs |] \
\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
-by (fast_tac (!claset addSIs [NB_Crypt_imp_Alice_msg]
+by (blast_tac (!claset addSIs [NB_Crypt_imp_Alice_msg]
addSEs [MPair_parts]
addDs [Says_imp_sees_Spy RS parts.Inj]) 1);
qed "Server_trusts_WL4";
@@ -131,8 +125,9 @@
\ Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs \
\ --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \
\ : set_of_list evs)";
-by (parts_induct_tac 1);
-by (ALLGOALS Fast_tac);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
+by (ALLGOALS Blast_tac);
bind_thm ("Server_sent_WL5", result() RSN (2, rev_mp));
@@ -141,7 +136,8 @@
"!!evs. [| B ~: lost; evs : woolam |] \
\ ==> Crypt (shrK B) {|Agent A, NB|} : parts (sees lost Spy evs) \
\ --> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs";
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
qed_spec_mp "NB_Crypt_imp_Server_msg";
(*Partial guarantee for B: if it gets a message of correct form then the Server
@@ -150,7 +146,7 @@
"!!evs. [| Says S B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs; \
\ B ~: lost; evs : woolam |] \
\ ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs";
-by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
+by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
addDs [Says_imp_sees_Spy RS parts.Inj]) 1);
qed "B_got_WL5";
@@ -162,7 +158,7 @@
"!!evs. [| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set_of_list evs; \
\ A ~: lost; B ~: lost; evs : woolam |] \
\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
-by (fast_tac (!claset addIs [Server_trusts_WL4]
+by (blast_tac (!claset addIs [Server_trusts_WL4]
addSDs [B_got_WL5 RS Server_sent_WL5]) 1);
qed "B_trusts_WL5";
@@ -172,8 +168,9 @@
"!!evs. [| B ~= Spy; evs : woolam |] \
\ ==> Says B A (Nonce NB) : set_of_list evs \
\ --> (EX A'. Says A' B (Agent A) : set_of_list evs)";
-by (parts_induct_tac 1);
-by (ALLGOALS Fast_tac);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
+by (ALLGOALS Blast_tac);
bind_thm ("B_said_WL2", result() RSN (2, rev_mp));
@@ -183,7 +180,8 @@
\ ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs) & \
\ Says B A (Nonce NB) : set_of_list evs \
\ --> Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
by (Step_tac 1);
-by (best_tac (!claset addSEs partsEs) 1);
+by (blast_tac (!claset addSEs partsEs) 1);
**)
--- a/src/HOL/Auth/Yahalom.ML Wed May 07 12:50:26 1997 +0200
+++ b/src/HOL/Auth/Yahalom.ML Wed May 07 13:01:43 1997 +0200
@@ -16,7 +16,8 @@
HOL_quantifiers := false;
Pretty.setdepth 25;
-val op addss = op unsafe_addss;
+(*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*)
@@ -38,7 +39,7 @@
by (rtac subsetI 1);
by (etac yahalom.induct 1);
by (REPEAT_FIRST
- (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
+ (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
:: yahalom.intrs))));
qed "yahalom_mono";
@@ -57,7 +58,7 @@
(*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_of_list evs ==> \
\ X : analz (sees lost Spy evs)";
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
qed "YM4_analz_sees_Spy";
bind_thm ("YM4_parts_sees_Spy",
@@ -67,26 +68,20 @@
goal thy "!!evs. Says S A {|Crypt (shrK A) {|B, K, NA, NB|}, X|} \
\ : set_of_list evs ==> \
\ K : parts (sees lost Spy evs)";
-by (fast_tac (!claset addSEs partsEs
- addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
+by (blast_tac (!claset addSEs partsEs
+ addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
qed "YM4_Key_parts_sees_Spy";
-(*We instantiate the variable to "lost". Leaving it as a Var makes proofs
- harder: the simplifier does less.*)
-val parts_Fake_tac =
- forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6 THEN
- forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7;
+(*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 lost Spy evs) *)
-fun parts_induct_tac i = SELECT_GOAL
- (DETERM (etac yahalom.induct 1 THEN parts_Fake_tac THEN
- (*Fake message*)
- TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]
- addss (!simpset)) 2)) THEN
- (*Base case*)
- fast_tac (!claset addss (!simpset)) 1 THEN
- ALLGOALS Asm_simp_tac) i;
+val parts_induct_tac =
+ etac yahalom.induct 1 THEN parts_sees_tac;
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
@@ -96,8 +91,9 @@
goal thy
"!!evs. evs : yahalom lost \
\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by (parts_induct_tac 1);
-by (Auto_tac());
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
@@ -110,7 +106,7 @@
goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \
\ evs : yahalom lost |] ==> A:lost";
-by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
+by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
qed "Spy_see_shrK_D";
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
@@ -120,11 +116,11 @@
(*Nobody can have used non-existent keys!*)
goal thy "!!evs. evs : yahalom lost ==> \
\ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
-by (parts_induct_tac 1);
+by parts_induct_tac;
(*YM4: Key K is not fresh!*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 3);
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
(*YM3*)
-by (fast_tac (!claset addss (!simpset)) 2);
+by (Blast_tac 2);
(*Fake*)
by (best_tac
(!claset addIs [impOfSubs analz_subset_parts]
@@ -149,12 +145,13 @@
\ ==> K ~: range shrK";
by (etac rev_mp 1);
by (etac yahalom.induct 1);
-by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+by (ALLGOALS Asm_simp_tac);
+by (Blast_tac 1);
qed "Says_Server_message_form";
(*For proofs involving analz. We again instantiate the variable to "lost".*)
-val analz_Fake_tac =
+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
assume_tac 7 THEN REPEAT ((etac exE ORELSE' hyp_subst_tac) 7);
@@ -177,12 +174,12 @@
\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
\ (K : KK | Key K : analz (sees lost Spy evs))";
by (etac yahalom.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
by (REPEAT_FIRST (resolve_tac [allI, impI]));
by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
(*Base*)
-by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
+by (Blast_tac 1);
(*YM4, Fake*)
by (REPEAT (spy_analz_tac 1));
qed_spec_mp "analz_image_freshK";
@@ -207,14 +204,13 @@
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
by (Step_tac 1);
by (ex_strip_tac 2);
-by (Fast_tac 2);
+by (Blast_tac 2);
(*Remaining case: YM3*)
by (expand_case_tac "K = ?y" 1);
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
(*...we assume X is a recent message and handle this case by contradiction*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs
- delrules [conjI] (*prevent split-up into 4 subgoals*)
- addss (!simpset addsimps [parts_insertI])) 1);
+by (blast_tac (!claset addSEs sees_Spy_partsEs
+ delrules [conjI] (*no split-up to 4 subgoals*)) 1);
val lemma = result();
goal thy
@@ -240,7 +236,8 @@
\ Crypt (shrK B) {|Agent A, Key K|}|} \
\ : set_of_list evs";
by (etac rev_mp 1);
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
qed "A_trusts_YM3";
@@ -255,22 +252,19 @@
\ Says A Spy {|NA, NB, Key K|} ~: set_of_list evs --> \
\ Key K ~: analz (sees lost Spy evs)";
by (etac yahalom.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
by (ALLGOALS
(asm_simp_tac
(!simpset addsimps [not_parts_not_analz, analz_insert_freshK]
setloop split_tac [expand_if])));
(*YM3*)
-by (fast_tac (!claset delrules [impCE]
- addSEs sees_Spy_partsEs
- addIs [impOfSubs analz_subset_parts]
- addss (!simpset addsimps [parts_insert2])) 2);
+by (blast_tac (!claset delrules [impCE]
+ addSEs sees_Spy_partsEs
+ addIs [impOfSubs analz_subset_parts]) 2);
(*OR4, Fake*)
by (REPEAT_FIRST spy_analz_tac);
(*Oops*)
-by (fast_tac (!claset delrules [disjE]
- addDs [unique_session_keys]
- addss (!simpset)) 1);
+by (blast_tac (!claset addDs [unique_session_keys]) 1);
val lemma = result() RS mp RS mp RSN(2,rev_notE);
@@ -284,7 +278,7 @@
\ A ~: lost; B ~: lost; evs : yahalom lost |] \
\ ==> Key K ~: analz (sees lost Spy evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
-by (fast_tac (!claset addSEs [lemma]) 1);
+by (blast_tac (!claset addSEs [lemma]) 1);
qed "Spy_not_see_encrypted_key";
@@ -300,7 +294,7 @@
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
-by (REPEAT_FIRST (fast_tac (!claset addIs [yahalom_mono RS subsetD])));
+by (REPEAT_FIRST (blast_tac (!claset addIs [yahalom_mono RS subsetD])));
qed "Agent_not_see_encrypted_key";
@@ -317,9 +311,10 @@
\ Crypt (shrK B) {|Agent A, Key K|}|} \
\ : set_of_list evs";
by (etac rev_mp 1);
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
(*YM3*)
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "B_trusts_YM4_shrK";
@@ -330,19 +325,15 @@
\ EX NA' A' B'. ALL NA A B. \
\ Crypt (shrK B) {|Agent A, Nonce NA, NB|} : parts(sees lost Spy evs) \
\ --> B ~: lost --> NA = NA' & A = A' & B = B'";
-by (etac yahalom.induct 1 THEN parts_Fake_tac);
-(*Fake: the tactic in parts_induct_tac works, but takes 4 times longer*)
-by (REPEAT (etac exE 2) THEN
- best_tac (!claset addSIs [exI]
- addDs [impOfSubs Fake_parts_insert]
- addss (!simpset)) 2);
-(*Base case*)
-by (fast_tac (!claset addss (!simpset)) 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
+by parts_induct_tac;
+(*Fake*)
+by (REPEAT (etac (exI RSN (2,exE)) 1) (*stripping EXs makes proof faster*)
+ THEN Fake_parts_insert_tac 1);
+by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
(*YM2: creation of new Nonce. Move assertion into global context*)
by (expand_case_tac "NB = ?y" 1);
by (REPEAT (resolve_tac [exI, conjI, impI, refl] 1));
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
val lemma = result();
goal thy
@@ -358,7 +349,7 @@
fun lost_tac s =
case_tac ("(" ^ s ^ ") : lost") THEN'
SELECT_GOAL
- (REPEAT_DETERM (dtac (Says_imp_sees_Spy RS analz.Inj) 1) THEN
+ (REPEAT_DETERM (dtac (Says_imp_sees_Spy' RS analz.Inj) 1) THEN
REPEAT_DETERM (etac MPair_analz 1) THEN
THEN_BEST_FIRST
(dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN assume_tac 1)
@@ -376,31 +367,34 @@
\ evs : yahalom lost |] \
\ ==> NA' = NA & A' = A & B' = B";
by (lost_tac "B'" 1);
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
- addSEs [MPair_parts]
- addDs [unique_NB]) 1);
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
+ addSEs [MPair_parts]
+ addDs [unique_NB]) 1);
qed "Says_unique_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))
+*)
+val analz_mono_parts_induct_tac =
+ etac yahalom.induct 1
+ THEN
+ REPEAT_FIRST
+ (rtac impI THEN'
+ dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN'
+ mp_tac)
+ THEN parts_sees_tac;
+
goal thy
"!!evs. [| B ~: lost; evs : yahalom lost |] \
-\ ==> Nonce NB ~: analz (sees lost Spy evs) --> \
-\ Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} : parts (sees lost Spy evs) \
-\ --> Crypt (shrK B') {|Agent A', Nonce NB, NB'|} ~: parts (sees lost Spy evs)";
-by (etac yahalom.induct 1);
-by parts_Fake_tac;
-by (REPEAT_FIRST
- (rtac impI THEN'
- dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN'
- mp_tac));
-by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]
- addss (!simpset)) 2);
-by (ALLGOALS Asm_simp_tac);
-by (fast_tac (!claset addss (!simpset)) 1);
-by (fast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj]
- addSIs [parts_insertI]
- addSEs partsEs
- addss (!simpset)) 1);
+\ ==> Nonce NB ~: analz (sees lost Spy evs) --> \
+\ Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}: parts(sees lost Spy evs)\
+\ --> Crypt (shrK B') {|Agent A', Nonce NB, NB'|} ~: parts(sees lost Spy evs)";
+by analz_mono_parts_induct_tac;
+by (Fake_parts_insert_tac 1);
+by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]
+ addSIs [parts_insertI]
+ addSEs partsEs) 1);
val no_nonce_YM1_YM2 = standard (result() RS mp RSN (2, rev_mp) RS notE);
@@ -419,23 +413,15 @@
\ Nonce NA, Nonce NB|}, \
\ Crypt (shrK B) {|Agent A, Key K|}|} \
\ : set_of_list evs)";
-by (etac yahalom.induct 1);
-by parts_Fake_tac;
-by (fast_tac (!claset addss (!simpset)) 1);
-by (REPEAT_FIRST
- (rtac impI THEN'
- dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD)));
-by (ALLGOALS Asm_simp_tac);
-(*Fake, YM3, YM4*)
-by (Fast_tac 2);
-by (fast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
- addDs [impOfSubs analz_subset_parts]
- addss (!simpset)) 1);
-(*YM4*)
+by analz_mono_parts_induct_tac;
+(*YM4 & Fake*)
+by (Blast_tac 2);
+by (Fake_parts_insert_tac 1);
+(*YM3*)
by (Step_tac 1);
by (lost_tac "A" 1);
-by (fast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS
- A_trusts_YM3]) 1);
+by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS
+ A_trusts_YM3]) 1);
val B_trusts_YM4_newK = result() RS mp RSN (2, rev_mp);
@@ -448,26 +434,19 @@
\ ==> Key K ~: analz (sees lost Spy evs) --> \
\ Crypt K (Nonce NB) : parts (sees lost Spy evs) --> \
\ (EX A B NA. Says Server A \
-\ {|Crypt (shrK A) {|Agent B, Key K, \
-\ Nonce NA, Nonce NB|}, \
+\ {|Crypt (shrK A) {|Agent B, Key K, \
+\ Nonce NA, Nonce NB|}, \
\ Crypt (shrK B) {|Agent A, Key K|}|} \
\ : set_of_list evs)";
-by (etac yahalom.induct 1);
-by parts_Fake_tac;
-by (fast_tac (!claset addss (!simpset)) 1);
-by (TRYALL (rtac impI));
-by (REPEAT_FIRST
- (dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD)));
-by (ALLGOALS Asm_simp_tac);
-(*Fake, YM3, YM4*)
-by (fast_tac (!claset addSDs [Crypt_Fake_parts_insert]
- addDs [impOfSubs analz_subset_parts]) 1);
-by (Fast_tac 1);
-(*YM4*)
+by analz_mono_parts_induct_tac;
+(*YM4 & Fake*)
+by (Blast_tac 2);
+by (Fake_parts_insert_tac 1);
+(*YM3*)
by (Step_tac 1);
by (lost_tac "A" 1);
-by (fast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS
- A_trusts_YM3]) 1);
+by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS
+ A_trusts_YM3]) 1);
result() RS mp RSN (2, rev_mp);
@@ -482,7 +461,7 @@
by (etac rev_mp 1);
by (etac yahalom.induct 1);
by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Blast_tac);
qed "Says_Server_imp_YM2";
@@ -491,9 +470,9 @@
val no_nonce_tac = SELECT_GOAL
(REPEAT (resolve_tac [impI, notI] 1) THEN
REPEAT (hyp_subst_tac 1) THEN
- etac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd RS no_nonce_YM1_YM2) 1
+ etac (Says_imp_sees_Spy' RS parts.Inj RS parts.Snd RS no_nonce_YM1_YM2) 1
THEN
- etac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd) 4
+ etac (Says_imp_sees_Spy' RS parts.Inj RS parts.Snd) 4
THEN
REPEAT_FIRST assume_tac);
@@ -509,30 +488,30 @@
goal thy
"!!evs. P --> (X : analz (G Un H)) --> (X : analz H) ==> \
\ P --> (X : analz (G Un H)) = (X : analz H)";
-by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
+by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
qed "Nonce_secrecy_lemma";
goal thy
- "!!evs. evs : yahalom lost ==> \
+ "!!evs. evs : yahalom lost ==> \
\ (ALL KK. KK <= Compl (range shrK) --> \
-\ (ALL K: KK. ALL A B na X. \
+\ (ALL K: KK. ALL A B na X. \
\ Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \
-\ ~: set_of_list evs) --> \
-\ (Nonce NB : analz (Key``KK Un (sees lost Spy evs))) = \
+\ ~: set_of_list evs) --> \
+\ (Nonce NB : analz (Key``KK Un (sees lost Spy evs))) = \
\ (Nonce NB : analz (sees lost Spy evs)))";
by (etac yahalom.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
by (REPEAT_FIRST (resolve_tac [impI RS allI]));
by (REPEAT_FIRST (rtac Nonce_secrecy_lemma ));
by (rtac ccontr 7);
-by (subgoal_tac "ALL A B na X. \
+by (subgoal_tac "ALL A B na X. \
\ Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \
\ ~: set_of_list evsa" 7);
by (eres_inst_tac [("P","?PP-->?QQ")] notE 7);
-by (subgoal_tac "ALL A B na X. \
-\ Says Server A \
+by (subgoal_tac "ALL A B na X. \
+\ Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB|}, X|} \
\ ~: set_of_list evsa" 5);
by (ALLGOALS (*22 seconds*)
@@ -542,15 +521,14 @@
not_parts_not_analz, analz_image_freshK]
@ pushes @ ball_simps))));
(*Base*)
-by (fast_tac (!claset addss (!simpset)) 1);
+by (Blast_tac 1);
(*Fake*) (** LEVEL 10 **)
by (spy_analz_tac 1);
(*YM3*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
(*Oops*)
-(*20 secs*)
-by (fast_tac (!claset delrules [ballE] addDs [unique_session_keys]
- addss (!simpset)) 2);
+by (Asm_full_simp_tac 2);
+by (blast_tac (!claset addDs [unique_session_keys]) 2);
(*YM4*)
(** LEVEL 13 **)
by (REPEAT (resolve_tac [impI, allI] 1));
@@ -562,10 +540,10 @@
by (step_tac (!claset addSDs [not_analz_insert]) 1);
by (lost_tac "A" 1);
(** LEVEL 20 **)
-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 (thin_tac "All ?PP" 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed_spec_mp "Nonce_secrecy";
@@ -581,8 +559,8 @@
\ KAB ~: range shrK; evs : yahalom lost |] \
\ ==> NB = NB'";
by (rtac ccontr 1);
-by (subgoal_tac "ALL A B na X. \
-\ Says Server A \
+by (subgoal_tac "ALL A B na X. \
+\ Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB|}, X|} \
\ ~: set_of_list evs" 1);
by (eres_inst_tac [("P","Nonce NB : ?HH")] rev_mp 1);
@@ -592,6 +570,8 @@
qed "single_Nonce_secrecy";
+val Says_unique_NB' = read_instantiate [("lost","lost")] Says_unique_NB;
+
goal thy
"!!evs. [| A ~: lost; B ~: lost; Spy: lost; evs : yahalom lost |] \
\ ==> Says B Server \
@@ -600,55 +580,53 @@
\ (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs) --> \
\ Nonce NB ~: analz (sees lost Spy evs)";
by (etac yahalom.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
by (ALLGOALS
(asm_simp_tac
(!simpset addsimps ([not_parts_not_analz,
analz_insert_freshK] @ pushes)
setloop split_tac [expand_if])));
-by (fast_tac (!claset addSIs [parts_insertI]
- addSEs sees_Spy_partsEs
- addss (!simpset)) 2);
+by (blast_tac (!claset addSIs [parts_insertI]
+ addSEs sees_Spy_partsEs) 2);
(*Proof of YM2*) (** LEVEL 4 **)
-by (deepen_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj,
- impOfSubs analz_subset_parts]
- addSEs partsEs) 3 2);
+by (blast_tac (!claset addSEs partsEs
+ addDs [Says_imp_sees_Spy' RS analz.Inj,
+ impOfSubs analz_subset_parts]) 2);
(*Prove YM3 by showing that no NB can also be an NA*)
by (REPEAT (Safe_step_tac 2 ORELSE no_nonce_tac 2));
-by (deepen_tac (!claset addDs [Says_unique_NB]) 1 2);
+by (blast_tac (!claset addDs [Says_unique_NB']) 2 THEN flexflex_tac);
(*Fake*)
by (spy_analz_tac 1);
(*YM4*) (** LEVEL 8 **)
by (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1);
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
-(*43 secs??*)
+(* SLOW: 13s*)
by (SELECT_GOAL (REPEAT_FIRST (spy_analz_tac ORELSE' Safe_step_tac)) 1);
by (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);
-(** LEVEL 15 **)
-by (REPEAT_FIRST ((eresolve_tac [asm_rl, bexE, exE, disjE])));
+by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, exE, disjE]));
+(** LEVEL 16 **)
+(* use unique_NB to identify message components *)
by (lost_tac "Ba" 1);
-by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd RS unique_NB) 1);
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
- addSEs [MPair_parts]) 1);
-by (REPEAT (assume_tac 1 ORELSE Safe_step_tac 1));
+by (subgoal_tac "Aa=A & Ba=B & NAa=NA" 1);
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
+ addSEs [MPair_parts] addDs [unique_NB]) 2);
+by (blast_tac (!claset addDs [Spy_not_see_encrypted_key,
+ impOfSubs Fake_analz_insert]
+ addIs [impOfSubs analz_mono]) 1);
(** LEVEL 20 **)
-by (dtac Spy_not_see_encrypted_key 1);
-by (REPEAT (assume_tac 1 ORELSE Fast_tac 1));
-by (spy_analz_tac 1);
-(*Oops case*) (** LEVEL 23 **)
+(*Oops case*)
by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
by (step_tac (!claset delrules [disjE, conjI]) 1);
by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
by (expand_case_tac "NB = NBa" 1);
-by (deepen_tac (!claset addDs [Says_unique_NB]) 1 1);
+by (blast_tac (!claset addDs [Says_unique_NB']) 1);
by (rtac conjI 1);
by (no_nonce_tac 1);
(** LEVEL 30 **)
-by (thin_tac "?PP|?QQ" 1); (*subsumption!*)
-by (fast_tac (!claset addSDs [single_Nonce_secrecy]) 1);
+by (blast_tac (!claset addSDs [single_Nonce_secrecy]) 1);
val Spy_not_see_NB = result() RSN(2,rev_mp) RSN(2,rev_mp) |> standard;
@@ -671,11 +649,11 @@
\ Crypt (shrK B) {|Agent A, Key K|}|} \
\ : set_of_list 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 (deepen_tac (!claset addDs [Says_unique_NB] addss (!simpset)) 0 1);
+by (blast_tac (!claset addDs [Says_unique_NB']) 1);
qed "B_trusts_YM4";
--- a/src/HOL/Auth/Yahalom2.ML Wed May 07 12:50:26 1997 +0200
+++ b/src/HOL/Auth/Yahalom2.ML Wed May 07 13:01:43 1997 +0200
@@ -17,8 +17,6 @@
proof_timing:=true;
HOL_quantifiers := false;
-val op addss = op unsafe_addss;
-
(*A "possibility property": there are traces that reach the end*)
goal thy
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
@@ -38,7 +36,7 @@
by (rtac subsetI 1);
by (etac yahalom.induct 1);
by (REPEAT_FIRST
- (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
+ (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
:: yahalom.intrs))));
qed "yahalom_mono";
@@ -57,7 +55,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_of_list evs ==> \
\ X : analz (sees lost Spy evs)";
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
+by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "YM4_analz_sees_Spy";
bind_thm ("YM4_parts_sees_Spy",
@@ -67,26 +65,18 @@
goal thy "!!evs. Says S A {|NB, Crypt (shrK A) {|B, K, NA|}, X|} \
\ : set_of_list evs ==> \
\ K : parts (sees lost Spy evs)";
-by (fast_tac (!claset addSEs partsEs
+by (blast_tac (!claset addSEs partsEs
addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
qed "YM4_Key_parts_sees_Spy";
-(*We instantiate the variable to "lost". Leaving it as a Var makes proofs
- harder: the simplifier does less.*)
-val parts_Fake_tac =
- forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6 THEN
- forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7;
-
-(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
-fun parts_induct_tac i = SELECT_GOAL
- (DETERM (etac yahalom.induct 1 THEN parts_Fake_tac THEN
- (*Fake message*)
- TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]
- addss (!simpset)) 2)) THEN
- (*Base case*)
- fast_tac (!claset addss (!simpset)) 1 THEN
- ALLGOALS Asm_simp_tac) i;
+(*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 yahalom.induct 1 THEN
+ 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;
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
@@ -96,8 +86,9 @@
goal thy
"!!evs. evs : yahalom lost \
\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
-by (parts_induct_tac 1);
-by (Auto_tac());
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
@@ -110,7 +101,7 @@
goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \
\ evs : yahalom lost |] ==> A:lost";
-by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
+by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
qed "Spy_see_shrK_D";
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
@@ -120,11 +111,11 @@
(*Nobody can have used non-existent keys!*)
goal thy "!!evs. evs : yahalom lost ==> \
\ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
-by (parts_induct_tac 1);
+by parts_induct_tac;
(*YM4: Key K is not fresh!*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs) 3);
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
(*YM3*)
-by (fast_tac (!claset addss (!simpset)) 2);
+by (blast_tac (!claset addss (!simpset)) 2);
(*Fake*)
by (best_tac
(!claset addIs [impOfSubs analz_subset_parts]
@@ -149,12 +140,12 @@
\ ==> K ~: range shrK & A ~= B";
by (etac rev_mp 1);
by (etac yahalom.induct 1);
-by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+by (ALLGOALS Asm_simp_tac);
qed "Says_Server_message_form";
(*For proofs involving analz. We again instantiate the variable to "lost".*)
-val analz_Fake_tac =
+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
assume_tac 7 THEN
@@ -179,12 +170,12 @@
\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
\ (K : KK | Key K : analz (sees lost Spy evs))";
by (etac yahalom.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
by (REPEAT_FIRST (resolve_tac [allI, impI]));
by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
(*Base*)
-by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
+by (blast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
(*YM4, Fake*)
by (REPEAT (spy_analz_tac 1));
qed_spec_mp "analz_image_freshK";
@@ -212,7 +203,7 @@
by (expand_case_tac "K = ?y" 1);
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
(*...we assume X is a recent message and handle this case by contradiction*)
-by (fast_tac (!claset addSEs sees_Spy_partsEs
+by (blast_tac (!claset addSEs sees_Spy_partsEs
delrules [conjI] (*prevent split-up into 4 subgoals*)
addss (!simpset addsimps [parts_insertI])) 1);
val lemma = result();
@@ -234,30 +225,28 @@
goal thy
"!!evs. [| A ~: lost; B ~: lost; A ~= B; \
-\ evs : yahalom lost |] \
+\ evs : yahalom lost |] \
\ ==> Says Server A \
-\ {|NB, Crypt (shrK A) {|Agent B, Key K, NA|}, \
-\ Crypt (shrK B) {|NB, Key K, Agent A|}|} \
-\ : set_of_list evs --> \
-\ Says A Spy {|NA, NB, Key K|} ~: set_of_list evs --> \
+\ {|NB, Crypt (shrK A) {|Agent B, Key K, NA|}, \
+\ Crypt (shrK B) {|NB, Key K, Agent A|}|} \
+\ : set_of_list evs --> \
+\ Says A Spy {|NA, NB, Key K|} ~: set_of_list evs --> \
\ Key K ~: analz (sees lost Spy evs)";
by (etac yahalom.induct 1);
-by analz_Fake_tac;
+by analz_sees_tac;
by (ALLGOALS
(asm_simp_tac
(!simpset addsimps [not_parts_not_analz, analz_insert_freshK]
setloop split_tac [expand_if])));
(*YM3*)
-by (fast_tac (!claset delrules [impCE]
+by (blast_tac (!claset delrules [impCE]
addSEs sees_Spy_partsEs
addIs [impOfSubs analz_subset_parts]
addss (!simpset addsimps [parts_insert2])) 2);
(*OR4, Fake*)
by (REPEAT_FIRST spy_analz_tac);
(*Oops*)
-by (fast_tac (!claset delrules [disjE]
- addDs [unique_session_keys]
- addss (!simpset)) 1);
+by (blast_tac (!claset addDs [unique_session_keys]) 1);
val lemma = result() RS mp RS mp RSN(2,rev_notE);
@@ -271,7 +260,7 @@
\ A ~: lost; B ~: lost; evs : yahalom lost |] \
\ ==> Key K ~: analz (sees lost Spy evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
-by (fast_tac (!claset addSEs [lemma]) 1);
+by (blast_tac (!claset addSEs [lemma]) 1);
qed "Spy_not_see_encrypted_key";
@@ -287,7 +276,7 @@
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
-by (REPEAT_FIRST (fast_tac (!claset addIs [yahalom_mono RS subsetD])));
+by (REPEAT_FIRST (blast_tac (!claset addIs [yahalom_mono RS subsetD])));
qed "Agent_not_see_encrypted_key";
@@ -303,9 +292,9 @@
\ Crypt (shrK B) {|NB, Key K, Agent A|}|} \
\ : set_of_list evs";
by (etac rev_mp 1);
-by (parts_induct_tac 1);
-(*The nested conjunctions are entirely useless*)
-by (REPEAT_FIRST (rtac conjI ORELSE' fast_tac (!claset delrules [conjI])));
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
qed "A_trusts_YM3";
@@ -321,9 +310,10 @@
\ Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|} \
\ : set_of_list evs";
by (etac rev_mp 1);
-by (parts_induct_tac 1);
+by parts_induct_tac;
+by (Fake_parts_insert_tac 1);
(*YM3*)
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "B_trusts_YM4_shrK";
(*With this variant we don't bother to use the 2nd part of YM4 at all, since
@@ -342,5 +332,5 @@
\ Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|} \
\ : set_of_list evs";
by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1);
-by (fast_tac (!claset addSDs [B_trusts_YM4_shrK]) 1);
+by (blast_tac (!claset addSDs [B_trusts_YM4_shrK]) 1);
qed "B_trusts_YM4";