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