# HG changeset patch
# User paulson
# Date 842613622 -7200
# Node ID 33c42cae3dd0f532626d67615c5a826d848eeb1c
# Parent  c80e58e78d9c017f50c38e9f1584f8bf0ca2995c
Uses the improved enemy_analz_tac of Shared.ML, with simpler proofs
Weak liveness

diff -r c80e58e78d9c -r 33c42cae3dd0 src/HOL/Auth/OtwayRees.ML
--- a/src/HOL/Auth/OtwayRees.ML	Fri Sep 13 13:16:57 1996 +0200
+++ b/src/HOL/Auth/OtwayRees.ML	Fri Sep 13 13:20:22 1996 +0200
@@ -15,6 +15,22 @@
 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 K. EX evs: otway.          \
+\               Says A B (Crypt (Agent A) K) : set_of_list evs";
+by (REPEAT (resolve_tac [exI,bexI] 1));
+br (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4 RS 
+    otway.OR5) 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 otway ****)
 
 (*The Enemy can see more than anybody else, except for their initial state*)
@@ -45,17 +61,17 @@
 
 (** For reasoning about the encrypted portion of messages **)
 
-goal thy "!!evs. (Says A' B {|N, Agent A, Agent B, X|}) : set_of_list evs ==> \
+goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs ==> \
 \                X : analz (sees Enemy evs)";
 by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
 qed "OR2_analz_sees_Enemy";
 
-goal thy "!!evs. (Says S B {|N, X, X'|}) : set_of_list evs ==> \
+goal thy "!!evs. Says S B {|N, X, X'|} : set_of_list evs ==> \
 \                X : analz (sees Enemy evs)";
 by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
 qed "OR4_analz_sees_Enemy";
 
-goal thy "!!evs. (Says B' A {|N, Crypt {|N,K|} K'|}) : set_of_list evs ==> \
+goal thy "!!evs. Says B' A {|N, Crypt {|N,K|} K'|} : set_of_list evs ==> \
 \                K : parts (sees Enemy evs)";
 by (fast_tac (!claset addSEs partsEs
 	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
@@ -165,18 +181,16 @@
 by (EVERY 
     (map
      (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)))
      [3,2,1]));
 (*OR5: dummy message*)
-by (best_tac (!claset addSDs [newK_invKey]
-		        addEs  [new_keys_not_seen RSN(2,rev_notE)]
-			addIs  [less_SucI, impOfSubs keysFor_mono]
-			addss (!simpset addsimps [le_def])) 1);
+by (best_tac (!claset addEs  [new_keys_not_seen RSN(2,rev_notE)]
+		      addIs  [less_SucI, impOfSubs keysFor_mono]
+		      addss (!simpset addsimps [le_def])) 1);
 val lemma = result();
 
 goal thy 
@@ -259,19 +273,6 @@
 
 (** Session keys are not used to encrypt other session keys **)
 
-(*Could generalize this so that the X component doesn't have to be first
-  in the message?*)
-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)
-	   ]);
-
-
 (*Lemma for the trivial direction of the if-and-only-if*)
 goal thy  
  "!!evs. (Key K : analz (Key``nE Un sEe)) --> \
@@ -294,22 +295,11 @@
      (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
 			 @ pushes)
                setloop split_tac [expand_if])));
-(*OR4*) 
-by (enemy_analz_tac 5);
+(*OR4, OR2, Fake*) 
+by (EVERY (map enemy_analz_tac [5,3,2]));
 (*OR3*)
-by (Fast_tac 4);
-(*OR2*) (** LEVEL 7 **)
-by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")] 
-    (insert_commute RS ssubst) 3);
-by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
-    (insert_commute RS ssubst) 3);
-by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 3);
-by (enemy_analz_tac 3);
-(*Fake case*) (** LEVEL 11 **)
-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 2);
+(*Base case*) 
 by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
 qed_spec_mp "analz_image_newK";
 
@@ -360,20 +350,10 @@
      (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
 			  analz_insert_Key_newK] @ pushes)
                setloop split_tac [expand_if])));
+(*OR4, OR2, Fake*) 
+by (EVERY (map enemy_analz_tac [4,2,1]));
 (*OR3*)
-by (fast_tac (!claset addSEs [less_irrefl]) 3);
-(*Fake*) (** LEVEL 10 **)
-by (res_inst_tac [("y1","X"), ("x1", "Key ?K")] (insert_commute RS ssubst) 1);
-by (enemy_analz_tac 1);
-(*OR4*)
-by (mp_tac 2);
-by (enemy_analz_tac 2);
-(*OR2*)
-by (mp_tac 1);
-by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
-    (insert_commute RS ssubst) 1);
-by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
-by (enemy_analz_tac 1);
+by (fast_tac (!claset addSEs [less_irrefl]) 1);
 qed "Enemy_not_see_encrypted_key";
 
 
@@ -432,9 +412,9 @@
 		      addEs [Says_imp_old_keys RS less_irrefl]
 	              addss (!simpset)) 3);
 (*OR2*) (** LEVEL 12 **)
+(*enemy_analz_tac just does not work here: it is an entirely different proof!*)
 by (ex_strip_tac 2);
-by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
-    (insert_commute RS ssubst) 2);
+by (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 2);
 by (Simp_tac 2);
 by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
 			      Crypt_parts_singleton]) 2);