# HG changeset patch
# User paulson
# Date 844074622 -7200
# Node ID ae1030e667451639175a952a3dd5f883aeceaf94
# Parent  e8d52d05530a2d911970dcc9d4add669cb1782a3
Removed some dead wood.  Transferred lemmas used to prove analz_image_newK
to Shared.ML

diff -r e8d52d05530a -r ae1030e66745 src/HOL/Auth/NS_Shared.ML
--- a/src/HOL/Auth/NS_Shared.ML	Mon Sep 30 11:04:14 1996 +0200
+++ b/src/HOL/Auth/NS_Shared.ML	Mon Sep 30 11:10:22 1996 +0200
@@ -297,35 +297,8 @@
 result();
 
 
-(** Specialized rewriting for this proof **)
-
-Delsimps [image_insert];
-Addsimps [image_insert RS sym];
-
-Delsimps [image_Un];
-Addsimps [image_Un RS sym];
-
-goal thy "insert (Key (newK x)) (sees lost A evs) = \
-\         Key `` (newK``{x}) Un (sees lost A evs)";
-by (Fast_tac 1);
-val insert_Key_singleton = result();
-
-goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
-\         Key `` (f `` (insert x E)) Un C";
-by (Fast_tac 1);
-val insert_Key_image = result();
-
-
 (** Session keys are not used to encrypt other session keys **)
 
