--- a/src/HOL/Auth/Yahalom.ML Wed Nov 18 15:10:46 1998 +0100
+++ b/src/HOL/Auth/Yahalom.ML Wed Nov 18 16:24:33 1998 +0100
@@ -449,8 +449,7 @@
\ : set evs";
by (etac rev_mp 1);
by (etac yahalom.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS Blast_tac);
+by Auto_tac;
qed "Says_Server_imp_YM2";
@@ -470,8 +469,7 @@
(*Prove YM3 by showing that no NB can also be an NA*)
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj]
addSEs [MPair_parts]
- addDs [no_nonce_YM1_YM2, Says_unique_NB]) 4
- THEN flexflex_tac);
+ addDs [no_nonce_YM1_YM2, Says_unique_NB]) 4);
(*YM2: similar freshness reasoning*)
by (blast_tac (claset() addSEs partsEs
addDs [Says_imp_spies RS analz.Inj,
@@ -482,23 +480,22 @@
(*Fake*)
by (spy_analz_tac 1);
(** LEVEL 7: YM4 and Oops remain **)
-by (ALLGOALS Clarify_tac);
+by (ALLGOALS (Clarify_tac THEN'
+ full_simp_tac (simpset() addsimps [all_conj_distrib])));
(*YM4: key K is visible to Spy, contradicting session key secrecy theorem*)
by (not_bad_tac "Aa" 1);
by (dtac (Says_imp_spies RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
by (forward_tac [Says_Server_imp_YM2] 3);
-by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, exE, disjE]));
-(* use Says_unique_NB to identify message components: Aa=A, Ba=B, NAa=NA *)
-by (blast_tac (claset() addDs [Says_unique_NB, Spy_not_see_encrypted_key,
- impOfSubs Fake_analz_insert]) 1);
+by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
+(* use Says_unique_NB to identify message components: Aa=A, Ba=B*)
+by (blast_tac (claset() addDs [Says_unique_NB, Spy_not_see_encrypted_key]) 1);
(** LEVEL 13 **)
(*Oops case: if the nonce is betrayed now, show that the Oops event is
covered by the quantified Oops assumption.*)
-by (full_simp_tac (simpset() addsimps [all_conj_distrib]) 1);
by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
by (expand_case_tac "NB = NBa" 1);
(*If NB=NBa then all other components of the Oops message agree*)
-by (blast_tac (claset() addDs [Says_unique_NB]) 1 THEN flexflex_tac);
+by (blast_tac (claset() addDs [Says_unique_NB]) 1);
(*case NB ~= NBa*)
by (asm_simp_tac (simpset() addsimps [single_Nonce_secrecy]) 1);
by (Clarify_tac 1);
--- a/src/HOL/Auth/Yahalom2.ML Wed Nov 18 15:10:46 1998 +0100
+++ b/src/HOL/Auth/Yahalom2.ML Wed Nov 18 16:24:33 1998 +0100
@@ -196,8 +196,9 @@
addsimps [analz_insert_eq, analz_insert_freshK])));
(*Oops*)
by (blast_tac (claset() addDs [unique_session_keys]) 3);
-(*YM3*)
-by (blast_tac (claset() delrules [impCE]) 2);
+(*YM3: delete a useless induction hypothesis*)
+by (thin_tac "?P-->?Q" 2);
+by (Blast_tac 2);
(*Fake*)
by (spy_analz_tac 1);
val lemma = result() RS mp RS mp RSN(2,rev_notE);
@@ -350,10 +351,11 @@
(*Fake*)
by (Blast_tac 1);
(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
-by (fast_tac (claset() addSDs [Crypt_imp_keysFor] addss (simpset())) 1);
+by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1);
(*YM4: was Crypt K (Nonce NB) the very last message? If not, use ind. hyp.*)
by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
-(*yes: apply unicity of session keys*)
+(*yes: delete a useless induction hypothesis; apply unicity of session keys*)
+by (thin_tac "?P-->?Q" 1);
by (not_bad_tac "Aa" 1);
by (blast_tac (claset() addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
addDs [unique_session_keys]) 1);