Changing "lost" from a parameter of protocol definitions to a constant.
Advantages: no "lost" argument everywhere; fewer Vars in subgoals;
less need for specially instantiated rules
Disadvantage: can no longer prove "Agent_not_see_encrypted_key", but this
theorem was never used, and its original proof was also broken
the introduction of the "Notes" constructor.
1 (* Title: HOL/Auth/Event
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4 Copyright 1996 University of Cambridge
6 Theory of events for security protocols
8 Datatype of events; function "sees"; freshness
11 Event = Message + List +
13 consts (*Initial states of agents -- parameter of the construction*)
14 initState :: agent => msg set
16 datatype (*Messages--could add another constructor for agent knowledge*)
17 event = Says agent agent msg
21 sees1 :: [agent, event] => msg set
24 (*Spy reads all traffic whether addressed to him or not*)
25 sees1_Says "sees1 A (Says A' B X) = (if A:{B,Spy} then {X} else {})"
26 sees1_Notes "sees1 A (Notes A' X) = (if A = A' then {X} else {})"
29 lost :: agent set (*agents whose private keys have been compromised*)
30 sees :: [agent, event list] => msg set
33 (*Spy has access to his own key for spoof messages, but Server is secure*)
34 Spy_in_lost "Spy: lost"
35 Server_not_lost "Server ~: lost"
38 sees_Nil "sees A [] = initState A"
39 sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
42 (*Set of items that might be visible to somebody: complement of the set
44 used :: event list => msg set
45 "used evs == parts (UN B. sees B evs)"