# HG changeset patch
# User paulson
# Date 874507047 -7200
# Node ID 414e04d7c2d6dc9d0e8a52ac817bbbbef0e75bf3
# Parent  f2569416d18b3dfd6cdaeb8a0d9246b172a6847d
Spy can see Notes of the compromised agents

diff -r f2569416d18b -r 414e04d7c2d6 src/HOL/Auth/Event.ML
--- a/src/HOL/Auth/Event.ML	Wed Sep 17 16:37:21 1997 +0200
+++ b/src/HOL/Auth/Event.ML	Wed Sep 17 16:37:27 1997 +0200
@@ -12,34 +12,59 @@
 
 AddIffs [Spy_in_lost, Server_not_lost];
 
-(*** Function "sees" ***)
+(**** Function "sees" ****)
 
-(** Specialized rewrite rules for (sees A (Says...#evs)) **)
+(** Specialized rewrite rules for (sees A' (Says A B X #evs)) **)
 
 goal thy "sees B (Says A B X # evs) = insert X (sees B evs)";
 by (Simp_tac 1);
-qed "sees_own";
-
-goal thy "sees B (Notes A X # evs) = \
-\         (if A=B then insert X (sees B evs) else sees B evs)";
-by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
-qed "sees_Notes";
+qed "sees_own_Says";
 
 (** Three special-case rules for rewriting of sees A **)
 
 goal thy "!!A. Server ~= B ==> \
-\          sees Server (Says A B X # evs) = sees Server evs";
+\              sees Server (Says A B X # evs) = sees Server evs";
 by (Asm_simp_tac 1);
-qed "sees_Server";
+qed "sees_Server_Says";
 
 goal thy "!!A. Friend i ~= B ==> \
-\          sees (Friend i) (Says A B X # evs) = sees (Friend i) evs";
+\              sees (Friend i) (Says A B X # evs) = sees (Friend i) evs";
 by (Asm_simp_tac 1);
-qed "sees_Friend";
+qed "sees_Friend_Says";
 
 goal thy "sees Spy (Says A B X # evs) = insert X (sees Spy evs)";
 by (Simp_tac 1);
-qed "sees_Spy";
+qed "sees_Spy_Says";
+
+
+(** Specialized rewrite rules for (sees A' (Notes A X evs)) **)
+
+goal thy "sees A (Notes A X # evs) = insert X (sees A evs)";
+by (Simp_tac 1);
+qed "sees_own_Notes";
+
+(** Three special-case rules for rewriting of sees A **)
+
+goal thy "!!A. Server ~= A ==> \
+\              sees Server (Notes A X # evs) = sees Server evs";
+by (Asm_simp_tac 1);
+qed "sees_Server_Notes";
+
+goal thy "!!A. Friend i ~= A ==> \
+\              sees (Friend i) (Notes A X # evs) = sees (Friend i) evs";
+by (Asm_simp_tac 1);
+qed "sees_Friend_Notes";
+
+(*The point of letting the Spy see "lost" agents' notes is to prevent
+  redundant case-splits on whether A=Spy and whether A:lost*)
+goal thy "sees Spy (Notes A X # evs) = \
+\         (if A:lost then insert X (sees Spy evs) else sees Spy evs)";
+by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (Blast_tac 1);
+qed "sees_Spy_Notes";
+
+
+(** Other "sees" lemmas **)
 
 goal thy "sees A (Says A' B X # evs) <= insert X (sees A evs)";
 by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
@@ -75,16 +100,24 @@
 				       setloop split_tac [expand_if]))));
 qed "UN_parts_sees_Notes";
 
+(*Spy sees all traffic*)
 goal thy "Says A B X : set evs --> X : sees Spy evs";
 by (induct_tac "evs" 1);
 by (Auto_tac ());
 qed_spec_mp "Says_imp_sees_Spy";
 
+(*Spy sees Notes of lost agents*)
+goal thy "Notes A X : set evs --> A: lost --> X : sees Spy evs";
+by (induct_tac "evs" 1);
+by (Auto_tac ());
+qed_spec_mp "Notes_imp_sees_Spy";
+
 (*Use with addSEs to derive contradictions from old Says events containing
   items known to be fresh*)
-val sees_Spy_partsEs = make_elim (Says_imp_sees_Spy RS parts.Inj):: partsEs;
+val sees_Spy_partsEs = make_elim (Says_imp_sees_Spy RS parts.Inj) :: partsEs;
 
-Addsimps [sees_own, sees_Notes, sees_Server, sees_Friend, sees_Spy];
+Addsimps [sees_own_Says, sees_Server_Says, sees_Friend_Says, sees_Spy_Says,
+      sees_own_Notes, sees_Server_Notes, sees_Friend_Notes, sees_Spy_Notes];
 
 (**** NOTE REMOVAL--laws above are cleaner--def of sees1 is messy ****)
 Delsimps [sees_Cons];   
@@ -104,8 +137,7 @@
 Addsimps [used_Says];
 
 goal thy "used (Notes A X # evs) = parts{X} Un used evs";
-by (simp_tac (!simpset delsimps [sees_Notes]
-		       addsimps [used_def, UN_parts_sees_Notes]) 1);
+by (simp_tac (!simpset addsimps [used_def, UN_parts_sees_Notes]) 1);
 qed "used_Notes";
 Addsimps [used_Notes];
 
diff -r f2569416d18b -r 414e04d7c2d6 src/HOL/Auth/Event.thy
--- a/src/HOL/Auth/Event.thy	Wed Sep 17 16:37:21 1997 +0200
+++ b/src/HOL/Auth/Event.thy	Wed Sep 17 16:37:27 1997 +0200
@@ -6,6 +6,9 @@
 Theory of events for security protocols
 
 Datatype of events; function "sees"; freshness
+
+"lost" agents have been broken by the Spy; their private keys and internal
+    stores are visible to him
 *)
 
 Event = Message + List + 
@@ -18,15 +21,7 @@
         | Notes agent       msg
 
 consts  
-  sees1 :: [agent, event] => msg set
-
-primrec sees1 event
-           (*Spy reads all traffic whether addressed to him or not*)
-  sees1_Says  "sees1 A (Says A' B X)  = (if A:{B,Spy} then {X} else {})"
-  sees1_Notes "sees1 A (Notes A' X)   = (if A = A'    then {X} else {})"
-
-consts  
-  lost :: agent set        (*agents whose private keys have been compromised*)
+  lost :: agent set        (*compromised agents*)
   sees :: [agent, event list] => msg set
 
 rules
@@ -34,6 +29,15 @@
   Spy_in_lost     "Spy: lost"
   Server_not_lost "Server ~: lost"
 
+consts  
+  sees1 :: [agent, event] => msg set
+
+primrec sees1 event
+           (*Spy reads all traffic whether addressed to him or not*)
+  sees1_Says  "sees1 A (Says A' B X)  = (if A:{B,Spy} then {X} else {})"
+  sees1_Notes "sees1 A (Notes A' X)   = (if A=A' | A=Spy & A':lost then {X}
+					 else {})"
+
 primrec sees list
   sees_Nil  "sees A []       = initState A"
   sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"