266 by (parts_induct_tac 1); |
266 by (parts_induct_tac 1); |
267 (*RA3 requires a further induction*) |
267 (*RA3 requires a further induction*) |
268 by (etac responses.induct 2); |
268 by (etac responses.induct 2); |
269 by (ALLGOALS Asm_simp_tac); |
269 by (ALLGOALS Asm_simp_tac); |
270 (*Fake*) |
270 (*Fake*) |
271 by (simp_tac (simpset() addsimps [parts_insert_spies]) 1); |
|
272 by (Fake_parts_insert_tac 1); |
271 by (Fake_parts_insert_tac 1); |
273 qed "Hash_imp_body"; |
272 qed "Hash_imp_body"; |
274 |
273 |
275 |
274 |
276 (** The Nonce NA uniquely identifies A's message. |
275 (** The Nonce NA uniquely identifies A's message. |
438 by (etac recur.induct 1); |
437 by (etac recur.induct 1); |
439 by analz_spies_tac; |
438 by analz_spies_tac; |
440 by (ALLGOALS |
439 by (ALLGOALS |
441 (asm_simp_tac |
440 (asm_simp_tac |
442 (simpset() addsimps (expand_ifs @ |
441 (simpset() addsimps (expand_ifs @ |
443 [analz_insert_eq, parts_insert_spies, |
442 [analz_insert_eq, analz_insert_freshK])))); |
444 analz_insert_freshK])))); |
|
445 (*RA4*) |
443 (*RA4*) |
446 by (spy_analz_tac 5); |
444 by (spy_analz_tac 5); |
447 (*RA2*) |
445 (*RA2*) |
448 by (spy_analz_tac 3); |
446 by (spy_analz_tac 3); |
449 (*Fake*) |
447 (*Fake*) |
450 by (spy_analz_tac 2); |
448 by (spy_analz_tac 2); |
451 (*Base*) |
449 (*Base*) |
452 by (Blast_tac 1); |
450 by (Blast_tac 1); |
453 (*RA3 remains*) |
451 (*RA3 remains*) |
|
452 by (simp_tac (simpset() addsimps [parts_insert_spies]) 1); |
454 by (safe_tac (claset() delrules [impCE])); |
453 by (safe_tac (claset() delrules [impCE])); |
455 (*RA3, case 2: K is an old key*) |
454 (*RA3, case 2: K is an old key*) |
456 by (blast_tac (claset() addSDs [resp_analz_insert] |
455 by (blast_tac (claset() addSDs [resp_analz_insert] |
457 addSEs partsEs |
456 addSEs partsEs |
458 addDs [Key_in_parts_respond]) 2); |
457 addDs [Key_in_parts_respond]) 2); |
459 (*RA3, case 1: use lemma previously proved by induction*) |
458 (*RA3, case 1: use lemma previously proved by induction*) |
460 by (blast_tac (claset() addSEs [respond_Spy_not_see_session_key RSN |
459 by (blast_tac (claset() addSEs [respond_Spy_not_see_session_key RSN |
461 (2,rev_notE)]) 1); |
460 (2,rev_notE)]) 1); |
462 qed "Spy_not_see_session_key"; |
461 qed "Spy_not_see_session_key"; |
463 |
|
464 |
462 |
465 (**** Authenticity properties for Agents ****) |
463 (**** Authenticity properties for Agents ****) |
466 |
464 |
467 (*The response never contains Hashes*) |
465 (*The response never contains Hashes*) |
468 goal thy |
466 goal thy |