equal
deleted
inserted
replaced
17 isSym_keys "isSymKey K" (*All keys are symmetric*) |
17 isSym_keys "isSymKey K" (*All keys are symmetric*) |
18 inj_shrK "inj shrK" (*No two agents have the same long-term key*) |
18 inj_shrK "inj shrK" (*No two agents have the same long-term key*) |
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 lost Server = Key `` range shrK" |
22 initState_Server "initState Server = Key `` range shrK" |
23 initState_Friend "initState lost (Friend i) = {Key (shrK (Friend i))}" |
23 initState_Friend "initState (Friend i) = {Key (shrK (Friend i))}" |
24 initState_Spy "initState lost Spy = Key``shrK``lost" |
24 initState_Spy "initState Spy = Key``shrK``lost" |
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 |