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 datatype (*Messages are agent names, nonces, keys, pairs and encryptions*) |
34 datatype |
35 msg = Agent agent |
35 atomic = AGENT agent (*Agent names*) |
36 | Nonce nat |
36 | NUMBER nat (*Ordinary integers, timestamps, ...*) |
37 | Key key |
37 | NONCE nat (*Unguessable nonces*) |
38 | Hash msg |
38 | KEY key (*Crypto keys*) |
39 | MPair msg msg |
39 |
40 | Crypt key msg |
40 datatype |
|
41 msg = Atomic atomic |
|
42 | Hash msg (*Hashing*) |
|
43 | MPair msg msg (*Compound messages*) |
|
44 | Crypt key msg (*Encryption, public- or shared-key*) |
41 |
45 |
42 (*Allows messages of the form {|A,B,NA|}, etc...*) |
46 (*Allows messages of the form {|A,B,NA|}, etc...*) |
43 syntax |
47 syntax |
|
48 Agent :: agent => msg |
|
49 Number :: nat => msg |
|
50 Nonce :: nat => msg |
|
51 Key :: key => msg |
44 "@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})") |
52 "@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})") |
45 |
53 |
46 translations |
54 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 |
47 "{|x, y, z|}" == "{|x, {|y, z|}|}" |
61 "{|x, y, z|}" == "{|x, {|y, z|}|}" |
48 "{|x, y|}" == "MPair x y" |
62 "{|x, y|}" == "MPair x y" |
49 |
63 |
50 |
64 |
51 constdefs |
65 constdefs |
81 Decrypt "[| Crypt K X : analz H; Key(invKey K): analz H |] ==> X : analz H" |
95 Decrypt "[| Crypt K X : analz H; Key(invKey K): analz H |] ==> X : analz H" |
82 |
96 |
83 |
97 |
84 (** Inductive definition of "synth" -- what can be built up from a set of |
98 (** Inductive definition of "synth" -- what can be built up from a set of |
85 messages. A form of upward closure. Pairs can be built, messages |
99 messages. A form of upward closure. Pairs can be built, messages |
86 encrypted with known keys. Agent names may be quoted. **) |
100 encrypted with known keys. Agent names are public domain. |
|
101 Numbers can be guessed, but Nonces cannot be. **) |
87 |
102 |
88 consts synth :: msg set => msg set |
103 consts synth :: msg set => msg set |
89 inductive "synth H" |
104 inductive "synth H" |
90 intrs |
105 intrs |
91 Inj "X: H ==> X: synth H" |
106 Inj "X: H ==> X: synth H" |
92 Agent "Agent agt : synth H" |
107 Agent "Agent agt : synth H" |
|
108 Number "Number n : synth H" |
93 Hash "X: synth H ==> Hash X : synth H" |
109 Hash "X: synth H ==> Hash X : synth H" |
94 MPair "[| X: synth H; Y: synth H |] ==> {|X,Y|} : synth H" |
110 MPair "[| X: synth H; Y: synth H |] ==> {|X,Y|} : synth H" |
95 Crypt "[| X: synth H; Key(K) : H |] ==> Crypt K X : synth H" |
111 Crypt "[| X: synth H; Key(K) : H |] ==> Crypt K X : synth H" |
96 |
112 |
97 end |
113 end |