1.1 --- a/src/HOL/Auth/NS_Shared.ML	Fri Sep 13 13:20:22 1996 +0200
     1.2 +++ b/src/HOL/Auth/NS_Shared.ML	Fri Sep 13 13:22:08 1996 +0200
     1.3 @@ -13,6 +13,20 @@
     1.4  open NS_Shared;
     1.5  
     1.6  proof_timing:=true;
     1.7 +HOL_quantifiers := false;
     1.8 +
     1.9 +(** Weak liveness: there are traces that reach the end **)
    1.10 +
    1.11 +goal thy 
    1.12 + "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    1.13 +\        ==> EX N K. EX evs: ns_shared.          \
    1.14 +\               Says A B (Crypt {|Nonce N, Nonce N|} K) : set_of_list evs";
    1.15 +by (REPEAT (resolve_tac [exI,bexI] 1));
    1.16 +br (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2;
    1.17 +by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    1.18 +by (REPEAT_FIRST (resolve_tac [refl, conjI]));
    1.19 +by (ALLGOALS (fast_tac (!claset addss (!simpset setsolver safe_solver))));
    1.20 +qed "weak_liveness";
    1.21  
    1.22  (**** Inductive proofs about ns_shared ****)
    1.23  
    1.24 @@ -152,15 +166,14 @@
    1.25  map (by o fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [3,2];
    1.26  (*Fake and NS3*)
    1.27  map (by o best_tac
    1.28 -     (!claset addSDs [newK_invKey]
    1.29 -	      addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
    1.30 +     (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
    1.31  		     impOfSubs (parts_insert_subset_Un RS keysFor_mono),
    1.32  		     Suc_leD]
    1.33  	      addEs [new_keys_not_seen RS not_parts_not_analz RSN (2,rev_notE)]
    1.34  	      addss (!simpset)))
    1.35      [2,1];
    1.36  (*NS4 and NS5: nonce exchange*)
    1.37 -by (ALLGOALS (deepen_tac (!claset addSDs [newK_invKey, Says_imp_old_keys]
    1.38 +by (ALLGOALS (deepen_tac (!claset addSDs [Says_imp_old_keys]
    1.39  	                          addIs  [less_SucI, impOfSubs keysFor_mono]
    1.40  		                  addss (!simpset addsimps [le_def])) 0));
    1.41  val lemma = result();
    1.42 @@ -311,17 +324,6 @@
    1.43  by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
    1.44  val lemma = result();
    1.45  
    1.46 -(*Copied from OtwayRees.ML*)
    1.47 -val enemy_analz_tac =
    1.48 -  SELECT_GOAL 
    1.49 -   (EVERY [REPEAT (resolve_tac [impI,notI] 1),
    1.50 -	   dtac (impOfSubs Fake_analz_insert) 1,
    1.51 -	   eresolve_tac [asm_rl, synth.Inj] 1,
    1.52 -	   Fast_tac 1,
    1.53 -	   Asm_full_simp_tac 1,
    1.54 -	   IF_UNSOLVED (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1)
    1.55 -	   ]);
    1.56 -
    1.57  goal thy  
    1.58   "!!evs. evs : ns_shared ==> \
    1.59  \  ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \
    1.60 @@ -341,8 +343,6 @@
    1.61  (*Cases NS2 and NS3!!  Simple, thanks to auto case splits*)
    1.62  by (REPEAT (Fast_tac 3));
    1.63  (*Fake case*) (** LEVEL 7 **)
    1.64 -by (res_inst_tac [("y1","X"), ("A1", "?G Un (?H::msg set)")] 
    1.65 -    (insert_commute RS ssubst) 2);
    1.66  by (enemy_analz_tac 2);
    1.67  (*Base case*)
    1.68  by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
    1.69 @@ -469,7 +469,7 @@
    1.70      (!simpset addsimps (mem_if::analz_insert_Key_newK::pushes)) 1);
    1.71  by (Step_tac 1);
    1.72  (**LEVEL 15 **)
    1.73 -by (excluded_middle_tac "Friend i : bad" 1);
    1.74 +by (excluded_middle_tac "Aa : bad" 1);
    1.75  (*But this contradicts Key (newK evta) ~: analz (sees Enemy evsa) *)
    1.76  bd (Says_imp_sees_Enemy RS analz.Inj) 2;
    1.77  bd analz.Decrypt 2;
    1.78 @@ -480,4 +480,3 @@
    1.79  by (REPEAT_FIRST assume_tac);
    1.80  by (Auto_tac ());
    1.81  qed "Enemy_not_see_encrypted_key";
    1.82 -

     2.1 --- a/src/HOL/Auth/NS_Shared.thy	Fri Sep 13 13:20:22 1996 +0200
     2.2 +++ b/src/HOL/Auth/NS_Shared.thy	Fri Sep 13 13:22:08 1996 +0200
     2.3 @@ -41,12 +41,10 @@
     2.4                     (shrK A)) # evs : ns_shared"
     2.5  
     2.6            (*We can't assume S=Server.  Agent A "remembers" her nonce.
     2.7 -            May assume WLOG that she is NOT the Enemy: the Fake rule
     2.8 -            covers this case.  Can inductively show A ~= Server*)
     2.9 +            Can inductively show A ~= Server*)
    2.10      NS3  "[| evs: ns_shared;  A ~= B;
    2.11               Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) 
    2.12                 : set_of_list evs;
    2.13 -             A = Friend i;
    2.14               Says A Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
    2.15            ==> Says A B X # evs : ns_shared"
    2.16