src/HOL/Auth/Yahalom.ML
changeset 5932 737559a43e71
parent 5535 678999604ee9
child 6335 7e4bffaa2a3e
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Wed Nov 18 15:10:46 1998 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Wed Nov 18 16:24:33 1998 +0100
     1.3 @@ -449,8 +449,7 @@
     1.4  \                : set evs";
     1.5  by (etac rev_mp 1);
     1.6  by (etac yahalom.induct 1);
     1.7 -by (ALLGOALS Asm_simp_tac);
     1.8 -by (ALLGOALS Blast_tac);
     1.9 +by Auto_tac;
    1.10  qed "Says_Server_imp_YM2";
    1.11  
    1.12  
    1.13 @@ -470,8 +469,7 @@
    1.14  (*Prove YM3 by showing that no NB can also be an NA*)
    1.15  by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj]
    1.16  	                addSEs [MPair_parts]
    1.17 -		        addDs  [no_nonce_YM1_YM2, Says_unique_NB]) 4
    1.18 -    THEN flexflex_tac);
    1.19 +		        addDs  [no_nonce_YM1_YM2, Says_unique_NB]) 4);
    1.20  (*YM2: similar freshness reasoning*) 
    1.21  by (blast_tac (claset() addSEs partsEs
    1.22  		        addDs  [Says_imp_spies RS analz.Inj,
    1.23 @@ -482,23 +480,22 @@
    1.24  (*Fake*)
    1.25  by (spy_analz_tac 1);
    1.26  (** LEVEL 7: YM4 and Oops remain **)
    1.27 -by (ALLGOALS Clarify_tac);
    1.28 +by (ALLGOALS (Clarify_tac THEN' 
    1.29 +	      full_simp_tac (simpset() addsimps [all_conj_distrib])));
    1.30  (*YM4: key K is visible to Spy, contradicting session key secrecy theorem*) 
    1.31  by (not_bad_tac "Aa" 1);
    1.32  by (dtac (Says_imp_spies RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
    1.33  by (forward_tac [Says_Server_imp_YM2] 3);
    1.34 -by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, exE, disjE]));
    1.35 -(*  use Says_unique_NB to identify message components: Aa=A, Ba=B, NAa=NA *)
    1.36 -by (blast_tac (claset() addDs [Says_unique_NB, Spy_not_see_encrypted_key,
    1.37 -			       impOfSubs Fake_analz_insert]) 1);
    1.38 +by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
    1.39 +(*  use Says_unique_NB to identify message components: Aa=A, Ba=B*)
    1.40 +by (blast_tac (claset() addDs [Says_unique_NB, Spy_not_see_encrypted_key]) 1);
    1.41  (** LEVEL 13 **)
    1.42  (*Oops case: if the nonce is betrayed now, show that the Oops event is 
    1.43    covered by the quantified Oops assumption.*)
    1.44 -by (full_simp_tac (simpset() addsimps [all_conj_distrib]) 1);
    1.45  by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
    1.46  by (expand_case_tac "NB = NBa" 1);
    1.47  (*If NB=NBa then all other components of the Oops message agree*)
    1.48 -by (blast_tac (claset() addDs [Says_unique_NB]) 1 THEN flexflex_tac);
    1.49 +by (blast_tac (claset() addDs [Says_unique_NB]) 1);
    1.50  (*case NB ~= NBa*)
    1.51  by (asm_simp_tac (simpset() addsimps [single_Nonce_secrecy]) 1);
    1.52  by (Clarify_tac 1);