3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1996 University of Cambridge |
4 Copyright 1996 University of Cambridge |
5 |
5 |
6 Inductive relation "yahalom" for the Yahalom protocol. |
6 Inductive relation "yahalom" for the Yahalom protocol. |
7 |
7 |
8 Example of why Oops is necessary. This protocol can be attacked because it |
8 Demonstrates of why Oops is necessary. This protocol can be attacked because |
9 doesn't keep NB secret, but without Oops it can be "verified" anyway. |
9 it doesn't keep NB secret, but without Oops it can be "verified" anyway. |
|
10 The issues are discussed in lcp's LICS 2000 invited lecture. |
10 *) |
11 *) |
11 |
12 |
12 Yahalom_Bad = Shared + |
13 theory Yahalom_Bad = Shared: |
13 |
14 |
14 consts yahalom :: event list set |
15 consts yahalom :: "event list set" |
15 inductive "yahalom" |
16 inductive "yahalom" |
16 intrs |
17 intros |
17 (*Initial trace is empty*) |
18 (*Initial trace is empty*) |
18 Nil "[] : yahalom" |
19 Nil: "[] \<in> yahalom" |
19 |
20 |
20 (*The spy MAY say anything he CAN say. We do not expect him to |
21 (*The spy MAY say anything he CAN say. We do not expect him to |
21 invent new nonces here, but he can also use NS1. Common to |
22 invent new nonces here, but he can also use NS1. Common to |
22 all similar protocols.*) |
23 all similar protocols.*) |
23 Fake "[| evsf \\<in> yahalom; X \\<in> synth (analz (knows Spy evsf)) |] |
24 Fake: "[| evsf \<in> yahalom; X \<in> synth (analz (knows Spy evsf)) |] |
24 ==> Says Spy B X # evsf \\<in> yahalom" |
25 ==> Says Spy B X # evsf \<in> yahalom" |
25 |
26 |
26 (*A message that has been sent can be received by the |
27 (*A message that has been sent can be received by the |
27 intended recipient.*) |
28 intended recipient.*) |
28 Reception "[| evsr \\<in> yahalom; Says A B X \\<in> set evsr |] |
29 Reception: "[| evsr \<in> yahalom; Says A B X \<in> set evsr |] |
29 ==> Gets B X # evsr \\<in> yahalom" |
30 ==> Gets B X # evsr \<in> yahalom" |
30 |
31 |
31 (*Alice initiates a protocol run*) |
32 (*Alice initiates a protocol run*) |
32 YM1 "[| evs1 \\<in> yahalom; Nonce NA \\<notin> used evs1 |] |
33 YM1: "[| evs1 \<in> yahalom; Nonce NA \<notin> used evs1 |] |
33 ==> Says A B {|Agent A, Nonce NA|} # evs1 \\<in> yahalom" |
34 ==> Says A B {|Agent A, Nonce NA|} # evs1 \<in> yahalom" |
34 |
35 |
35 (*Bob's response to Alice's message.*) |
36 (*Bob's response to Alice's message.*) |
36 YM2 "[| evs2 \\<in> yahalom; Nonce NB \\<notin> used evs2; |
37 YM2: "[| evs2 \<in> yahalom; Nonce NB \<notin> used evs2; |
37 Gets B {|Agent A, Nonce NA|} \\<in> set evs2 |] |
38 Gets B {|Agent A, Nonce NA|} \<in> set evs2 |] |
38 ==> Says B Server |
39 ==> Says B Server |
39 {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} |
40 {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} |
40 # evs2 \\<in> yahalom" |
41 # evs2 \<in> yahalom" |
41 |
42 |
42 (*The Server receives Bob's message. He responds by sending a |
43 (*The Server receives Bob's message. He responds by sending a |
43 new session key to Alice, with a packet for forwarding to Bob.*) |
44 new session key to Alice, with a packet for forwarding to Bob.*) |
44 YM3 "[| evs3 \\<in> yahalom; Key KAB \\<notin> used evs3; |
45 YM3: "[| evs3 \<in> yahalom; Key KAB \<notin> used evs3; |
45 Gets Server |
46 Gets Server |
46 {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} |
47 {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} |
47 \\<in> set evs3 |] |
48 \<in> set evs3 |] |
48 ==> Says Server A |
49 ==> Says Server A |
49 {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|}, |
50 {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|}, |
50 Crypt (shrK B) {|Agent A, Key KAB|}|} |
51 Crypt (shrK B) {|Agent A, Key KAB|}|} |
51 # evs3 \\<in> yahalom" |
52 # evs3 \<in> yahalom" |
52 |
53 |
53 (*Alice receives the Server's (?) message, checks her Nonce, and |
54 (*Alice receives the Server's (?) message, checks her Nonce, and |
54 uses the new session key to send Bob his Nonce. The premise |
55 uses the new session key to send Bob his Nonce. The premise |
55 A \\<noteq> Server is needed to prove Says_Server_not_range.*) |
56 A \<noteq> Server is needed to prove Says_Server_not_range.*) |
56 YM4 "[| evs4 \\<in> yahalom; A \\<noteq> Server; |
57 YM4: "[| evs4 \<in> yahalom; A \<noteq> Server; |
57 Gets A {|Crypt(shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, X|} |
58 Gets A {|Crypt(shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, X|} |
58 \\<in> set evs4; |
59 \<in> set evs4; |
59 Says A B {|Agent A, Nonce NA|} \\<in> set evs4 |] |
60 Says A B {|Agent A, Nonce NA|} \<in> set evs4 |] |
60 ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 \\<in> yahalom" |
61 ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 \<in> yahalom" |
61 |
62 |
62 (*This message models possible leaks of session keys. The Nonces |
63 |
63 identify the protocol run. Quoting Server here ensures they are |
64 declare Says_imp_knows_Spy [THEN analz.Inj, dest] |
64 correct.*) |
65 declare parts.Body [dest] |
|
66 declare Fake_parts_insert_in_Un [dest] |
|
67 declare analz_into_parts [dest] |
|
68 |
|
69 |
|
70 (*A "possibility property": there are traces that reach the end*) |
|
71 lemma "A \<noteq> Server |
|
72 ==> \<exists>X NB K. \<exists>evs \<in> yahalom. |
|
73 Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs" |
|
74 apply (intro exI bexI) |
|
75 apply (rule_tac [2] yahalom.Nil |
|
76 [THEN yahalom.YM1, THEN yahalom.Reception, |
|
77 THEN yahalom.YM2, THEN yahalom.Reception, |
|
78 THEN yahalom.YM3, THEN yahalom.Reception, |
|
79 THEN yahalom.YM4]) |
|
80 apply possibility |
|
81 done |
|
82 |
|
83 lemma Gets_imp_Says: |
|
84 "[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> \<exists>A. Says A B X \<in> set evs" |
|
85 by (erule rev_mp, erule yahalom.induct, auto) |
|
86 |
|
87 (*Must be proved separately for each protocol*) |
|
88 lemma Gets_imp_knows_Spy: |
|
89 "[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> X \<in> knows Spy evs" |
|
90 by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) |
|
91 |
|
92 declare Gets_imp_knows_Spy [THEN analz.Inj, dest] |
|
93 |
|
94 |
|
95 (**** Inductive proofs about yahalom ****) |
|
96 |
|
97 (** For reasoning about the encrypted portion of messages **) |
|
98 |
|
99 (*Lets us treat YM4 using a similar argument as for the Fake case.*) |
|
100 lemma YM4_analz_knows_Spy: |
|
101 "[| Gets A {|Crypt (shrK A) Y, X|} \<in> set evs; evs \<in> yahalom |] |
|
102 ==> X \<in> analz (knows Spy evs)" |
|
103 by blast |
|
104 |
|
105 lemmas YM4_parts_knows_Spy = |
|
106 YM4_analz_knows_Spy [THEN analz_into_parts, standard] |
|
107 |
|
108 |
|
109 (** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY |
|
110 sends messages containing X! **) |
|
111 |
|
112 (*Spy never sees a good agent's shared key!*) |
|
113 lemma Spy_see_shrK [simp]: |
|
114 "evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" |
|
115 apply (erule yahalom.induct, force, |
|
116 drule_tac [6] YM4_parts_knows_Spy, simp_all) |
|
117 apply blast+ |
|
118 done |
|
119 |
|
120 lemma Spy_analz_shrK [simp]: |
|
121 "evs \<in> yahalom ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)" |
|
122 by auto |
|
123 |
|
124 lemma Spy_see_shrK_D [dest!]: |
|
125 "[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> yahalom|] ==> A \<in> bad" |
|
126 by (blast dest: Spy_see_shrK) |
|
127 |
|
128 (*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*) |
|
129 lemma new_keys_not_used [rule_format, simp]: |
|
130 "evs \<in> yahalom ==> Key K \<notin> used evs --> K \<notin> keysFor (parts (knows Spy evs))" |
|
131 apply (erule yahalom.induct, force, |
|
132 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
|
133 (*Fake, YM3, YM4*) |
|
134 apply (blast dest!: keysFor_parts_insert)+ |
|
135 done |
|
136 |
|
137 |
|
138 (**** |
|
139 The following is to prove theorems of the form |
|
140 |
|
141 Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==> |
|
142 Key K \<in> analz (knows Spy evs) |
|
143 |
|
144 A more general formula must be proved inductively. |
|
145 ****) |
|
146 |
|
147 (** Session keys are not used to encrypt other session keys **) |
|
148 |
|
149 lemma analz_image_freshK [rule_format]: |
|
150 "evs \<in> yahalom ==> |
|
151 \<forall>K KK. KK <= - (range shrK) --> |
|
152 (Key K \<in> analz (Key`KK Un (knows Spy evs))) = |
|
153 (K \<in> KK | Key K \<in> analz (knows Spy evs))" |
|
154 apply (erule yahalom.induct, force, |
|
155 drule_tac [6] YM4_analz_knows_Spy) |
|
156 apply analz_freshK |
|
157 apply spy_analz |
|
158 done |
|
159 |
|
160 lemma analz_insert_freshK: "[| evs \<in> yahalom; KAB \<notin> range shrK |] ==> |
|
161 Key K \<in> analz (insert (Key KAB) (knows Spy evs)) = |
|
162 (K = KAB | Key K \<in> analz (knows Spy evs))" |
|
163 by (simp only: analz_image_freshK analz_image_freshK_simps) |
|
164 |
|
165 |
|
166 (*** The Key K uniquely identifies the Server's message. **) |
|
167 |
|
168 lemma unique_session_keys: |
|
169 "[| Says Server A |
|
170 {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \<in> set evs; |
|
171 Says Server A' |
|
172 {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} \<in> set evs; |
|
173 evs \<in> yahalom |] |
|
174 ==> A=A' & B=B' & na=na' & nb=nb'" |
|
175 apply (erule rev_mp, erule rev_mp) |
|
176 apply (erule yahalom.induct, simp_all) |
|
177 (*YM3, by freshness, and YM4*) |
|
178 apply blast+ |
|
179 done |
|
180 |
|
181 |
|
182 (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **) |
|
183 |
|
184 lemma secrecy_lemma: |
|
185 "[| A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
|
186 ==> Says Server A |
|
187 {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, |
|
188 Crypt (shrK B) {|Agent A, Key K|}|} |
|
189 \<in> set evs --> |
|
190 Key K \<notin> analz (knows Spy evs)" |
|
191 apply (erule yahalom.induct, force, drule_tac [6] YM4_analz_knows_Spy) |
|
192 apply (simp_all add: pushes analz_insert_eq analz_insert_freshK) |
|
193 apply spy_analz (*Fake*) |
|
194 apply (blast dest: unique_session_keys) (*YM3*) |
|
195 done |
|
196 |
|
197 (*Final version*) |
|
198 lemma Spy_not_see_encrypted_key: |
|
199 "[| Says Server A |
|
200 {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, |
|
201 Crypt (shrK B) {|Agent A, Key K|}|} |
|
202 \<in> set evs; |
|
203 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
|
204 ==> Key K \<notin> analz (knows Spy evs)" |
|
205 by (blast dest: secrecy_lemma) |
|
206 |
|
207 |
|
208 (** Security Guarantee for A upon receiving YM3 **) |
|
209 |
|
210 (*If the encrypted message appears then it originated with the Server*) |
|
211 lemma A_trusts_YM3: |
|
212 "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs); |
|
213 A \<notin> bad; evs \<in> yahalom |] |
|
214 ==> Says Server A |
|
215 {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, |
|
216 Crypt (shrK B) {|Agent A, Key K|}|} |
|
217 \<in> set evs" |
|
218 apply (erule rev_mp) |
|
219 apply (erule yahalom.induct, force, |
|
220 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
|
221 (*Fake, YM3*) |
|
222 apply blast+ |
|
223 done |
|
224 |
|
225 (*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*) |
|
226 lemma A_gets_good_key: |
|
227 "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs); |
|
228 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
|
229 ==> Key K \<notin> analz (knows Spy evs)" |
|
230 by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key) |
|
231 |
|
232 (** Security Guarantees for B upon receiving YM4 **) |
|
233 |
|
234 (*B knows, by the first part of A's message, that the Server distributed |
|
235 the key for A and B. But this part says nothing about nonces.*) |
|
236 lemma B_trusts_YM4_shrK: |
|
237 "[| Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs); |
|
238 B \<notin> bad; evs \<in> yahalom |] |
|
239 ==> \<exists>NA NB. Says Server A |
|
240 {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, |
|
241 Crypt (shrK B) {|Agent A, Key K|}|} |
|
242 \<in> set evs" |
|
243 apply (erule rev_mp) |
|
244 apply (erule yahalom.induct, force, |
|
245 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
|
246 (*Fake, YM3*) |
|
247 apply blast+ |
|
248 done |
|
249 |
|
250 (** Up to now, the reasoning is similar to standard Yahalom. Now the |
|
251 doubtful reasoning occurs. We should not be assuming that an unknown |
|
252 key is secure, but the model allows us to: there is no Oops rule to |
|
253 let session keys become compromised.*) |
|
254 |
|
255 (*B knows, by the second part of A's message, that the Server distributed |
|
256 the key quoting nonce NB. This part says nothing about agent names. |
|
257 Secrecy of K is assumed; the valid Yahalom proof uses (and later proves) |
|
258 the secrecy of NB.*) |
|
259 lemma B_trusts_YM4_newK [rule_format]: |
|
260 "[|Key K \<notin> analz (knows Spy evs); evs \<in> yahalom|] |
|
261 ==> Crypt K (Nonce NB) \<in> parts (knows Spy evs) --> |
|
262 (\<exists>A B NA. Says Server A |
|
263 {|Crypt (shrK A) {|Agent B, Key K, |
|
264 Nonce NA, Nonce NB|}, |
|
265 Crypt (shrK B) {|Agent A, Key K|}|} |
|
266 \<in> set evs)" |
|
267 apply (erule rev_mp) |
|
268 apply (erule yahalom.induct, force, |
|
269 frule_tac [6] YM4_parts_knows_Spy) |
|
270 apply (analz_mono_contra, simp_all) |
|
271 (*Fake*) |
|
272 apply blast |
|
273 (*YM3*) |
|
274 apply blast |
|
275 (*A is uncompromised because NB is secure |
|
276 A's certificate guarantees the existence of the Server message*) |
|
277 apply (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad |
|
278 dest: Says_imp_spies |
|
279 parts.Inj [THEN parts.Fst, THEN A_trusts_YM3]) |
|
280 done |
|
281 |
|
282 |
|
283 (*B's session key guarantee from YM4. The two certificates contribute to a |
|
284 single conclusion about the Server's message. *) |
|
285 lemma B_trusts_YM4: |
|
286 "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, |
|
287 Crypt K (Nonce NB)|} \<in> set evs; |
|
288 Says B Server |
|
289 {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} |
|
290 \<in> set evs; |
|
291 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
|
292 ==> \<exists>na nb. Says Server A |
|
293 {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, |
|
294 Crypt (shrK B) {|Agent A, Key K|}|} |
|
295 \<in> set evs" |
|
296 by (blast dest: B_trusts_YM4_newK B_trusts_YM4_shrK Spy_not_see_encrypted_key |
|
297 unique_session_keys) |
|
298 |
|
299 |
|
300 (*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*) |
|
301 lemma B_gets_good_key: |
|
302 "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, |
|
303 Crypt K (Nonce NB)|} \<in> set evs; |
|
304 Says B Server |
|
305 {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} |
|
306 \<in> set evs; |
|
307 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
|
308 ==> Key K \<notin> analz (knows Spy evs)" |
|
309 by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key) |
|
310 |
|
311 |
|
312 (*** Authenticating B to A: these proofs are not considered. |
|
313 They are irrelevant to showing the need for Oops. ***) |
|
314 |
|
315 |
|
316 (*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***) |
|
317 |
|
318 (*Assuming the session key is secure, if both certificates are present then |
|
319 A has said NB. We can't be sure about the rest of A's message, but only |
|
320 NB matters for freshness.*) |
|
321 lemma A_Said_YM3_lemma [rule_format]: |
|
322 "evs \<in> yahalom |
|
323 ==> Key K \<notin> analz (knows Spy evs) --> |
|
324 Crypt K (Nonce NB) \<in> parts (knows Spy evs) --> |
|
325 Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs) --> |
|
326 B \<notin> bad --> |
|
327 (\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs)" |
|
328 apply (erule yahalom.induct, force, |
|
329 frule_tac [6] YM4_parts_knows_Spy) |
|
330 apply (analz_mono_contra, simp_all) |
|
331 (*Fake*) |
|
332 apply blast |
|
333 (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*) |
|
334 apply (force dest!: Crypt_imp_keysFor) |
|
335 (*YM4: was Crypt K (Nonce NB) the very last message? If not, use ind. hyp.*) |
|
336 apply (simp add: ex_disj_distrib) |
|
337 (*yes: apply unicity of session keys*) |
|
338 apply (blast dest!: Gets_imp_Says A_trusts_YM3 B_trusts_YM4_shrK |
|
339 Crypt_Spy_analz_bad |
|
340 dest: Says_imp_knows_Spy [THEN parts.Inj] unique_session_keys) |
|
341 done |
|
342 |
|
343 (*If B receives YM4 then A has used nonce NB (and therefore is alive). |
|
344 Moreover, A associates K with NB (thus is talking about the same run). |
|
345 Other premises guarantee secrecy of K.*) |
|
346 lemma YM4_imp_A_Said_YM3 [rule_format]: |
|
347 "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, |
|
348 Crypt K (Nonce NB)|} \<in> set evs; |
|
349 Says B Server |
|
350 {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} |
|
351 \<in> set evs; |
|
352 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
|
353 ==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs" |
|
354 apply (blast intro!: A_Said_YM3_lemma |
|
355 dest: Spy_not_see_encrypted_key B_trusts_YM4 Gets_imp_Says) |
|
356 done |
65 |
357 |
66 end |
358 end |