No longer assumes Alice is not the Enemy in NS3.
authorpaulson
Fri Sep 13 13:22:08 1996 +0200 (1996-09-13)
changeset 19976efba890341e
parent 1996 33c42cae3dd0
child 1998 f8230821f1e8
No longer assumes Alice is not the Enemy in NS3.
Proofs do not need it, and the assumption complicated the liveness argument
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/NS_Shared.thy
     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