3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1996 University of Cambridge |
4 Copyright 1996 University of Cambridge |
5 |
5 |
6 Theory of events for security protocols |
6 Theory of events for security protocols |
7 |
7 |
8 Datatype of events; function "sees"; freshness |
8 Datatype of events; function "spies"; freshness |
9 |
9 |
10 "lost" agents have been broken by the Spy; their private keys and internal |
10 "bad" agents have been broken by the Spy; their private keys and internal |
11 stores are visible to him |
11 stores are visible to him |
12 *) |
12 *) |
13 |
13 |
14 Event = Message + List + |
14 Event = Message + List + |
15 |
15 |
19 datatype (*Messages--could add another constructor for agent knowledge*) |
19 datatype (*Messages--could add another constructor for agent knowledge*) |
20 event = Says agent agent msg |
20 event = Says agent agent msg |
21 | Notes agent msg |
21 | Notes agent msg |
22 |
22 |
23 consts |
23 consts |
24 lost :: agent set (*compromised agents*) |
24 bad :: agent set (*compromised agents*) |
25 sees :: [agent, event list] => msg set |
25 spies :: event list => msg set |
26 |
26 |
27 rules |
27 rules |
28 (*Spy has access to his own key for spoof messages, but Server is secure*) |
28 (*Spy has access to his own key for spoof messages, but Server is secure*) |
29 Spy_in_lost "Spy: lost" |
29 Spy_in_bad "Spy: bad" |
30 Server_not_lost "Server ~: lost" |
30 Server_not_bad "Server ~: bad" |
31 |
31 |
32 consts |
32 primrec spies list |
33 sees1 :: [agent, event] => msg set |
33 (*Spy reads all traffic whether addressed to him or not*) |
|
34 spies_Nil "spies [] = initState Spy" |
|
35 spies_Cons "spies (ev # evs) = |
|
36 (case ev of |
|
37 Says A B X => insert X (spies evs) |
|
38 | Notes A X => |
|
39 if A:bad then insert X (spies evs) else spies evs)" |
34 |
40 |
35 primrec sees1 event |
41 consts |
36 (*Spy reads all traffic whether addressed to him or not*) |
42 (*Set of items that might be visible to somebody: |
37 sees1_Says "sees1 A (Says A' B X) = (if A:{B,Spy} then {X} else {})" |
43 complement of the set of fresh items*) |
38 sees1_Notes "sees1 A (Notes A' X) = (if A=A' | A=Spy & A':lost then {X} |
44 used :: event list => msg set |
39 else {})" |
|
40 |
45 |
41 primrec sees list |
46 primrec used list |
42 sees_Nil "sees A [] = initState A" |
47 used_Nil "used [] = (UN B. parts (initState B))" |
43 sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs" |
48 used_Cons "used (ev # evs) = |
44 |
49 (case ev of |
45 constdefs |
50 Says A B X => parts {X} Un (used evs) |
46 (*Set of items that might be visible to somebody: complement of the set |
51 | Notes A X => parts {X} Un (used evs))" |
47 of fresh items*) |
|
48 used :: event list => msg set |
|
49 "used evs == parts (UN B. sees B evs)" |
|
50 |
52 |
51 end |
53 end |