equal
deleted
inserted
replaced
22 knows :: "agent => event list => msg set" (*agents' knowledge*) |
22 knows :: "agent => event list => msg set" (*agents' knowledge*) |
23 stolen :: "card set" (* stolen smart cards *) |
23 stolen :: "card set" (* stolen smart cards *) |
24 cloned :: "card set" (* cloned smart cards*) |
24 cloned :: "card set" (* cloned smart cards*) |
25 secureM :: "bool"(*assumption of secure means between agents and their cards*) |
25 secureM :: "bool"(*assumption of secure means between agents and their cards*) |
26 |
26 |
27 syntax |
27 abbreviation |
28 insecureM :: bool (*certain protocols make no assumption of secure means*) |
28 insecureM :: bool (*certain protocols make no assumption of secure means*) |
29 translations |
29 "insecureM == \<not>secureM" |
30 "insecureM" == "\<not>secureM" |
|
31 |
30 |
32 |
31 |
33 text{*Spy has access to his own key for spoof messages, but Server is secure*} |
32 text{*Spy has access to his own key for spoof messages, but Server is secure*} |
34 specification (bad) |
33 specification (bad) |
35 Spy_in_bad [iff]: "Spy \<in> bad" |
34 Spy_in_bad [iff]: "Spy \<in> bad" |