src/HOL/Auth/Yahalom.ML
changeset 3708 56facaebf3e3
parent 3683 aafe719dff14
child 3919 c036caebfc75
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Thu Sep 25 12:10:07 1997 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Thu Sep 25 12:13:18 1997 +0200
     1.3 @@ -190,7 +190,7 @@
     1.4  \          : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
     1.5  by (etac yahalom.induct 1);
     1.6  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
     1.7 -by (Step_tac 1);
     1.8 +by (ALLGOALS Clarify_tac);
     1.9  by (ex_strip_tac 2);
    1.10  by (Blast_tac 2);
    1.11  (*Remaining case: YM3*)
    1.12 @@ -198,7 +198,7 @@
    1.13  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
    1.14  (*...we assume X is a recent message and handle this case by contradiction*)
    1.15  by (blast_tac (!claset addSEs spies_partsEs
    1.16 -                      delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
    1.17 +                       delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
    1.18  val lemma = result();
    1.19  
    1.20  goal thy 
    1.21 @@ -301,11 +301,11 @@
    1.22  \                          Crypt (shrK B) {|Agent A, Key K|}|}     \
    1.23  \                       : set evs)";
    1.24  by (parts_induct_tac 1);
    1.25 +by (ALLGOALS Clarify_tac);
    1.26  (*YM3 & Fake*)
    1.27  by (Blast_tac 2);
    1.28  by (Fake_parts_insert_tac 1);
    1.29  (*YM4*)
    1.30 -by (Step_tac 1);
    1.31  (*A is uncompromised because NB is secure*)
    1.32  by (not_bad_tac "A" 1);
    1.33  (*A's certificate guarantees the existence of the Server message*)
    1.34 @@ -515,8 +515,8 @@
    1.35  (*Fake*)
    1.36  by (spy_analz_tac 1);
    1.37  (** LEVEL 7: YM4 and Oops remain **)
    1.38 +by (ALLGOALS Clarify_tac);
    1.39  (*YM4: key K is visible to Spy, contradicting session key secrecy theorem*) 
    1.40 -by (REPEAT (Safe_step_tac 1));
    1.41  by (not_bad_tac "Aa" 1);
    1.42  by (dtac (Says_imp_spies RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
    1.43  by (forward_tac [Says_Server_message_form] 3);
    1.44 @@ -529,7 +529,6 @@
    1.45  (*Oops case: if the nonce is betrayed now, show that the Oops event is 
    1.46    covered by the quantified Oops assumption.*)
    1.47  by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
    1.48 -by (step_tac (!claset delrules [disjE, conjI]) 1);
    1.49  by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
    1.50  by (expand_case_tac "NB = NBa" 1);
    1.51  (*If NB=NBa then all other components of the Oops message agree*)