-(*Lemma for the trivial direction of the if-and-only-if*)
-goal thy  
- "!!evs. (Key K : analz (Key``nE Un sEe)) --> \
-\         (K : nE | Key K : analz sEe)  ==>     \
-\        (Key K : analz (Key``nE Un sEe)) = (K : nE | Key K : analz sEe)";
-by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
-val lemma = result();
-
 (*The equality makes the induction hypothesis easier to apply*)
 goal thy  
  "!!evs. evs : ns_shared lost ==> \
@@ -334,7 +307,7 @@
 by (etac ns_shared.induct 1);
 by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
 by (REPEAT ((eresolve_tac [bexE, conjE, disjE] ORELSE' hyp_subst_tac) 5));
-by (REPEAT_FIRST (resolve_tac [allI, lemma]));
+by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
 by (ALLGOALS 
     (asm_simp_tac 
      (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
diff -r e8d52d05530a -r ae1030e66745 src/HOL/Auth/OtwayRees.ML
--- a/src/HOL/Auth/OtwayRees.ML	Mon Sep 30 11:04:14 1996 +0200
+++ b/src/HOL/Auth/OtwayRees.ML	Mon Sep 30 11:10:22 1996 +0200
@@ -43,7 +43,6 @@
                               :: otway.intrs))));
 qed "otway_mono";
 
-
 (*The Spy can see more than anybody else, except for their initial state*)
 goal thy 
  "!!evs. evs : otway lost ==> \
@@ -301,37 +300,6 @@
 result();
 
 
-(** Specialized rewriting for this proof **)
-
-Delsimps [image_insert];
-Addsimps [image_insert RS sym];
-
-Delsimps [image_Un];
-Addsimps [image_Un RS sym];
-
-goal thy "insert (Key (newK x)) (sees lost A evs) = \
-\         Key `` (newK``{x}) Un (sees lost A evs)";
-by (Fast_tac 1);
-val insert_Key_singleton = result();
-
-goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
-\         Key `` (f `` (insert x E)) Un C";
-by (Fast_tac 1);
-val insert_Key_image = result();
-
-
-(*This lets us avoid analyzing the new message -- unless we have to!*)
-(*NEEDED??*)
-goal thy "synth (analz (sees lost Spy evs)) <=   \
-\         synth (analz (sees lost Spy (Says A B X # evs)))";
-by (Simp_tac 1);
-by (rtac (subset_insertI RS analz_mono RS synth_mono) 1);
-qed "synth_analz_thin";
-
-AddIs [impOfSubs synth_analz_thin];
-
-
-
 (** Session keys are not used to encrypt other session keys **)
 
 (*Describes the form of Key K when the following message is sent.  The use of
@@ -358,7 +326,8 @@
 goal thy 
  "!!evs. [| Says B' A {|N, Crypt {|N, Key K|} (shrK A)|} : set_of_list evs;  \
 \           evs : otway lost |]                      \
-\        ==> (EX evt: otway lost. K = newK evt) | Key K : analz (sees lost Spy evs)";
+\        ==> (EX evt: otway lost. K = newK evt)          \
+\          | Key K : analz (sees lost Spy evs)";
 by (excluded_middle_tac "A : lost" 1);
 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
                       addss (!simpset)) 2);
@@ -369,15 +338,6 @@
 qed "Reveal_message_form";
 
 
-(*Lemma for the trivial direction of the if-and-only-if*)
-goal thy  
- "!!evs. (Key K : analz (Key``nE Un sEe)) --> \
-\         (K : nE | Key K : analz sEe)  ==>     \
-\        (Key K : analz (Key``nE Un sEe)) = (K : nE | Key K : analz sEe)";
-by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
-val lemma = result();
-
-
 (*The equality makes the induction hypothesis easier to apply*)
 goal thy  
  "!!evs. evs : otway lost ==> \
@@ -387,7 +347,7 @@
 by (dtac OR2_analz_sees_Spy 4);
 by (dtac OR4_analz_sees_Spy 6);
 by (dtac Reveal_message_form 7);
-by (REPEAT_FIRST (ares_tac [allI, lemma]));
+by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
 by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 7));
 by (ALLGOALS (*Takes 28 secs*)
     (asm_simp_tac 
diff -r e8d52d05530a -r ae1030e66745 src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Mon Sep 30 11:04:14 1996 +0200
+++ b/src/HOL/Auth/Shared.ML	Mon Sep 30 11:10:22 1996 +0200
@@ -10,38 +10,6 @@
 
 
 
-(****************DELETE****************)
-
-local
-    fun string_of (a,0) = a
-      | string_of (a,i) = a ^ "_" ^ string_of_int i;
-in
-  fun freeze_thaw th =
-    let val fth = freezeT th
-        val {prop,sign,...} = rep_thm fth
-        fun mk_inst (Var(v,T)) = 
-            (cterm_of sign (Var(v,T)),
-             cterm_of sign (Free(string_of v, T)))
-        val insts = map mk_inst (term_vars prop)
-        fun thaw th' = 
-            th' |> forall_intr_list (map #2 insts)
-                |> forall_elim_list (map #1 insts)
-    in  (instantiate ([],insts) fth, thaw)  end;
-end;
-fun defer_tac i state = 
-    let val (state',thaw) = freeze_thaw state
-        val hyps = Drule.strip_imp_prems (adjust_maxidx (cprop_of state'))
-        val hyp::hyps' = drop(i-1,hyps)
-    in  implies_intr hyp (implies_elim_list state' (map assume hyps)) 
-        |> implies_intr_list (take(i-1,hyps) @ hyps')
-        |> thaw
-        |> Sequence.single
-    end
-    handle Bind => Sequence.null;
-
-
-
-
 (*GOALS.ML??*)
 fun prlim n = (goals_limit:=n; pr());
 
@@ -132,12 +100,12 @@
 qed_spec_mp "sees_own_shrK";
 
 (*Spy sees shared keys of lost agents!*)
-goal thy "!!i. A: lost ==> Key (shrK A) : sees lost Spy evs";
+goal thy "!!A. A: lost ==> Key (shrK A) : sees lost Spy evs";
 by (list.induct_tac "evs" 1);
 by (Auto_tac());
-qed "Spy_sees_bad";
+qed "Spy_sees_lost";
 
-AddSIs [sees_own_shrK, Spy_sees_bad];
+AddSIs [sees_own_shrK, Spy_sees_lost];
 
 
 (** Specialized rewrite rules for (sees lost A (Says...#evs)) **)
@@ -259,8 +227,37 @@
 
 
 (** Simplifying   parts (insert X (sees lost A evs))
-                = parts {X} Un parts (sees lost A evs) -- since general case loops*)
+      = parts {X} Un parts (sees lost A evs) -- since general case loops*)
 
 val parts_insert_sees = 
-    parts_insert |> read_instantiate_sg (sign_of thy) [("H", "sees lost A evs")]
+    parts_insert |> read_instantiate_sg (sign_of thy)
+                                        [("H", "sees lost A evs")]
                  |> standard;
+
+
+(** Specialized rewriting for  **)
+
+Delsimps [image_insert];
+Addsimps [image_insert RS sym];
+
+Delsimps [image_Un];
+Addsimps [image_Un RS sym];
+
+goal thy "insert (Key (newK x)) H = Key `` (newK``{x}) Un H";
+by (Fast_tac 1);
+qed "insert_Key_singleton";
+
+goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
+\         Key `` (f `` (insert x E)) Un C";
+by (Fast_tac 1);
+qed "insert_Key_image";
+
+
+(*Lemma for the trivial direction of the if-and-only-if*)
+goal thy  
+ "!!evs. (Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H)  ==> \
+\        (Key K : analz (Key``nE Un H)) = (K : nE | Key K : analz H)";
+by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
+qed "analz_image_newK_lemma";
+
+
diff -r e8d52d05530a -r ae1030e66745 src/HOL/Auth/Yahalom.ML
--- a/src/HOL/Auth/Yahalom.ML	Mon Sep 30 11:04:14 1996 +0200
+++ b/src/HOL/Auth/Yahalom.ML	Mon Sep 30 11:10:22 1996 +0200
@@ -31,6 +31,14 @@
 
 (**** Inductive proofs about yahalom ****)
 
+goal thy "!!evs. lost' <= lost ==> yahalom lost' <= yahalom lost";
+by (rtac subsetI 1);
+by (etac yahalom.induct 1);
+by (REPEAT_FIRST
+    (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
+                              :: yahalom.intrs))));
+qed "yahalom_mono";
+
 (*The Spy can see more than anybody else, except for their initial state*)
 goal thy 
  "!!evs. evs : yahalom lost ==> \
@@ -40,6 +48,15 @@
                                 addss (!simpset))));
 qed "sees_agent_subset_sees_Spy";
 
+(*The Spy can see more than anybody else who's lost their key!*)
+goal thy 
+ "!!evs. evs : yahalom lost ==> \
+\        A: lost --> A ~= Server --> sees lost A evs <= sees lost Spy evs";
+by (etac yahalom.induct 1);
+by (agent.induct_tac "A" 1);
+by (auto_tac (!claset addDs [sees_Says_subset_insert RS subsetD], (!simpset)));
+qed_spec_mp "sees_lost_agent_subset_sees_Spy";
+
 
 (*Nobody sends themselves messages*)
 goal thy "!!evs. evs : yahalom lost ==> ALL A X. Says A A X ~: set_of_list evs";
@@ -222,55 +239,15 @@
 result();
 
 
-(** Specialized rewriting for this proof **)
-
-Delsimps [image_insert];
-Addsimps [image_insert RS sym];
-
-Delsimps [image_Un];
-Addsimps [image_Un RS sym];
-
-goal thy "insert (Key (newK x)) (sees lost A evs) = \
-\         Key `` (newK``{x}) Un (sees lost A evs)";
-by (Fast_tac 1);
-val insert_Key_singleton = result();
-
-goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
-\         Key `` (f `` (insert x E)) Un C";
-by (Fast_tac 1);
-val insert_Key_image = result();
-
-
-(*This lets us avoid analyzing the new message -- unless we have to!*)
-(*NEEDED??*)
-goal thy "synth (analz (sees lost Spy evs)) <=   \
-\         synth (analz (sees lost Spy (Says A B X # evs)))";
-by (Simp_tac 1);
-by (rtac (subset_insertI RS analz_mono RS synth_mono) 1);
-qed "synth_analz_thin";
-
-AddIs [impOfSubs synth_analz_thin];
-
-
-
 (** Session keys are not used to encrypt other session keys **)
 
-(*Lemma for the trivial direction of the if-and-only-if*)
-goal thy  
- "!!evs. (Key K : analz (Key``nE Un sEe)) --> \
-\         (K : nE | Key K : analz sEe)  ==>     \
-\        (Key K : analz (Key``nE Un sEe)) = (K : nE | Key K : analz sEe)";
-by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
-val lemma = result();
-
-
 goal thy  
  "!!evs. evs : yahalom lost ==> \
 \  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
 \           (K : newK``E | Key K : analz (sees lost Spy evs))";
 by (etac yahalom.induct 1);
 by (dtac YM4_analz_sees_Spy 6);
-by (REPEAT_FIRST (resolve_tac [allI, lemma]));
+by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
 by (ALLGOALS 
     (asm_simp_tac 
      (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
@@ -349,6 +326,20 @@
 qed "Spy_not_see_encrypted_key";
 
 
+goal thy 
+ "!!evs. [| C ~: {A,B,Server};                                          \
+\           Says Server A                                               \
+\            {|Crypt {|Agent B, K, NA, NB|} (shrK A),                   \
+\              Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs;       \
+\           A ~: lost;  B ~: lost;  evs : yahalom lost |] ==>           \
+\     K ~: analz (sees lost C evs)";
+by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
+by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
+by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
+by (REPEAT_FIRST (fast_tac (!claset addIs [yahalom_mono RS subsetD])));
+qed "Agent_not_see_encrypted_key";
+
+
 (** Towards proofs of stronger authenticity properties **)
 
 goal thy