29 "isSymKey K == (invKey K = K)" |
29 "isSymKey K == (invKey K = K)" |
30 |
30 |
31 datatype (*We allow any number of friendly agents*) |
31 datatype (*We allow any number of friendly agents*) |
32 agent = Server | Friend nat | Spy |
32 agent = Server | Friend nat | Spy |
33 |
33 |
|
34 |
|
35 (*Datatype msg is (awkwardly) split into two parts to avoid having freeness |
|
36 expressed using natural numbers.*) |
34 datatype |
37 datatype |
35 atomic = AGENT agent (*Agent names*) |
38 atomic = AGENT agent (*Agent names*) |
36 | NUMBER nat (*Ordinary integers, timestamps, ...*) |
39 | NUMBER nat (*Ordinary integers, timestamps, ...*) |
37 | NONCE nat (*Unguessable nonces*) |
40 | NONCE nat (*Unguessable nonces*) |
38 | KEY key (*Crypto keys*) |
41 | KEY key (*Crypto keys*) |
39 |
42 |
40 datatype |
43 datatype |
41 msg = Atomic atomic |
44 msg = Atomic atomic |
42 | Hash msg (*Hashing*) |
45 | Hash msg (*Hashing*) |
43 | MPair msg msg (*Compound messages*) |
46 | MPair msg msg (*Compound messages*) |
44 | Crypt key msg (*Encryption, public- or shared-key*) |
47 | Crypt key msg (*Encryption, public- or shared-key*) |
45 |
48 |
46 (*Allows messages of the form {|A,B,NA|}, etc...*) |
49 (*These translations complete the illustion that "msg" has seven constructors*) |
47 syntax |
50 syntax |
48 Agent :: agent => msg |
51 Agent :: agent => msg |
49 Number :: nat => msg |
52 Number :: nat => msg |
50 Nonce :: nat => msg |
53 Nonce :: nat => msg |
51 Key :: key => msg |
54 Key :: key => msg |
|
55 |
|
56 translations |
|
57 "Agent x" == "Atomic (AGENT x)" |
|
58 "Number x" == "Atomic (NUMBER x)" |
|
59 "Nonce x" == "Atomic (NONCE x)" |
|
60 "Key x" == "Atomic (KEY x)" |
|
61 "Key``x" == "Atomic `` (KEY `` x)" |
|
62 |
|
63 |
|
64 (*Concrete syntax: messages appear as {|A,B,NA|}, etc...*) |
|
65 syntax |
52 "@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})") |
66 "@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})") |
53 |
67 |
54 translations |
68 translations |
55 "Agent x" == "Atomic (AGENT x)" |
|
56 "Number x" == "Atomic (NUMBER x)" |
|
57 "Nonce x" == "Atomic (NONCE x)" |
|
58 "Key x" == "Atomic (KEY x)" |
|
59 "Key``x" == "Atomic `` (KEY `` x)" |
|
60 |
|
61 "{|x, y, z|}" == "{|x, {|y, z|}|}" |
69 "{|x, y, z|}" == "{|x, {|y, z|}|}" |
62 "{|x, y|}" == "MPair x y" |
70 "{|x, y|}" == "MPair x y" |
63 |
71 |
64 |
72 |
65 constdefs |
73 constdefs |