src/HOL/Auth/Event.thy
changeset 6308 76f3865a2b1d
parent 5183 89f162de39cf
child 6399 4a9040b85e2e
--- a/src/HOL/Auth/Event.thy	Mon Mar 08 13:49:53 1999 +0100
+++ b/src/HOL/Auth/Event.thy	Tue Mar 09 11:01:39 1999 +0100
@@ -19,24 +19,49 @@
 datatype  (*Messages--could add another constructor for agent knowledge*)
   event = Says  agent agent msg
         | Notes agent       msg
+        | Gets  agent       msg
+       
+consts 
+  bad    :: agent set        (*compromised agents*)
+  knows  :: agent => event list => msg set
 
-consts  
-  bad    :: agent set        (*compromised agents*)
+
+(*"spies" is retained for compability's sake*)
+syntax
   spies  :: event list => msg set
 
+translations
+  "spies"   => "knows Spy"
+
+
 rules
   (*Spy has access to his own key for spoof messages, but Server is secure*)
   Spy_in_bad     "Spy: bad"
   Server_not_bad "Server ~: bad"
 
 primrec
-           (*Spy reads all traffic whether addressed to him or not*)
-  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)"
+  knows_Nil   "knows A []         = initState A"
+  knows_Cons  "knows A (ev # evs) =
+	        (if A = Spy then 
+                  (case ev of
+		    Says A' B X => insert X (knows Spy evs)
+		  | Notes A' X  => 
+                   if A' : bad then insert X (knows Spy evs) else knows Spy evs
+                  | Gets A' X => knows Spy evs)
+                 else
+                  (case ev of
+		    Says A' B X => 
+                      if A'=A then insert X (knows A evs) else knows A evs
+		  | Notes A' X    => 
+                      if A'=A then insert X (knows A evs) else knows A evs
+		  | Gets A' X    => 
+                      if A'=A then insert X (knows A evs) else knows A evs))"
+
+(*
+  Case A=Spy on the Gets event
+  enforces the fact that if a message is received then it must have been sent,
+  therefore the oops case must use Notes
+*)
 
 consts
   (*Set of items that might be visible to somebody:
@@ -48,6 +73,9 @@
   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))"
+		  | Notes A X  => parts {X} Un (used evs)
+		  | Gets A X   => used evs)"
+
+
 
 end