6 Inductive relation "otway" for the Otway-Rees protocol. |
6 Inductive relation "otway" for the Otway-Rees protocol. |
7 |
7 |
8 The FAULTY version omitting encryption of Nonce NB, as suggested on page 247 of |
8 The FAULTY version omitting encryption of Nonce NB, as suggested on page 247 of |
9 Burrows, Abadi and Needham. A Logic of Authentication. |
9 Burrows, Abadi and Needham. A Logic of Authentication. |
10 Proc. Royal Soc. 426 (1989) |
10 Proc. Royal Soc. 426 (1989) |
|
11 |
|
12 This file illustrates the consequences of such errors. We can still prove |
|
13 impressive-looking properties such as Spy_not_see_encrypted_key, yet the |
|
14 protocol is open to a middleperson attack. Attempting to prove some key lemmas |
|
15 indicates the possibility of this attack. |
11 *) |
16 *) |
12 |
17 |
13 OtwayRees_Bad = Shared + |
18 theory OtwayRees_Bad = Shared: |
14 |
19 |
15 consts otway :: event list set |
20 consts otway :: "event list set" |
16 |
21 inductive "otway" |
17 inductive otway |
22 intros |
18 intrs |
|
19 (*Initial trace is empty*) |
23 (*Initial trace is empty*) |
20 Nil "[] \\<in> otway" |
24 Nil: "[] \<in> otway" |
21 |
25 |
22 (*The spy MAY say anything he CAN say. We do not expect him to |
26 (*The spy MAY say anything he CAN say. We do not expect him to |
23 invent new nonces here, but he can also use NS1. Common to |
27 invent new nonces here, but he can also use NS1. Common to |
24 all similar protocols.*) |
28 all similar protocols.*) |
25 Fake "[| evsf \\<in> otway; X \\<in> synth (analz (knows Spy evsf)) |] |
29 Fake: "[| evsf \<in> otway; X \<in> synth (analz (knows Spy evsf)) |] |
26 ==> Says Spy B X # evsf \\<in> otway" |
30 ==> Says Spy B X # evsf \<in> otway" |
27 |
31 |
28 (*A message that has been sent can be received by the |
32 (*A message that has been sent can be received by the |
29 intended recipient.*) |
33 intended recipient.*) |
30 Reception "[| evsr \\<in> otway; Says A B X \\<in> set evsr |] |
34 Reception: "[| evsr \<in> otway; Says A B X \<in>set evsr |] |
31 ==> Gets B X # evsr \\<in> otway" |
35 ==> Gets B X # evsr \<in> otway" |
32 |
36 |
33 (*Alice initiates a protocol run*) |
37 (*Alice initiates a protocol run*) |
34 OR1 "[| evs1 \\<in> otway; Nonce NA \\<notin> used evs1 |] |
38 OR1: "[| evs1 \<in> otway; Nonce NA \<notin> used evs1 |] |
35 ==> Says A B {|Nonce NA, Agent A, Agent B, |
39 ==> Says A B {|Nonce NA, Agent A, Agent B, |
36 Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |} |
40 Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |} |
37 # evs1 \\<in> otway" |
41 # evs1 \<in> otway" |
38 |
42 |
39 (*Bob's response to Alice's message. |
43 (*Bob's response to Alice's message. |
40 This variant of the protocol does NOT encrypt NB.*) |
44 This variant of the protocol does NOT encrypt NB.*) |
41 OR2 "[| evs2 \\<in> otway; Nonce NB \\<notin> used evs2; |
45 OR2: "[| evs2 \<in> otway; Nonce NB \<notin> used evs2; |
42 Gets B {|Nonce NA, Agent A, Agent B, X|} \\<in> set evs2 |] |
46 Gets B {|Nonce NA, Agent A, Agent B, X|} \<in> set evs2 |] |
43 ==> Says B Server |
47 ==> Says B Server |
44 {|Nonce NA, Agent A, Agent B, X, Nonce NB, |
48 {|Nonce NA, Agent A, Agent B, X, Nonce NB, |
45 Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} |
49 Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} |
46 # evs2 \\<in> otway" |
50 # evs2 \<in> otway" |
47 |
51 |
48 (*The Server receives Bob's message and checks that the three NAs |
52 (*The Server receives Bob's message and checks that the three NAs |
49 match. Then he sends a new session key to Bob with a packet for |
53 match. Then he sends a new session key to Bob with a packet for |
50 forwarding to Alice.*) |
54 forwarding to Alice.*) |
51 OR3 "[| evs3 \\<in> otway; Key KAB \\<notin> used evs3; |
55 OR3: "[| evs3 \<in> otway; Key KAB \<notin> used evs3; |
52 Gets Server |
56 Gets Server |
53 {|Nonce NA, Agent A, Agent B, |
57 {|Nonce NA, Agent A, Agent B, |
54 Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, |
58 Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, |
55 Nonce NB, |
59 Nonce NB, |
56 Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} |
60 Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} |
57 \\<in> set evs3 |] |
61 \<in> set evs3 |] |
58 ==> Says Server B |
62 ==> Says Server B |
59 {|Nonce NA, |
63 {|Nonce NA, |
60 Crypt (shrK A) {|Nonce NA, Key KAB|}, |
64 Crypt (shrK A) {|Nonce NA, Key KAB|}, |
61 Crypt (shrK B) {|Nonce NB, Key KAB|}|} |
65 Crypt (shrK B) {|Nonce NB, Key KAB|}|} |
62 # evs3 \\<in> otway" |
66 # evs3 \<in> otway" |
63 |
67 |
64 (*Bob receives the Server's (?) message and compares the Nonces with |
68 (*Bob receives the Server's (?) message and compares the Nonces with |
65 those in the message he previously sent the Server. |
69 those in the message he previously sent the Server. |
66 Need B ~= Server because we allow messages to self.*) |
70 Need B ~= Server because we allow messages to self.*) |
67 OR4 "[| evs4 \\<in> otway; B ~= Server; |
71 OR4: "[| evs4 \<in> otway; B ~= Server; |
68 Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, |
72 Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, |
69 Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} |
73 Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} |
70 \\<in> set evs4; |
74 \<in> set evs4; |
71 Gets B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} |
75 Gets B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} |
72 \\<in> set evs4 |] |
76 \<in> set evs4 |] |
73 ==> Says B A {|Nonce NA, X|} # evs4 \\<in> otway" |
77 ==> Says B A {|Nonce NA, X|} # evs4 \<in> otway" |
74 |
78 |
75 (*This message models possible leaks of session keys. The nonces |
79 (*This message models possible leaks of session keys. The nonces |
76 identify the protocol run.*) |
80 identify the protocol run.*) |
77 Oops "[| evso \\<in> otway; |
81 Oops: "[| evso \<in> otway; |
78 Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} |
82 Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} |
79 \\<in> set evso |] |
83 \<in> set evso |] |
80 ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \\<in> otway" |
84 ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \<in> otway" |
|
85 |
|
86 |
|
87 declare Says_imp_knows_Spy [THEN analz.Inj, dest] |
|
88 declare parts.Body [dest] |
|
89 declare analz_into_parts [dest] |
|
90 declare Fake_parts_insert_in_Un [dest] |
|
91 |
|
92 (*A "possibility property": there are traces that reach the end*) |
|
93 lemma "B \<noteq> Server |
|
94 ==> \<exists>K. \<exists>NA. \<exists>evs \<in> otway. |
|
95 Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} |
|
96 \<in> set evs" |
|
97 apply (intro exI bexI) |
|
98 apply (rule_tac [2] otway.Nil |
|
99 [THEN otway.OR1, THEN otway.Reception, |
|
100 THEN otway.OR2, THEN otway.Reception, |
|
101 THEN otway.OR3, THEN otway.Reception, THEN otway.OR4]) |
|
102 apply possibility |
|
103 done |
|
104 |
|
105 lemma Gets_imp_Says [dest!]: |
|
106 "[| Gets B X \<in> set evs; evs \<in> otway |] ==> \<exists>A. Says A B X \<in> set evs" |
|
107 apply (erule rev_mp) |
|
108 apply (erule otway.induct) |
|
109 apply auto |
|
110 done |
|
111 |
|
112 |
|
113 (**** Inductive proofs about otway ****) |
|
114 |
|
115 |
|
116 (** For reasoning about the encrypted portion of messages **) |
|
117 |
|
118 lemma OR2_analz_knows_Spy: |
|
119 "[| Gets B {|N, Agent A, Agent B, X|} \<in> set evs; evs \<in> otway |] |
|
120 ==> X \<in> analz (knows Spy evs)" |
|
121 by blast |
|
122 |
|
123 lemma OR4_analz_knows_Spy: |
|
124 "[| Gets B {|N, X, Crypt (shrK B) X'|} \<in> set evs; evs \<in> otway |] |
|
125 ==> X \<in> analz (knows Spy evs)" |
|
126 by blast |
|
127 |
|
128 lemma Oops_parts_knows_Spy: |
|
129 "Says Server B {|NA, X, Crypt K' {|NB,K|}|} \<in> set evs |
|
130 ==> K \<in> parts (knows Spy evs)" |
|
131 by blast |
|
132 |
|
133 (*Forwarding lemma: see comments in OtwayRees.thy*) |
|
134 lemmas OR2_parts_knows_Spy = |
|
135 OR2_analz_knows_Spy [THEN analz_into_parts, standard] |
|
136 |
|
137 |
|
138 (** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY |
|
139 sends messages containing X! **) |
|
140 |
|
141 (*Spy never sees a good agent's shared key!*) |
|
142 lemma Spy_see_shrK [simp]: |
|
143 "evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" |
|
144 apply (erule otway.induct, force, |
|
145 drule_tac [4] OR2_parts_knows_Spy, simp_all) |
|
146 apply blast+ |
|
147 done |
|
148 |
|
149 lemma Spy_analz_shrK [simp]: |
|
150 "evs \<in> otway ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)" |
|
151 by auto |
|
152 |
|
153 lemma Spy_see_shrK_D [dest!]: |
|
154 "[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> otway|] ==> A \<in> bad" |
|
155 by (blast dest: Spy_see_shrK) |
|
156 |
|
157 |
|
158 (*** Proofs involving analz ***) |
|
159 |
|
160 (*Describes the form of K and NA when the Server sends this message. Also |
|
161 for Oops case.*) |
|
162 lemma Says_Server_message_form: |
|
163 "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs; |
|
164 evs \<in> otway |] |
|
165 ==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)" |
|
166 apply (erule rev_mp) |
|
167 apply (erule otway.induct, simp_all) |
|
168 apply blast |
|
169 done |
|
170 |
|
171 |
|
172 (**** |
|
173 The following is to prove theorems of the form |
|
174 |
|
175 Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==> |
|
176 Key K \<in> analz (knows Spy evs) |
|
177 |
|
178 A more general formula must be proved inductively. |
|
179 ****) |
|
180 |
|
181 |
|
182 (** Session keys are not used to encrypt other session keys **) |
|
183 |
|
184 (*The equality makes the induction hypothesis easier to apply*) |
|
185 lemma analz_image_freshK [rule_format]: |
|
186 "evs \<in> otway ==> |
|
187 \<forall>K KK. KK <= -(range shrK) --> |
|
188 (Key K \<in> analz (Key`KK Un (knows Spy evs))) = |
|
189 (K \<in> KK | Key K \<in> analz (knows Spy evs))" |
|
190 apply (erule otway.induct, force) |
|
191 apply (frule_tac [7] Says_Server_message_form) |
|
192 apply (drule_tac [6] OR4_analz_knows_Spy) |
|
193 apply (drule_tac [4] OR2_analz_knows_Spy) |
|
194 apply analz_freshK |
|
195 apply spy_analz |
|
196 done |
|
197 |
|
198 lemma analz_insert_freshK: |
|
199 "[| evs \<in> otway; KAB \<notin> range shrK |] ==> |
|
200 Key K \<in> analz (insert (Key KAB) (knows Spy evs)) = |
|
201 (K = KAB | Key K \<in> analz (knows Spy evs))" |
|
202 by (simp only: analz_image_freshK analz_image_freshK_simps) |
|
203 |
|
204 |
|
205 (*** The Key K uniquely identifies the Server's message. **) |
|
206 |
|
207 lemma unique_session_keys: |
|
208 "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} \<in> set evs; |
|
209 Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \<in> set evs; |
|
210 evs \<in> otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'" |
|
211 apply (erule rev_mp) |
|
212 apply (erule rev_mp) |
|
213 apply (erule otway.induct, simp_all) |
|
214 (*Remaining cases: OR3 and OR4*) |
|
215 apply blast+ |
|
216 done |
|
217 |
|
218 |
|
219 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3 |
|
220 Does not in itself guarantee security: an attack could violate |
|
221 the premises, e.g. by having A=Spy **) |
|
222 |
|
223 lemma secrecy_lemma: |
|
224 "[| A \<notin> bad; B \<notin> bad; evs \<in> otway |] |
|
225 ==> Says Server B |
|
226 {|NA, Crypt (shrK A) {|NA, Key K|}, |
|
227 Crypt (shrK B) {|NB, Key K|}|} \<in> set evs --> |
|
228 Notes Spy {|NA, NB, Key K|} \<notin> set evs --> |
|
229 Key K \<notin> analz (knows Spy evs)" |
|
230 apply (erule otway.induct, force) |
|
231 apply (frule_tac [7] Says_Server_message_form) |
|
232 apply (drule_tac [6] OR4_analz_knows_Spy) |
|
233 apply (drule_tac [4] OR2_analz_knows_Spy) |
|
234 apply (simp_all add: analz_insert_eq analz_insert_freshK pushes) |
|
235 apply spy_analz (*Fake*) |
|
236 (*OR3, OR4, Oops*) |
|
237 apply (blast dest: unique_session_keys)+ |
|
238 done |
|
239 |
|
240 |
|
241 lemma Spy_not_see_encrypted_key: |
|
242 "[| Says Server B |
|
243 {|NA, Crypt (shrK A) {|NA, Key K|}, |
|
244 Crypt (shrK B) {|NB, Key K|}|} \<in> set evs; |
|
245 Notes Spy {|NA, NB, Key K|} \<notin> set evs; |
|
246 A \<notin> bad; B \<notin> bad; evs \<in> otway |] |
|
247 ==> Key K \<notin> analz (knows Spy evs)" |
|
248 by (blast dest: Says_Server_message_form secrecy_lemma) |
|
249 |
|
250 |
|
251 (*** Attempting to prove stronger properties ***) |
|
252 |
|
253 (*Only OR1 can have caused such a part of a message to appear. |
|
254 The premise A \<noteq> B prevents OR2's similar-looking cryptogram from being |
|
255 picked up. Original Otway-Rees doesn't need it.*) |
|
256 lemma Crypt_imp_OR1 [rule_format]: |
|
257 "[| A \<notin> bad; A \<noteq> B; evs \<in> otway |] |
|
258 ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs) --> |
|
259 Says A B {|NA, Agent A, Agent B, |
|
260 Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs" |
|
261 apply (erule otway.induct, force, |
|
262 drule_tac [4] OR2_parts_knows_Spy, simp_all) |
|
263 apply blast+ |
|
264 done |
|
265 |
|
266 |
|
267 (*Crucial property: If the encrypted message appears, and A has used NA |
|
268 to start a run, then it originated with the Server! |
|
269 The premise A \<noteq> B allows use of Crypt_imp_OR1*) |
|
270 (*Only it is FALSE. Somebody could make a fake message to Server |
|
271 substituting some other nonce NA' for NB.*) |
|
272 lemma "[| A \<notin> bad; A \<noteq> B; evs \<in> otway |] |
|
273 ==> Crypt (shrK A) {|NA, Key K|} \<in> parts (knows Spy evs) --> |
|
274 Says A B {|NA, Agent A, Agent B, |
|
275 Crypt (shrK A) {|NA, Agent A, Agent B|}|} |
|
276 \<in> set evs --> |
|
277 (\<exists>B NB. Says Server B |
|
278 {|NA, |
|
279 Crypt (shrK A) {|NA, Key K|}, |
|
280 Crypt (shrK B) {|NB, Key K|}|} \<in> set evs)" |
|
281 apply (erule otway.induct, force, |
|
282 drule_tac [4] OR2_parts_knows_Spy) |
|
283 apply simp_all |
|
284 (*Fake*) |
|
285 apply blast |
|
286 (*OR1: it cannot be a new Nonce, contradiction.*) |
|
287 apply blast |
|
288 (*OR3 and OR4*) |
|
289 apply (simp_all add: ex_disj_distrib) |
|
290 (*OR4*) |
|
291 prefer 2 apply (blast intro!: Crypt_imp_OR1) |
|
292 (*OR3*) |
|
293 apply clarify |
|
294 (*The hypotheses at this point suggest an attack in which nonce NB is used |
|
295 in two different roles: |
|
296 Gets Server |
|
297 {|Nonce NA, Agent Aa, Agent A, |
|
298 Crypt (shrK Aa) {|Nonce NA, Agent Aa, Agent A|}, Nonce NB, |
|
299 Crypt (shrK A) {|Nonce NA, Agent Aa, Agent A|}|} |
|
300 \<in> set evs3 |
|
301 Says A B |
|
302 {|Nonce NB, Agent A, Agent B, |
|
303 Crypt (shrK A) {|Nonce NB, Agent A, Agent B|}|} |
|
304 \<in> set evs3; |
|
305 *) |
|
306 |
|
307 |
|
308 (*Thus the key property A_can_trust probably fails too.*) |
|
309 oops |
81 |
310 |
82 end |
311 end |