# HG changeset patch
# User paulson
# Date 842613728 -7200
# Node ID 6efba890341e231563065fbf838bd90723fbbefc
# Parent  33c42cae3dd0f532626d67615c5a826d848eeb1c
No longer assumes Alice is not the Enemy in NS3.
Proofs do not need it, and the assumption complicated the liveness argument

diff -r 33c42cae3dd0 -r 6efba890341e src/HOL/Auth/NS_Shared.ML
--- a/src/HOL/Auth/NS_Shared.ML	Fri Sep 13 13:20:22 1996 +0200
+++ b/src/HOL/Auth/NS_Shared.ML	Fri Sep 13 13:22:08 1996 +0200
@@ -13,6 +13,20 @@
 open NS_Shared;
 
 proof_timing:=true;
+HOL_quantifiers := false;
+
+(** Weak liveness: there are traces that reach the end **)
+
+goal thy 
+ "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
+\        ==> EX N K. EX evs: ns_shared.          \
+\               Says A B (Crypt {|Nonce N, Nonce N|} K) : set_of_list evs";
+by (REPEAT (resolve_tac [exI,bexI] 1));
+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;
+by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
+by (REPEAT_FIRST (resolve_tac [refl, conjI]));
+by (ALLGOALS (fast_tac (!claset addss (!simpset setsolver safe_solver))));
+qed "weak_liveness";
 
 (**** Inductive proofs about ns_shared ****)
 
@@ -152,15 +166,14 @@
 map (by o fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [3,2];
 (*Fake and NS3*)
 map (by o best_tac
-     (!claset addSDs [newK_invKey]
-	      addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
+     (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
 		     impOfSubs (parts_insert_subset_Un RS keysFor_mono),
 		     Suc_leD]
 	      addEs [new_keys_not_seen RS not_parts_not_analz RSN (2,rev_notE)]
 	      addss (!simpset)))
     [2,1];
 (*NS4 and NS5: nonce exchange*)
-by (ALLGOALS (deepen_tac (!claset addSDs [newK_invKey, Says_imp_old_keys]
+by (ALLGOALS (deepen_tac (!claset addSDs [Says_imp_old_keys]
 	                          addIs  [less_SucI, impOfSubs keysFor_mono]
 		                  addss (!simpset addsimps [le_def])) 0));
 val lemma = result();
@@ -311,17 +324,6 @@
 by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
 val lemma = result();
 
-(*Copied from OtwayRees.ML*)
-val enemy_analz_tac =
-  SELECT_GOAL 
-   (EVERY [REPEAT (resolve_tac [impI,notI] 1),
-	   dtac (impOfSubs Fake_analz_insert) 1,
-	   eresolve_tac [asm_rl, synth.Inj] 1,
-	   Fast_tac 1,
-	   Asm_full_simp_tac 1,
-	   IF_UNSOLVED (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1)
-	   ]);
-
 goal thy  
  "!!evs. evs : ns_shared ==> \
 \  ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \
@@ -341,8 +343,6 @@
 (*Cases NS2 and NS3!!  Simple, thanks to auto case splits*)
 by (REPEAT (Fast_tac 3));
 (*Fake case*) (** LEVEL 7 **)
-by (res_inst_tac [("y1","X"), ("A1", "?G Un (?H::msg set)")] 
-    (insert_commute RS ssubst) 2);
 by (enemy_analz_tac 2);
 (*Base case*)
 by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
@@ -469,7 +469,7 @@
     (!simpset addsimps (mem_if::analz_insert_Key_newK::pushes)) 1);
 by (Step_tac 1);
 (**LEVEL 15 **)
-by (excluded_middle_tac "Friend i : bad" 1);
+by (excluded_middle_tac "Aa : bad" 1);
 (*But this contradicts Key (newK evta) ~: analz (sees Enemy evsa) *)
 bd (Says_imp_sees_Enemy RS analz.Inj) 2;
 bd analz.Decrypt 2;
@@ -480,4 +480,3 @@
 by (REPEAT_FIRST assume_tac);
 by (Auto_tac ());
 qed "Enemy_not_see_encrypted_key";
-
diff -r 33c42cae3dd0 -r 6efba890341e src/HOL/Auth/NS_Shared.thy
--- a/src/HOL/Auth/NS_Shared.thy	Fri Sep 13 13:20:22 1996 +0200
+++ b/src/HOL/Auth/NS_Shared.thy	Fri Sep 13 13:22:08 1996 +0200
@@ -41,12 +41,10 @@
                    (shrK A)) # evs : ns_shared"
 
           (*We can't assume S=Server.  Agent A "remembers" her nonce.
-            May assume WLOG that she is NOT the Enemy: the Fake rule
-            covers this case.  Can inductively show A ~= Server*)
+            Can inductively show A ~= Server*)
     NS3  "[| evs: ns_shared;  A ~= B;
              Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) 
                : set_of_list evs;
-             A = Friend i;
              Says A Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
           ==> Says A B X # evs : ns_shared"