src/HOL/Auth/Event.thy
changeset 3519 ab0a9fbed4c0
parent 3512 9dcb4daa15e8
child 3678 414e04d7c2d6
--- a/src/HOL/Auth/Event.thy	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/Event.thy	Mon Jul 14 12:47:21 1997 +0200
@@ -11,7 +11,7 @@
 Event = Message + List + 
 
 consts  (*Initial states of agents -- parameter of the construction*)
-  initState :: [agent set, agent] => msg set
+  initState :: agent => msg set
 
 datatype  (*Messages--could add another constructor for agent knowledge*)
   event = Says  agent agent msg
@@ -26,17 +26,22 @@
   sees1_Notes "sees1 A (Notes A' X)   = (if A = A'    then {X} else {})"
 
 consts  
-  sees :: [agent set, agent, event list] => msg set
+  lost :: agent set        (*agents whose private keys have been compromised*)
+  sees :: [agent, event list] => msg set
+
+rules
+  (*Spy has access to his own key for spoof messages, but Server is secure*)
+  Spy_in_lost     "Spy: lost"
+  Server_not_lost "Server ~: lost"
 
 primrec sees list
-  sees_Nil  "sees lost A []       = initState lost A"
-  sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
-
+  sees_Nil  "sees A []       = initState A"
+  sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
 
 constdefs
   (*Set of items that might be visible to somebody: complement of the set
         of fresh items*)
   used :: event list => msg set
-    "used evs == parts (UN lost B. sees lost B evs)"
+    "used evs == parts (UN B. sees B evs)"
 
 end