src/HOL/Auth/WooLam.ML
changeset 2516 4d68fbe6378b
parent 2451 ce85a2aafc7a
child 2637 e9b203f854ae
     1.1 --- a/src/HOL/Auth/WooLam.ML	Fri Jan 17 11:50:09 1997 +0100
     1.2 +++ b/src/HOL/Auth/WooLam.ML	Fri Jan 17 12:49:31 1997 +0100
     1.3 @@ -25,10 +25,11 @@
     1.4  \                 : set_of_list evs";
     1.5  by (REPEAT (resolve_tac [exI,bexI] 1));
     1.6  by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS 
     1.7 -	  woolam.WL4 RS woolam.WL5) 2);
     1.8 +          woolam.WL4 RS woolam.WL5) 2);
     1.9  by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    1.10  by (REPEAT_FIRST (resolve_tac [refl, conjI]));
    1.11 -by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver))));
    1.12 +by (REPEAT_FIRST (fast_tac (!claset addSEs [Nonce_supply RS notE]
    1.13 +                                    addss (!simpset setsolver safe_solver))));
    1.14  result();
    1.15  
    1.16  
    1.17 @@ -94,23 +95,6 @@
    1.18  AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
    1.19  
    1.20  
    1.21 -(*** Future nonces can't be seen or used! ***)
    1.22 -
    1.23 -goal thy "!!i. evs : woolam ==>             \
    1.24 -\             length evs <= i --> Nonce(newN(i)) ~: parts (sees lost Spy evs)";
    1.25 -by (parts_induct_tac 1);
    1.26 -by (REPEAT_FIRST (fast_tac (!claset 
    1.27 -                              addSEs partsEs
    1.28 -                              addSDs  [Says_imp_sees_Spy RS parts.Inj]
    1.29 -                              addEs [leD RS notE]
    1.30 -			      addDs  [impOfSubs analz_subset_parts,
    1.31 -                                      impOfSubs parts_insert_subset_Un,
    1.32 -                                      Suc_leD]
    1.33 -                              addss (!simpset))));
    1.34 -qed_spec_mp "new_nonces_not_seen";
    1.35 -Addsimps [new_nonces_not_seen];
    1.36 -
    1.37 -
    1.38  (**** Autheticity properties for Woo-Lam ****)
    1.39  
    1.40  
    1.41 @@ -201,6 +185,5 @@
    1.42  \        --> Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
    1.43  by (parts_induct_tac 1);
    1.44  by (Step_tac 1);
    1.45 -by (best_tac (!claset addSEs partsEs
    1.46 -                      addEs  [new_nonces_not_seen RSN(2,rev_notE)]) 1);
    1.47 +by (best_tac (!claset addSEs partsEs) 1);
    1.48  **)