1 (* Title: HOL/Auth/Yahalom2 |
1 (* Title: HOL/Auth/Yahalom2 |
2 ID: $Id$ |
2 ID: $Id$ |
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 |
|
7 header{*The Yahalom Protocol, Variant 2*} |
|
8 |
|
9 theory Yahalom2 = Public: |
|
10 |
|
11 text{* |
6 This version trades encryption of NB for additional explicitness in YM3. |
12 This version trades encryption of NB for additional explicitness in YM3. |
7 Also in YM3, care is taken to make the two certificates distinct. |
13 Also in YM3, care is taken to make the two certificates distinct. |
8 |
14 |
9 From page 259 of |
15 From page 259 of |
10 Burrows, Abadi and Needham. A Logic of Authentication. |
16 Burrows, Abadi and Needham (1989). A Logic of Authentication. |
11 Proc. Royal Soc. 426 (1989) |
17 Proc. Royal Soc. 426 |
12 *) |
18 |
13 |
19 This theory has the prototypical example of a secrecy relation, KeyCryptNonce. |
14 header{*The Yahalom Protocol, Variant 2*} |
20 *} |
15 |
|
16 theory Yahalom2 = Shared: |
|
17 |
21 |
18 consts yahalom :: "event list set" |
22 consts yahalom :: "event list set" |
19 inductive "yahalom" |
23 inductive "yahalom" |
20 intros |
24 intros |
21 (*Initial trace is empty*) |
25 (*Initial trace is empty*) |
87 apply (rule_tac [2] yahalom.Nil |
91 apply (rule_tac [2] yahalom.Nil |
88 [THEN yahalom.YM1, THEN yahalom.Reception, |
92 [THEN yahalom.YM1, THEN yahalom.Reception, |
89 THEN yahalom.YM2, THEN yahalom.Reception, |
93 THEN yahalom.YM2, THEN yahalom.Reception, |
90 THEN yahalom.YM3, THEN yahalom.Reception, |
94 THEN yahalom.YM3, THEN yahalom.Reception, |
91 THEN yahalom.YM4]) |
95 THEN yahalom.YM4]) |
92 apply (possibility, simp add: used_Cons) |
96 apply (possibility, simp add: used_Cons) |
93 done |
97 done |
94 |
98 |
95 lemma Gets_imp_Says: |
99 lemma Gets_imp_Says: |
96 "[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> \<exists>A. Says A B X \<in> set evs" |
100 "[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> \<exists>A. Says A B X \<in> set evs" |
97 by (erule rev_mp, erule yahalom.induct, auto) |
101 by (erule rev_mp, erule yahalom.induct, auto) |
132 |
136 |
133 lemma Spy_see_shrK_D [dest!]: |
137 lemma Spy_see_shrK_D [dest!]: |
134 "[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> yahalom|] ==> A \<in> bad" |
138 "[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> yahalom|] ==> A \<in> bad" |
135 by (blast dest: Spy_see_shrK) |
139 by (blast dest: Spy_see_shrK) |
136 |
140 |
137 (*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*) |
141 text{*Nobody can have used non-existent keys! |
138 lemma new_keys_not_used [rule_format, simp]: |
142 Needed to apply @{text analz_insert_Key}*} |
139 "evs \<in> yahalom ==> Key K \<notin> used evs --> K \<notin> keysFor (parts (knows Spy evs))" |
143 lemma new_keys_not_used [simp]: |
|
144 "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> yahalom|] |
|
145 ==> K \<notin> keysFor (parts (spies evs))" |
|
146 apply (erule rev_mp) |
140 apply (erule yahalom.induct, force, |
147 apply (erule yahalom.induct, force, |
141 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
148 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
142 txt{*Fake*} |
149 txt{*Fake*} |
143 apply (force dest!: keysFor_parts_insert) |
150 apply (force dest!: keysFor_parts_insert) |
144 txt{*YM3, YM4*} |
151 txt{*YM3*} |
145 apply blast+ |
152 apply blast |
146 done |
153 txt{*YM4*} |
147 |
154 apply auto |
148 |
155 apply (blast dest!: Gets_imp_knows_Spy [THEN parts.Inj]) |
149 (*Describes the form of K when the Server sends this message. Useful for |
156 done |
150 Oops as well as main secrecy property.*) |
157 |
|
158 |
|
159 text{*Describes the form of K when the Server sends this message. Useful for |
|
160 Oops as well as main secrecy property.*} |
151 lemma Says_Server_message_form: |
161 lemma Says_Server_message_form: |
152 "[| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|} |
162 "[| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|} |
153 \<in> set evs; evs \<in> yahalom |] |
163 \<in> set evs; evs \<in> yahalom |] |
154 ==> K \<notin> range shrK" |
164 ==> K \<notin> range shrK" |
155 by (erule rev_mp, erule yahalom.induct, simp_all) |
165 by (erule rev_mp, erule yahalom.induct, simp_all) |
169 lemma analz_image_freshK [rule_format]: |
179 lemma analz_image_freshK [rule_format]: |
170 "evs \<in> yahalom ==> |
180 "evs \<in> yahalom ==> |
171 \<forall>K KK. KK <= - (range shrK) --> |
181 \<forall>K KK. KK <= - (range shrK) --> |
172 (Key K \<in> analz (Key`KK Un (knows Spy evs))) = |
182 (Key K \<in> analz (Key`KK Un (knows Spy evs))) = |
173 (K \<in> KK | Key K \<in> analz (knows Spy evs))" |
183 (K \<in> KK | Key K \<in> analz (knows Spy evs))" |
174 apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form, |
184 apply (erule yahalom.induct) |
175 drule_tac [6] YM4_analz_knows_Spy, analz_freshK, spy_analz) |
185 apply (frule_tac [8] Says_Server_message_form) |
|
186 apply (drule_tac [7] YM4_analz_knows_Spy, analz_freshK, spy_analz, blast) |
176 done |
187 done |
177 |
188 |
178 lemma analz_insert_freshK: |
189 lemma analz_insert_freshK: |
179 "[| evs \<in> yahalom; KAB \<notin> range shrK |] ==> |
190 "[| evs \<in> yahalom; KAB \<notin> range shrK |] ==> |
180 (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = |
191 (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = |
212 apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz) |
223 apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz) |
213 apply (blast dest: unique_session_keys)+ (*YM3, Oops*) |
224 apply (blast dest: unique_session_keys)+ (*YM3, Oops*) |
214 done |
225 done |
215 |
226 |
216 |
227 |
217 (*Final version*) |
228 text{*Final version*} |
218 lemma Spy_not_see_encrypted_key: |
229 lemma Spy_not_see_encrypted_key: |
219 "[| Says Server A |
230 "[| Says Server A |
220 {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, |
231 {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, |
221 Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} |
232 Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} |
222 \<in> set evs; |
233 \<in> set evs; |
225 ==> Key K \<notin> analz (knows Spy evs)" |
236 ==> Key K \<notin> analz (knows Spy evs)" |
226 by (blast dest: secrecy_lemma Says_Server_message_form) |
237 by (blast dest: secrecy_lemma Says_Server_message_form) |
227 |
238 |
228 |
239 |
229 |
240 |
230 text{*This form is an immediate consequence of the previous result. It is |
241 text{*This form is an immediate consequence of the previous result. It is |
231 similar to the assertions established by other methods. It is equivalent |
242 similar to the assertions established by other methods. It is equivalent |
232 to the previous result in that the Spy already has @{term analz} and |
243 to the previous result in that the Spy already has @{term analz} and |
233 @{term synth} at his disposal. However, the conclusion |
244 @{term synth} at his disposal. However, the conclusion |
234 @{term "Key K \<notin> knows Spy evs"} appears not to be inductive: all the cases |
245 @{term "Key K \<notin> knows Spy evs"} appears not to be inductive: all the cases |
235 other than Fake are trivial, while Fake requires |
246 other than Fake are trivial, while Fake requires |
236 @{term "Key K \<notin> analz (knows Spy evs)"}. *} |
247 @{term "Key K \<notin> analz (knows Spy evs)"}. *} |
237 lemma Spy_not_know_encrypted_key: |
248 lemma Spy_not_know_encrypted_key: |
238 "[| Says Server A |
249 "[| Says Server A |
239 {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, |
250 {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, |
240 Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} |
251 Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} |
245 by (blast dest: Spy_not_see_encrypted_key) |
256 by (blast dest: Spy_not_see_encrypted_key) |
246 |
257 |
247 |
258 |
248 subsection{*Security Guarantee for A upon receiving YM3*} |
259 subsection{*Security Guarantee for A upon receiving YM3*} |
249 |
260 |
250 (*If the encrypted message appears then it originated with the Server. |
261 text{*If the encrypted message appears then it originated with the Server. |
251 May now apply Spy_not_see_encrypted_key, subject to its conditions.*) |
262 May now apply @{text Spy_not_see_encrypted_key}, subject to its conditions.*} |
252 lemma A_trusts_YM3: |
263 lemma A_trusts_YM3: |
253 "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> parts (knows Spy evs); |
264 "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> parts (knows Spy evs); |
254 A \<notin> bad; evs \<in> yahalom |] |
265 A \<notin> bad; evs \<in> yahalom |] |
255 ==> \<exists>nb. Says Server A |
266 ==> \<exists>nb. Says Server A |
256 {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, |
267 {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, |
261 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
272 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
262 txt{*Fake, YM3*} |
273 txt{*Fake, YM3*} |
263 apply blast+ |
274 apply blast+ |
264 done |
275 done |
265 |
276 |
266 (*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*) |
277 text{*The obvious combination of @{text A_trusts_YM3} with |
|
278 @{text Spy_not_see_encrypted_key}*} |
267 theorem A_gets_good_key: |
279 theorem A_gets_good_key: |
268 "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> parts (knows Spy evs); |
280 "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> parts (knows Spy evs); |
269 \<forall>nb. Notes Spy {|na, nb, Key K|} \<notin> set evs; |
281 \<forall>nb. Notes Spy {|na, nb, Key K|} \<notin> set evs; |
270 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
282 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
271 ==> Key K \<notin> analz (knows Spy evs)" |
283 ==> Key K \<notin> analz (knows Spy evs)" |
272 by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key) |
284 by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key) |
273 |
285 |
274 |
286 |
275 subsection{*Security Guarantee for B upon receiving YM4*} |
287 subsection{*Security Guarantee for B upon receiving YM4*} |
276 |
288 |
277 (*B knows, by the first part of A's message, that the Server distributed |
289 text{*B knows, by the first part of A's message, that the Server distributed |
278 the key for A and B, and has associated it with NB.*) |
290 the key for A and B, and has associated it with NB.*} |
279 lemma B_trusts_YM4_shrK: |
291 lemma B_trusts_YM4_shrK: |
280 "[| Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|} |
292 "[| Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|} |
281 \<in> parts (knows Spy evs); |
293 \<in> parts (knows Spy evs); |
282 B \<notin> bad; evs \<in> yahalom |] |
294 B \<notin> bad; evs \<in> yahalom |] |
283 ==> \<exists>NA. Says Server A |
295 ==> \<exists>NA. Says Server A |
286 Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|} |
298 Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|} |
287 \<in> set evs" |
299 \<in> set evs" |
288 apply (erule rev_mp) |
300 apply (erule rev_mp) |
289 apply (erule yahalom.induct, force, |
301 apply (erule yahalom.induct, force, |
290 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
302 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
291 (*Fake, YM3*) |
303 txt{*Fake, YM3*} |
292 apply blast+ |
304 apply blast+ |
293 done |
305 done |
294 |
306 |
295 |
307 |
296 (*With this protocol variant, we don't need the 2nd part of YM4 at all: |
308 text{*With this protocol variant, we don't need the 2nd part of YM4 at all: |
297 Nonce NB is available in the first part.*) |
309 Nonce NB is available in the first part.*} |
298 |
310 |
299 (*What can B deduce from receipt of YM4? Stronger and simpler than Yahalom |
311 text{*What can B deduce from receipt of YM4? Stronger and simpler than Yahalom |
300 because we do not have to show that NB is secret. *) |
312 because we do not have to show that NB is secret. *} |
301 lemma B_trusts_YM4: |
313 lemma B_trusts_YM4: |
302 "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, X|} |
314 "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, X|} |
303 \<in> set evs; |
315 \<in> set evs; |
304 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
316 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
305 ==> \<exists>NA. Says Server A |
317 ==> \<exists>NA. Says Server A |
308 Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|} |
320 Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|} |
309 \<in> set evs" |
321 \<in> set evs" |
310 by (blast dest!: B_trusts_YM4_shrK) |
322 by (blast dest!: B_trusts_YM4_shrK) |
311 |
323 |
312 |
324 |
313 (*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*) |
325 text{*The obvious combination of @{text B_trusts_YM4} with |
|
326 @{text Spy_not_see_encrypted_key}*} |
314 theorem B_gets_good_key: |
327 theorem B_gets_good_key: |
315 "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, X|} |
328 "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, X|} |
316 \<in> set evs; |
329 \<in> set evs; |
317 \<forall>na. Notes Spy {|na, Nonce NB, Key K|} \<notin> set evs; |
330 \<forall>na. Notes Spy {|na, Nonce NB, Key K|} \<notin> set evs; |
318 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
331 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
320 by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key) |
333 by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key) |
321 |
334 |
322 |
335 |
323 subsection{*Authenticating B to A*} |
336 subsection{*Authenticating B to A*} |
324 |
337 |
325 (*The encryption in message YM2 tells us it cannot be faked.*) |
338 text{*The encryption in message YM2 tells us it cannot be faked.*} |
326 lemma B_Said_YM2: |
339 lemma B_Said_YM2: |
327 "[| Crypt (shrK B) {|Agent A, Nonce NA|} \<in> parts (knows Spy evs); |
340 "[| Crypt (shrK B) {|Agent A, Nonce NA|} \<in> parts (knows Spy evs); |
328 B \<notin> bad; evs \<in> yahalom |] |
341 B \<notin> bad; evs \<in> yahalom |] |
329 ==> \<exists>NB. Says B Server {|Agent B, Nonce NB, |
342 ==> \<exists>NB. Says B Server {|Agent B, Nonce NB, |
330 Crypt (shrK B) {|Agent A, Nonce NA|}|} |
343 Crypt (shrK B) {|Agent A, Nonce NA|}|} |
331 \<in> set evs" |
344 \<in> set evs" |
332 apply (erule rev_mp) |
345 apply (erule rev_mp) |
333 apply (erule yahalom.induct, force, |
346 apply (erule yahalom.induct, force, |
334 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
347 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
335 (*Fake, YM2*) |
348 txt{*Fake, YM2*} |
336 apply blast+ |
349 apply blast+ |
337 done |
350 done |
338 |
351 |
339 |
352 |
340 (*If the server sends YM3 then B sent YM2, perhaps with a different NB*) |
353 text{*If the server sends YM3 then B sent YM2, perhaps with a different NB*} |
341 lemma YM3_auth_B_to_A_lemma: |
354 lemma YM3_auth_B_to_A_lemma: |
342 "[| Says Server A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} |
355 "[| Says Server A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} |
343 \<in> set evs; |
356 \<in> set evs; |
344 B \<notin> bad; evs \<in> yahalom |] |
357 B \<notin> bad; evs \<in> yahalom |] |
345 ==> \<exists>nb'. Says B Server {|Agent B, nb', |
358 ==> \<exists>nb'. Says B Server {|Agent B, nb', |
346 Crypt (shrK B) {|Agent A, Nonce NA|}|} |
359 Crypt (shrK B) {|Agent A, Nonce NA|}|} |
347 \<in> set evs" |
360 \<in> set evs" |
348 apply (erule rev_mp) |
361 apply (erule rev_mp) |
349 apply (erule yahalom.induct, simp_all) |
362 apply (erule yahalom.induct, simp_all) |
350 (*Fake, YM2, YM3*) |
363 txt{*Fake, YM2, YM3*} |
351 apply (blast dest!: B_Said_YM2)+ |
364 apply (blast dest!: B_Said_YM2)+ |
352 done |
365 done |
353 |
366 |
354 text{*If A receives YM3 then B has used nonce NA (and therefore is alive)*} |
367 text{*If A receives YM3 then B has used nonce NA (and therefore is alive)*} |
355 theorem YM3_auth_B_to_A: |
368 theorem YM3_auth_B_to_A: |
364 |
377 |
365 subsection{*Authenticating A to B*} |
378 subsection{*Authenticating A to B*} |
366 |
379 |
367 text{*using the certificate @{term "Crypt K (Nonce NB)"}*} |
380 text{*using the certificate @{term "Crypt K (Nonce NB)"}*} |
368 |
381 |
369 (*Assuming the session key is secure, if both certificates are present then |
382 text{*Assuming the session key is secure, if both certificates are present then |
370 A has said NB. We can't be sure about the rest of A's message, but only |
383 A has said NB. We can't be sure about the rest of A's message, but only |
371 NB matters for freshness. Note that Key K \<notin> analz (knows Spy evs) must be |
384 NB matters for freshness. Note that @{term "Key K \<notin> analz (knows Spy evs)"} |
372 the FIRST antecedent of the induction formula.*) |
385 must be the FIRST antecedent of the induction formula.*} |
373 |
386 |
374 (*This lemma allows a use of unique_session_keys in the next proof, |
387 text{*This lemma allows a use of @{text unique_session_keys} in the next proof, |
375 which otherwise is extremely slow.*) |
388 which otherwise is extremely slow.*} |
376 lemma secure_unique_session_keys: |
389 lemma secure_unique_session_keys: |
377 "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> analz (spies evs); |
390 "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> analz (spies evs); |
378 Crypt (shrK A') {|Agent B', Key K, na'|} \<in> analz (spies evs); |
391 Crypt (shrK A') {|Agent B', Key K, na'|} \<in> analz (spies evs); |
379 Key K \<notin> analz (knows Spy evs); evs \<in> yahalom |] |
392 Key K \<notin> analz (knows Spy evs); evs \<in> yahalom |] |
380 ==> A=A' & B=B'" |
393 ==> A=A' & B=B'" |
382 |
395 |
383 |
396 |
384 lemma Auth_A_to_B_lemma [rule_format]: |
397 lemma Auth_A_to_B_lemma [rule_format]: |
385 "evs \<in> yahalom |
398 "evs \<in> yahalom |
386 ==> Key K \<notin> analz (knows Spy evs) --> |
399 ==> Key K \<notin> analz (knows Spy evs) --> |
|
400 K \<in> symKeys --> |
387 Crypt K (Nonce NB) \<in> parts (knows Spy evs) --> |
401 Crypt K (Nonce NB) \<in> parts (knows Spy evs) --> |
388 Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|} |
402 Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|} |
389 \<in> parts (knows Spy evs) --> |
403 \<in> parts (knows Spy evs) --> |
390 B \<notin> bad --> |
404 B \<notin> bad --> |
391 (\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs)" |
405 (\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs)" |
392 apply (erule yahalom.induct, force, |
406 apply (erule yahalom.induct, force, |
393 frule_tac [6] YM4_parts_knows_Spy) |
407 frule_tac [6] YM4_parts_knows_Spy) |
394 apply (analz_mono_contra, simp_all) |
408 apply (analz_mono_contra, simp_all) |
395 (*Fake*) |
409 txt{*Fake*} |
396 apply blast |
410 apply blast |
397 (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*) |
411 txt{*YM3: by @{text new_keys_not_used}, the message |
|
412 @{term "Crypt K (Nonce NB)"} could not exist*} |
398 apply (force dest!: Crypt_imp_keysFor) |
413 apply (force dest!: Crypt_imp_keysFor) |
399 (*YM4: was Crypt K (Nonce NB) the very last message? If so, apply unicity |
414 txt{*YM4: was @{term "Crypt K (Nonce NB)"} the very last message? If so, |
400 of session keys; if not, use ind. hyp.*) |
415 apply unicity of session keys; if not, use the induction hypothesis*} |
401 apply (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys ) |
416 apply (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys) |
402 done |
417 done |
403 |
418 |
404 |
419 |
405 text{*If B receives YM4 then A has used nonce NB (and therefore is alive). |
420 text{*If B receives YM4 then A has used nonce NB (and therefore is alive). |
406 Moreover, A associates K with NB (thus is talking about the same run). |
421 Moreover, A associates K with NB (thus is talking about the same run). |
407 Other premises guarantee secrecy of K.*} |
422 Other premises guarantee secrecy of K.*} |
408 theorem YM4_imp_A_Said_YM3 [rule_format]: |
423 theorem YM4_imp_A_Said_YM3 [rule_format]: |
409 "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, |
424 "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, |
410 Crypt K (Nonce NB)|} \<in> set evs; |
425 Crypt K (Nonce NB)|} \<in> set evs; |
411 (\<forall>NA. Notes Spy {|Nonce NA, Nonce NB, Key K|} \<notin> set evs); |
426 (\<forall>NA. Notes Spy {|Nonce NA, Nonce NB, Key K|} \<notin> set evs); |
412 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
427 K \<in> symKeys; A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
413 ==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs" |
428 ==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs" |
414 by (blast intro: Auth_A_to_B_lemma |
429 by (blast intro: Auth_A_to_B_lemma |
415 dest: Spy_not_see_encrypted_key B_trusts_YM4_shrK) |
430 dest: Spy_not_see_encrypted_key B_trusts_YM4_shrK) |
416 |
431 |
417 end |
432 end |