equal
deleted
inserted
replaced
23 where "priK x \<equiv> invKey(pubK x)" |
23 where "priK x \<equiv> invKey(pubK x)" |
24 (*<*) |
24 (*<*) |
25 primrec |
25 primrec |
26 (*Agents know their private key and all public keys*) |
26 (*Agents know their private key and all public keys*) |
27 initState_Server: "initState Server = |
27 initState_Server: "initState Server = |
28 insert (Key (priK Server)) (Key ` range pubK)" |
28 insert (Key (priK Server)) (Key ` range pubK)" |
29 initState_Friend: "initState (Friend i) = |
29 initState_Friend: "initState (Friend i) = |
30 insert (Key (priK (Friend i))) (Key ` range pubK)" |
30 insert (Key (priK (Friend i))) (Key ` range pubK)" |
31 initState_Spy: "initState Spy = |
31 initState_Spy: "initState Spy = |
32 (Key`invKey`pubK`bad) Un (Key ` range pubK)" |
32 (Key`invKey`pubK`bad) Un (Key ` range pubK)" |
33 (*>*) |
33 (*>*) |
34 |
34 |
35 text {* |
35 text {* |
36 \noindent |
36 \noindent |
37 The set @{text bad} consists of those agents whose private keys are known to |
37 The set @{text bad} consists of those agents whose private keys are known to |