--- 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