--- a/src/HOL/Auth/NS_Shared.ML Fri Jan 02 13:24:53 1998 +0100
+++ b/src/HOL/Auth/NS_Shared.ML Fri Jan 02 17:15:19 1998 +0100
@@ -97,11 +97,7 @@
\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
by (parts_induct_tac 1);
(*Fake*)
-by (best_tac
- (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
- addIs [impOfSubs analz_subset_parts]
- addDs [impOfSubs (analz_subset_parts RS keysFor_mono)]
- addss (simpset())) 1);
+by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
(*NS2, NS4, NS5*)
by (ALLGOALS (Blast_tac));
qed_spec_mp "new_keys_not_used";
@@ -271,7 +267,7 @@
(simpset() addsimps ([analz_insert_eq, analz_insert_freshK] @
pushes @ expand_ifs))));
(*Oops*)
-by (blast_tac (claset() addDs [unique_session_keys]) 5);
+by (blast_tac (claset() addSDs [unique_session_keys]) 5);
(*NS3, replay sub-case*)
by (Blast_tac 4);
(*NS2*)
--- a/src/HOL/Auth/OtwayRees.ML Fri Jan 02 13:24:53 1998 +0100
+++ b/src/HOL/Auth/OtwayRees.ML Fri Jan 02 17:15:19 1998 +0100
@@ -110,11 +110,7 @@
\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
by (parts_induct_tac 1);
(*Fake*)
-by (best_tac
- (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
- addIs [impOfSubs analz_subset_parts]
- addDs [impOfSubs (analz_subset_parts RS keysFor_mono)]
- addss (simpset())) 1);
+by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
by (ALLGOALS Blast_tac);
qed_spec_mp "new_keys_not_used";
@@ -202,7 +198,7 @@
by (expand_case_tac "K = ?y" 1);
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
(*...we assume X is a recent message, and handle this case by contradiction*)
-by (Blast_tac 1);
+by (blast_tac (claset() addSEs spies_partsEs) 1);
val lemma = result();
goal thy
@@ -329,8 +325,8 @@
by analz_spies_tac;
by (ALLGOALS
(asm_simp_tac (simpset() addcongs [conj_cong]
- addsimps [analz_insert_eq, analz_insert_freshK]
- addsimps (pushes@expand_ifs))));
+ addsimps [analz_insert_eq, analz_insert_freshK]
+ addsimps (pushes@expand_ifs))));
(*Oops*)
by (blast_tac (claset() addSDs [unique_session_keys]) 4);
(*OR4*)
--- a/src/HOL/Auth/OtwayRees_AN.ML Fri Jan 02 13:24:53 1998 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML Fri Jan 02 17:15:19 1998 +0100
@@ -99,11 +99,7 @@
\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
by (parts_induct_tac 1);
(*Fake*)
-by (best_tac
- (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
- addIs [impOfSubs analz_subset_parts]
- addDs [impOfSubs (analz_subset_parts RS keysFor_mono)]
- addss (simpset())) 1);
+by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
(*OR3*)
by (Blast_tac 1);
qed_spec_mp "new_keys_not_used";
@@ -195,7 +191,7 @@
by (expand_case_tac "K = ?y" 1);
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
(*...we assume X is a recent message and handle this case by contradiction*)
-by (Blast_tac 1);
+by (blast_tac (claset() addSEs spies_partsEs) 1);
val lemma = result();
@@ -263,8 +259,8 @@
by analz_spies_tac;
by (ALLGOALS
(asm_simp_tac (simpset() addcongs [conj_cong, if_weak_cong]
- addsimps [analz_insert_eq, analz_insert_freshK]
- addsimps (pushes@expand_ifs))));
+ addsimps [analz_insert_eq, analz_insert_freshK]
+ addsimps (pushes@expand_ifs))));
(*Oops*)
by (blast_tac (claset() addSDs [unique_session_keys]) 4);
(*OR4*)
--- a/src/HOL/Auth/OtwayRees_Bad.ML Fri Jan 02 13:24:53 1998 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Fri Jan 02 17:15:19 1998 +0100
@@ -107,11 +107,7 @@
\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
by (parts_induct_tac 1);
(*Fake*)
-by (best_tac
- (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
- addIs [impOfSubs analz_subset_parts]
- addDs [impOfSubs (analz_subset_parts RS keysFor_mono)]
- addss (simpset())) 1);
+by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
(*OR1-3*)
by (ALLGOALS Blast_tac);
qed_spec_mp "new_keys_not_used";
--- a/src/HOL/Auth/Recur.ML Fri Jan 02 13:24:53 1998 +0100
+++ b/src/HOL/Auth/Recur.ML Fri Jan 02 17:15:19 1998 +0100
@@ -170,9 +170,10 @@
(** Nobody can have used non-existent keys! **)
+(*The special case of H={} has the same proof*)
goal thy
- "!!evs. [| K : keysFor (parts {RB}); (PB,RB,K') : respond evs |] \
-\ ==> K : range shrK";
+ "!!evs. [| K : keysFor (parts (insert RB H)); (PB,RB,K') : respond evs |] \
+\ ==> K : range shrK | K : keysFor (parts H)";
by (etac rev_mp 1);
by (etac (respond_imp_responses RS responses.induct) 1);
by Auto_tac;
@@ -183,14 +184,9 @@
\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
by (parts_induct_tac 1);
(*RA3*)
-by (best_tac (claset() addDs [Key_in_keysFor_parts]
- addss (simpset() addsimps [parts_insert_spies])) 2);
+by (blast_tac (claset() addSDs [Key_in_keysFor_parts]) 2);
(*Fake*)
-by (best_tac
- (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
- addIs [impOfSubs analz_subset_parts]
- addDs [impOfSubs (analz_subset_parts RS keysFor_mono)]
- addss (simpset())) 1);
+by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
qed_spec_mp "new_keys_not_used";
--- a/src/HOL/Auth/Shared.ML Fri Jan 02 13:24:53 1998 +0100
+++ b/src/HOL/Auth/Shared.ML Fri Jan 02 17:15:19 1998 +0100
@@ -28,6 +28,16 @@
qed "keysFor_parts_initState";
Addsimps [keysFor_parts_initState];
+(*Specialized to shared-key model: no need for addss in protocol proofs*)
+goal thy "!!X. [| K: keysFor (parts (insert X H)); X : synth (analz H) |] \
+\ ==> K : keysFor (parts H) | Key K : parts H";
+by (fast_tac
+ (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono),
+ impOfSubs (analz_subset_parts RS keysFor_mono)]
+ addIs [impOfSubs analz_subset_parts]
+ addss (simpset())) 1);
+qed "keysFor_parts_insert";
+
goal thy "!!H. Crypt K X : H ==> K : keysFor H";
by (dtac Crypt_imp_invKey_keysFor 1);
by (Asm_full_simp_tac 1);
--- a/src/HOL/Auth/Yahalom.ML Fri Jan 02 13:24:53 1998 +0100
+++ b/src/HOL/Auth/Yahalom.ML Fri Jan 02 17:15:19 1998 +0100
@@ -101,11 +101,7 @@
\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
by (parts_induct_tac 1);
(*Fake*)
-by (best_tac
- (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
- addIs [impOfSubs analz_subset_parts]
- addDs [impOfSubs (analz_subset_parts RS keysFor_mono)]
- addss (simpset())) 1);
+by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
(*YM2-4: Because Key K is not fresh, etc.*)
by (REPEAT (blast_tac (claset() addSEs spies_partsEs) 1));
qed_spec_mp "new_keys_not_used";
@@ -587,7 +583,7 @@
by (ALLGOALS Asm_simp_tac);
(*YM4*)
by (Blast_tac 2);
-(*YM3*)
+(*YM3 [blast_tac is 50% slower] *)
by (best_tac (claset() addSDs [B_Said_YM2, Says_imp_spies RS parts.Inj]
addSEs [MPair_parts]) 1);
val lemma = result() RSN (2, rev_mp) RS mp |> standard;
--- a/src/HOL/Auth/Yahalom2.ML Fri Jan 02 13:24:53 1998 +0100
+++ b/src/HOL/Auth/Yahalom2.ML Fri Jan 02 17:15:19 1998 +0100
@@ -105,11 +105,7 @@
(*YM3*)
by (blast_tac (claset() addss (simpset())) 2);
(*Fake*)
-by (best_tac
- (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
- addIs [impOfSubs analz_subset_parts]
- addDs [impOfSubs (analz_subset_parts RS keysFor_mono)]
- addss (simpset())) 1);
+by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
qed_spec_mp "new_keys_not_used";
bind_thm ("new_keys_not_analzd",