21 | Gets agent msg |
21 | Gets agent msg |
22 | Notes agent msg |
22 | Notes agent msg |
23 |
23 |
24 consts |
24 consts |
25 bad :: "agent set" -- {* compromised agents *} |
25 bad :: "agent set" -- {* compromised agents *} |
26 knows :: "agent => event list => msg set" |
|
27 |
26 |
28 |
27 |
29 text{*The constant "spies" is retained for compatibility's sake*} |
28 text{*The constant "spies" is retained for compatibility's sake*} |
30 |
29 |
31 abbreviation (input) |
|
32 spies :: "event list => msg set" where |
|
33 "spies == knows Spy" |
|
34 |
|
35 text{*Spy has access to his own key for spoof messages, but Server is secure*} |
|
36 specification (bad) |
|
37 Spy_in_bad [iff]: "Spy \<in> bad" |
|
38 Server_not_bad [iff]: "Server \<notin> bad" |
|
39 by (rule exI [of _ "{Spy}"], simp) |
|
40 |
|
41 primrec |
30 primrec |
|
31 knows :: "agent => event list => msg set" |
|
32 where |
42 knows_Nil: "knows A [] = initState A" |
33 knows_Nil: "knows A [] = initState A" |
43 knows_Cons: |
34 | knows_Cons: |
44 "knows A (ev # evs) = |
35 "knows A (ev # evs) = |
45 (if A = Spy then |
36 (if A = Spy then |
46 (case ev of |
37 (case ev of |
47 Says A' B X => insert X (knows Spy evs) |
38 Says A' B X => insert X (knows Spy evs) |
48 | Gets A' X => knows Spy evs |
39 | Gets A' X => knows Spy evs |
55 | Gets A' X => |
46 | Gets A' X => |
56 if A'=A then insert X (knows A evs) else knows A evs |
47 if A'=A then insert X (knows A evs) else knows A evs |
57 | Notes A' X => |
48 | Notes A' X => |
58 if A'=A then insert X (knows A evs) else knows A evs))" |
49 if A'=A then insert X (knows A evs) else knows A evs))" |
59 |
50 |
|
51 abbreviation (input) |
|
52 spies :: "event list => msg set" where |
|
53 "spies == knows Spy" |
|
54 |
|
55 text{*Spy has access to his own key for spoof messages, but Server is secure*} |
|
56 specification (bad) |
|
57 Spy_in_bad [iff]: "Spy \<in> bad" |
|
58 Server_not_bad [iff]: "Server \<notin> bad" |
|
59 by (rule exI [of _ "{Spy}"], simp) |
|
60 |
60 (* |
61 (* |
61 Case A=Spy on the Gets event |
62 Case A=Spy on the Gets event |
62 enforces the fact that if a message is received then it must have been sent, |
63 enforces the fact that if a message is received then it must have been sent, |
63 therefore the oops case must use Notes |
64 therefore the oops case must use Notes |
64 *) |
65 *) |
65 |
66 |
66 consts |
67 primrec |
67 (*Set of items that might be visible to somebody: |
68 (*Set of items that might be visible to somebody: |
68 complement of the set of fresh items*) |
69 complement of the set of fresh items*) |
69 used :: "event list => msg set" |
70 used :: "event list => msg set" |
70 |
71 where |
71 primrec |
|
72 used_Nil: "used [] = (UN B. parts (initState B))" |
72 used_Nil: "used [] = (UN B. parts (initState B))" |
73 used_Cons: "used (ev # evs) = |
73 | used_Cons: "used (ev # evs) = |
74 (case ev of |
74 (case ev of |
75 Says A B X => parts {X} \<union> used evs |
75 Says A B X => parts {X} \<union> used evs |
76 | Gets A X => used evs |
76 | Gets A X => used evs |
77 | Notes A X => parts {X} \<union> used evs)" |
77 | Notes A X => parts {X} \<union> used evs)" |
78 --{*The case for @{term Gets} seems anomalous, but @{term Gets} always |
78 --{*The case for @{term Gets} seems anomalous, but @{term Gets} always |