src/HOL/Auth/Event.thy
changeset 3683 aafe719dff14
parent 3678 414e04d7c2d6
child 5183 89f162de39cf
--- a/src/HOL/Auth/Event.thy	Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/Event.thy	Thu Sep 18 13:24:04 1997 +0200
@@ -5,9 +5,9 @@
 
 Theory of events for security protocols
 
-Datatype of events; function "sees"; freshness
+Datatype of events; function "spies"; freshness
 
-"lost" agents have been broken by the Spy; their private keys and internal
+"bad" agents have been broken by the Spy; their private keys and internal
     stores are visible to him
 *)
 
@@ -21,31 +21,33 @@
         | Notes agent       msg
 
 consts  
-  lost :: agent set        (*compromised agents*)
-  sees :: [agent, event list] => msg set
+  bad    :: agent set        (*compromised agents*)
+  spies  :: 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"
+  Spy_in_bad     "Spy: bad"
+  Server_not_bad "Server ~: bad"
 
-consts  
-  sees1 :: [agent, event] => msg set
-
-primrec sees1 event
+primrec spies list
            (*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 {})"
+  spies_Nil   "spies []       = initState Spy"
+  spies_Cons  "spies (ev # evs) =
+	         (case ev of
+		    Says A B X => insert X (spies evs)
+		  | Notes A X  => 
+	              if A:bad then insert X (spies evs) else spies evs)"
 
-primrec sees list
-  sees_Nil  "sees A []       = initState A"
-  sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
+consts
+  (*Set of items that might be visible to somebody:
+    complement of the set of fresh items*)
+  used :: event list => msg set
 
-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 B. sees B evs)"
+primrec used list
+  used_Nil   "used []         = (UN B. parts (initState B))"
+  used_Cons  "used (ev # evs) =
+	         (case ev of
+		    Says A B X => parts {X} Un (used evs)
+		  | Notes A X  => parts {X} Un (used evs))"
 
 end