equal
deleted
inserted
replaced
24 consts |
24 consts |
25 bad :: "agent set" (*compromised agents*) |
25 bad :: "agent set" (*compromised agents*) |
26 knows :: "agent => event list => msg set" |
26 knows :: "agent => event list => msg set" |
27 |
27 |
28 |
28 |
29 (*"spies" is retained for compatibility's sake*) |
29 text{*The constant "spies" is retained for compatibility's sake*} |
30 syntax |
30 syntax |
31 spies :: "event list => msg set" |
31 spies :: "event list => msg set" |
32 |
32 |
33 translations |
33 translations |
34 "spies" => "knows Spy" |
34 "spies" => "knows Spy" |
35 |
35 |
36 |
36 text{*Spy has access to his own key for spoof messages, but Server is secure*} |
37 axioms |
37 specification (bad) |
38 (*Spy has access to his own key for spoof messages, but Server is secure*) |
38 bad_properties: "Spy \<in> bad & Server \<notin> bad" |
39 Spy_in_bad [iff] : "Spy \<in> bad" |
39 by (rule exI [of _ "{Spy}"], simp) |
40 Server_not_bad [iff] : "Server \<notin> bad" |
40 |
|
41 lemmas Spy_in_bad = bad_properties [THEN conjunct1, iff] |
|
42 lemmas Server_not_bad = bad_properties [THEN conjunct2, iff] |
|
43 |
41 |
44 |
42 primrec |
45 primrec |
43 knows_Nil: "knows A [] = initState A" |
46 knows_Nil: "knows A [] = initState A" |
44 knows_Cons: |
47 knows_Cons: |
45 "knows A (ev # evs) = |
48 "knows A (ev # evs) = |