equal
deleted
inserted
replaced
19 |
19 |
20 primrec initState agent |
20 primrec initState agent |
21 (*Server knows all long-term keys; other agents know only their own*) |
21 (*Server knows all long-term keys; other agents know only their own*) |
22 initState_Server "initState Server = Key `` range shrK" |
22 initState_Server "initState Server = Key `` range shrK" |
23 initState_Friend "initState (Friend i) = {Key (shrK (Friend i))}" |
23 initState_Friend "initState (Friend i) = {Key (shrK (Friend i))}" |
24 initState_Spy "initState Spy = Key``shrK``lost" |
24 initState_Spy "initState Spy = Key``shrK``bad" |
25 |
25 |
26 |
26 |
27 rules |
27 rules |
28 (*Unlike the corresponding property of nonces, this cannot be proved. |
28 (*Unlike the corresponding property of nonces, this cannot be proved. |
29 We have infinitely many agents and there is nothing to stop their |
29 We have infinitely many agents and there is nothing to stop their |