tidied
authorpaulson
Wed Nov 18 16:24:33 1998 +0100 (1998-11-18)
changeset 5932737559a43e71
parent 5931 325300576da7
child 5933 7b0f502a25b1
tidied
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom2.ML
     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);
     2.1 --- a/src/HOL/Auth/Yahalom2.ML	Wed Nov 18 15:10:46 1998 +0100
     2.2 +++ b/src/HOL/Auth/Yahalom2.ML	Wed Nov 18 16:24:33 1998 +0100
     2.3 @@ -196,8 +196,9 @@
     2.4  	        addsimps [analz_insert_eq, analz_insert_freshK])));
     2.5  (*Oops*)
     2.6  by (blast_tac (claset() addDs [unique_session_keys]) 3);
     2.7 -(*YM3*)
     2.8 -by (blast_tac (claset() delrules [impCE]) 2);
     2.9 +(*YM3: delete a useless induction hypothesis*)
    2.10 +by (thin_tac "?P-->?Q" 2);
    2.11 +by (Blast_tac 2);
    2.12  (*Fake*) 
    2.13  by (spy_analz_tac 1);
    2.14  val lemma = result() RS mp RS mp RSN(2,rev_notE);
    2.15 @@ -350,10 +351,11 @@
    2.16  (*Fake*)
    2.17  by (Blast_tac 1);
    2.18  (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
    2.19 -by (fast_tac (claset() addSDs [Crypt_imp_keysFor] addss (simpset())) 1); 
    2.20 +by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); 
    2.21  (*YM4: was Crypt K (Nonce NB) the very last message?  If not, use ind. hyp.*)
    2.22  by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
    2.23 -(*yes: apply unicity of session keys*)
    2.24 +(*yes: delete a useless induction hypothesis; apply unicity of session keys*)
    2.25 +by (thin_tac "?P-->?Q" 1);
    2.26  by (not_bad_tac "Aa" 1);
    2.27  by (blast_tac (claset() addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
    2.28  			addDs  [unique_session_keys]) 1);