257 val nonce_OR1_OR2_E = no_nonce_OR1_OR2 RSN (2, rev_notE); |
257 val nonce_OR1_OR2_E = no_nonce_OR1_OR2 RSN (2, rev_notE); |
258 |
258 |
259 (*Crucial property: If the encrypted message appears, and A has used NA |
259 (*Crucial property: If the encrypted message appears, and A has used NA |
260 to start a run, then it originated with the Server!*) |
260 to start a run, then it originated with the Server!*) |
261 goal thy |
261 goal thy |
262 "!!evs. [| A ~: bad; A ~= Spy; evs : otway |] \ |
262 "!!evs. [| A ~: bad; evs : otway |] \ |
263 \ ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs) \ |
263 \ ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs) \ |
264 \ --> Says A B {|NA, Agent A, Agent B, \ |
264 \ --> Says A B {|NA, Agent A, Agent B, \ |
265 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ |
265 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ |
266 \ : set evs --> \ |
266 \ : set evs --> \ |
267 \ (EX NB. Says Server B \ |
267 \ (EX NB. Says Server B \ |
289 (*Corollary: if A receives B's OR4 message and the nonce NA agrees |
289 (*Corollary: if A receives B's OR4 message and the nonce NA agrees |
290 then the key really did come from the Server! CANNOT prove this of the |
290 then the key really did come from the Server! CANNOT prove this of the |
291 bad form of this protocol, even though we can prove |
291 bad form of this protocol, even though we can prove |
292 Spy_not_see_encrypted_key*) |
292 Spy_not_see_encrypted_key*) |
293 goal thy |
293 goal thy |
294 "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \ |
294 "!!evs. [| Says A B {|NA, Agent A, Agent B, \ |
295 \ Says A B {|NA, Agent A, Agent B, \ |
|
296 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \ |
295 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \ |
297 \ A ~: bad; A ~= Spy; evs : otway |] \ |
296 \ Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \ |
|
297 \ A ~: bad; evs : otway |] \ |
298 \ ==> EX NB. Says Server B \ |
298 \ ==> EX NB. Says Server B \ |
299 \ {|NA, \ |
299 \ {|NA, \ |
300 \ Crypt (shrK A) {|NA, Key K|}, \ |
300 \ Crypt (shrK A) {|NA, Key K|}, \ |
301 \ Crypt (shrK B) {|NB, Key K|}|} \ |
301 \ Crypt (shrK B) {|NB, Key K|}|} \ |
302 \ : set evs"; |
302 \ : set evs"; |
341 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); |
341 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); |
342 by (blast_tac (claset() addSEs [lemma]) 1); |
342 by (blast_tac (claset() addSEs [lemma]) 1); |
343 qed "Spy_not_see_encrypted_key"; |
343 qed "Spy_not_see_encrypted_key"; |
344 |
344 |
345 |
345 |
|
346 (*A's guarantee. The Oops premise quantifies over NB because A cannot know |
|
347 what it is.*) |
|
348 goal thy |
|
349 "!!evs. [| Says A B {|NA, Agent A, Agent B, \ |
|
350 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \ |
|
351 \ Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \ |
|
352 \ ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs; \ |
|
353 \ A ~: bad; B ~: bad; evs : otway |] \ |
|
354 \ ==> Key K ~: analz (spies evs)"; |
|
355 by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1); |
|
356 qed "A_gets_good_key"; |
|
357 |
|
358 |
346 (**** Authenticity properties relating to NB ****) |
359 (**** Authenticity properties relating to NB ****) |
347 |
360 |
348 (*Only OR2 can have caused such a part of a message to appear. We do not |
361 (*Only OR2 can have caused such a part of a message to appear. We do not |
349 know anything about X: it does NOT have to have the right form.*) |
362 know anything about X: it does NOT have to have the right form.*) |
350 goal thy |
363 goal thy |
361 |
374 |
362 |
375 |
363 (** The Nonce NB uniquely identifies B's message. **) |
376 (** The Nonce NB uniquely identifies B's message. **) |
364 |
377 |
365 goal thy |
378 goal thy |
366 "!!evs. [| evs : otway; B ~: bad |] \ |
379 "!!evs. [| evs : otway; B ~: bad |] \ |
367 \ ==> EX NA' A'. ALL NA A. \ |
380 \ ==> EX NA' A'. ALL NA A. \ |
368 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs) \ |
381 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs) \ |
369 \ --> NA = NA' & A = A'"; |
382 \ --> NA = NA' & A = A'"; |
370 by (parts_induct_tac 1); |
383 by (parts_induct_tac 1); |
371 by (Blast_tac 1); |
384 by (Blast_tac 1); |
372 by (simp_tac (simpset() addsimps [all_conj_distrib]) 1); |
385 by (simp_tac (simpset() addsimps [all_conj_distrib]) 1); |
385 |
398 |
386 |
399 |
387 (*If the encrypted message appears, and B has used Nonce NB, |
400 (*If the encrypted message appears, and B has used Nonce NB, |
388 then it originated with the Server!*) |
401 then it originated with the Server!*) |
389 goal thy |
402 goal thy |
390 "!!evs. [| B ~: bad; B ~= Spy; evs : otway |] \ |
403 "!!evs. [| B ~: bad; evs : otway |] \ |
391 \ ==> Crypt (shrK B) {|NB, Key K|} : parts (spies evs) \ |
404 \ ==> Crypt (shrK B) {|NB, Key K|} : parts (spies evs) \ |
392 \ --> (ALL X'. Says B Server \ |
405 \ --> (ALL X'. Says B Server \ |
393 \ {|NA, Agent A, Agent B, X', \ |
406 \ {|NA, Agent A, Agent B, X', \ |
394 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \ |
407 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \ |
395 \ : set evs \ |
408 \ : set evs \ |
396 \ --> Says Server B \ |
409 \ --> Says Server B \ |
416 |
429 |
417 |
430 |
418 (*Guarantee for B: if it gets a message with matching NB then the Server |
431 (*Guarantee for B: if it gets a message with matching NB then the Server |
419 has sent the correct message.*) |
432 has sent the correct message.*) |
420 goal thy |
433 goal thy |
421 "!!evs. [| B ~: bad; B ~= Spy; evs : otway; \ |
434 "!!evs. [| Says B Server {|NA, Agent A, Agent B, X', \ |
422 \ Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \ |
|
423 \ Says B Server {|NA, Agent A, Agent B, X', \ |
|
424 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ |
435 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ |
425 \ : set evs |] \ |
436 \ : set evs; \ |
|
437 \ Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \ |
|
438 \ B ~: bad; evs : otway |] \ |
426 \ ==> Says Server B \ |
439 \ ==> Says Server B \ |
427 \ {|NA, \ |
440 \ {|NA, \ |
428 \ Crypt (shrK A) {|NA, Key K|}, \ |
441 \ Crypt (shrK A) {|NA, Key K|}, \ |
429 \ Crypt (shrK B) {|NB, Key K|}|} \ |
442 \ Crypt (shrK B) {|NB, Key K|}|} \ |
430 \ : set evs"; |
443 \ : set evs"; |
431 by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]) 1); |
444 by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]) 1); |
432 qed "B_trusts_OR3"; |
445 qed "B_trusts_OR3"; |
433 |
446 |
434 |
447 |
435 B_trusts_OR3 RS Spy_not_see_encrypted_key; |
448 (*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*) |
436 |
449 goal thy |
437 |
450 "!!evs. [| Says B Server {|NA, Agent A, Agent B, X', \ |
438 goal thy |
451 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ |
439 "!!evs. [| B ~: bad; evs : otway |] \ |
452 \ : set evs; \ |
|
453 \ Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \ |
|
454 \ Notes Spy {|NA, NB, Key K|} ~: set evs; \ |
|
455 \ A ~: bad; B ~: bad; evs : otway |] \ |
|
456 \ ==> Key K ~: analz (spies evs)"; |
|
457 by (blast_tac (claset() addSDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1); |
|
458 qed "B_gets_good_key"; |
|
459 |
|
460 |
|
461 goal thy |
|
462 "!!evs. [| B ~: bad; evs : otway |] \ |
440 \ ==> Says Server B \ |
463 \ ==> Says Server B \ |
441 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
464 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
442 \ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \ |
465 \ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \ |
443 \ (EX X. Says B Server {|NA, Agent A, Agent B, X, \ |
466 \ (EX X. Says B Server {|NA, Agent A, Agent B, X, \ |
444 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ |
467 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ |
452 |
475 |
453 (*After getting and checking OR4, agent A can trust that B has been active. |
476 (*After getting and checking OR4, agent A can trust that B has been active. |
454 We could probably prove that X has the expected form, but that is not |
477 We could probably prove that X has the expected form, but that is not |
455 strictly necessary for authentication.*) |
478 strictly necessary for authentication.*) |
456 goal thy |
479 goal thy |
457 "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \ |
480 "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \ |
458 \ Says A B {|NA, Agent A, Agent B, \ |
481 \ Says A B {|NA, Agent A, Agent B, \ |
459 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \ |
482 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \ |
460 \ A ~: bad; A ~= Spy; B ~: bad; evs : otway |] \ |
483 \ A ~: bad; B ~: bad; evs : otway |] \ |
461 \ ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X, \ |
484 \ ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X, \ |
462 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}\ |
485 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}\ |
463 \ : set evs"; |
486 \ : set evs"; |
464 by (blast_tac (claset() addSDs [A_trusts_OR4] |
487 by (blast_tac (claset() addSDs [A_trusts_OR4] |
465 addSEs [OR3_imp_OR2]) 1); |
488 addSEs [OR3_imp_OR2]) 1); |
466 qed "A_auths_B"; |
489 qed "A_auths_B"; |