263 goal thy |
368 goal thy |
264 "!!evs. [| evs : traces; length evs <= length evs' |] ==> \ |
369 "!!evs. [| evs : traces; length evs <= length evs' |] ==> \ |
265 \ newK evs' ~: keysFor (parts (sees C evs))"; |
370 \ newK evs' ~: keysFor (parts (sees C evs))"; |
266 by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1); |
371 by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1); |
267 qed "new_keys_not_used"; |
372 qed "new_keys_not_used"; |
268 Addsimps [new_keys_not_used]; |
|
269 |
373 |
270 bind_thm ("new_keys_not_analyzed", |
374 bind_thm ("new_keys_not_analyzed", |
271 [analyze_subset_parts RS keysFor_mono, |
375 [analyze_subset_parts RS keysFor_mono, |
272 new_keys_not_used] MRS contra_subsetD); |
376 new_keys_not_used] MRS contra_subsetD); |
273 |
377 |
274 |
378 Addsimps [new_keys_not_used, new_keys_not_analyzed]; |
275 (*Maybe too specific to be of much use...*) |
379 |
276 goal thy |
380 |
277 "!!evs. [| Says Server A (Crypt {|Nonce NA, Agent B, Key K, X|} \ |
381 (** Rewrites to push in Key and Crypt messages, so that other messages can |
278 \ (serverKey A)) \ |
382 be pulled out using the analyze_insert rules **) |
279 \ : setOfList evs; \ |
383 |
|
384 fun insComm x y = read_instantiate_sg (sign_of thy) [("x",x), ("y",y)] |
|
385 insert_commute; |
|
386 |
|
387 val pushKeys = map (insComm "Key ?K") |
|
388 ["Agent ?C", "Nonce ?N", "MPair ?X ?Y", "Crypt ?X ?K'"]; |
|
389 |
|
390 val pushCrypts = map (insComm "Crypt ?X ?K") |
|
391 ["Agent ?C", "Nonce ?N", "MPair ?X' ?Y"]; |
|
392 |
|
393 (*Cannot be added with Addsimps -- we don't always want to re-order messages*) |
|
394 val pushes = pushKeys@pushCrypts; |
|
395 |
|
396 val pushKey_newK = insComm "Key (newK ?evs)" "Key (serverKey ?C)"; |
|
397 |
|
398 |
|
399 (** Lemmas concerning the form of items passed in messages **) |
|
400 |
|
401 (*Describes the form *and age* of K, and the form of X, |
|
402 when the following message is sent*) |
|
403 goal thy |
|
404 "!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') : setOfList evs; \ |
280 \ evs : traces \ |
405 \ evs : traces \ |
281 \ |] ==> (EX evs'. X = (Crypt {|Key(newK evs'), Agent A|} (serverKey B)))"; |
406 \ |] ==> (EX evs':traces. K = Key(newK evs') & length evs' < length evs & \ |
282 be rev_mp 1; |
407 \ X = (Crypt {|K, Agent A|} (serverKey B)))"; |
283 be traces.induct 1; |
|
284 be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*) |
|
285 be subst 5; (*NS3: discard evsa = Says S Aa... as irrelevant!*) |
|
286 by (ALLGOALS Asm_full_simp_tac); |
|
287 by (Fast_tac 1); (*Proves the NS2 case*) |
|
288 qed "Says_Server_imp_X_eq_Crypt"; |
|
289 |
|
290 |
|
291 (*Pushes Crypt events in so that others might be pulled out*) |
|
292 goal thy "insert (Crypt X K) (insert y evs) = \ |
|
293 \ insert y (insert (Crypt X K) evs)"; |
|
294 by (Fast_tac 1); |
|
295 qed "insert_Crypt_delay"; |
|
296 |
|
297 goal thy "insert (Key K) (insert y evs) = \ |
|
298 \ insert y (insert (Key K) evs)"; |
|
299 by (Fast_tac 1); |
|
300 qed "insert_Key_delay"; |
|
301 |
|
302 |
|
303 (** Lemmas concerning the form of items passed in messages **) |
|
304 |
|
305 (*Describes the form *and age* of K when the following message is sent*) |
|
306 goal thy |
|
307 "!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') \ |
|
308 \ : setOfList evs; \ |
|
309 \ evs : traces \ |
|
310 \ |] ==> (EX evs'. K = Key (newK evs') & length evs' < length evs)"; |
|
311 be rev_mp 1; |
408 be rev_mp 1; |
312 be traces.induct 1; |
409 be traces.induct 1; |
313 be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*) |
410 be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*) |
314 by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset)))); |
411 by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset)))); |
315 qed "Says_Server_imp_Key_newK"; |
412 qed "Says_Server_message_form"; |
316 |
413 |
317 (* c ~: keysFor (parts H) ==> c ~: keysFor (analyze H) *) |
414 (* c ~: keysFor (parts H) ==> c ~: keysFor (analyze H) *) |
318 bind_thm ("not_parts_not_keysFor_analyze", |
415 bind_thm ("not_parts_not_keysFor_analyze", |
319 analyze_subset_parts RS keysFor_mono RS contra_subsetD); |
416 analyze_subset_parts RS keysFor_mono RS contra_subsetD); |
|
417 |
|
418 |
|
419 |
|
420 (*USELESS for NS3, case 1, as the ind hyp says the same thing! |
|
421 goal thy |
|
422 "!!evs. [| evs = Says Server (Friend i) \ |
|
423 \ (Crypt {|N, Agent(Friend j), K, X|} K') # evs'; \ |
|
424 \ evs : traces; i~=k \ |
|
425 \ |] ==> \ |
|
426 \ K ~: analyze (insert (Key (serverKey (Friend k))) (sees Enemy evs))"; |
|
427 be rev_mp 1; |
|
428 be traces.induct 1; |
|
429 be subst 4; (*NS2: discard evsa = Says A Server... as irrelevant!*) |
|
430 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes))); |
|
431 by (Step_tac 1); |
|
432 by (asm_full_simp_tac (!simpset addsimps[analyze_subset_parts RS contra_subsetD]) 1); |
|
433 val Enemy_not_see_encrypted_key_lemma = result(); |
|
434 *) |
|
435 |
|
436 |
|
437 (*Describes the form of X when the following message is sent*) |
|
438 goal thy |
|
439 "!!evs. evs : traces ==> \ |
|
440 \ ALL A NA B K X. \ |
|
441 \ (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \ |
|
442 \ : parts (sees Enemy evs) & A ~= Enemy --> \ |
|
443 \ (EX evt:traces. K = newK evt & \ |
|
444 \ X = (Crypt {|Key K, Agent A|} (serverKey B)))"; |
|
445 be traces.induct 1; |
|
446 be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*) |
|
447 by (Step_tac 1); |
|
448 by (ALLGOALS Asm_full_simp_tac); |
|
449 (*Remaining cases are Fake, NS2 and NS3*) |
|
450 by (fast_tac (!claset addSDs [spec]) 2); |
|
451 (*The NS3 case needs the induction hypothesis twice! |
|
452 One application is to the X component of the most recent message.*) |
|
453 by (full_simp_tac (!simpset addsimps [conj_disj_distribR, all_conj_distrib]) 2); |
|
454 be conjE 2; |
|
455 by (subgoal_tac "? evs':traces. K = newK evs' & \ |
|
456 \ X = Crypt {|Key K, Agent (Friend i)|} (serverKey B)" 2); |
|
457 (*DELETE the second quantified formula for speed*) |
|
458 by (eres_inst_tac [("V","ALL A NA B K Xa. ?f A NA B K Xa : ?H X & ?P(A) --> \ |
|
459 \ ?Q K Xa A B")] thin_rl 3); |
|
460 by (fast_tac (!claset addSEs [allE, mp] addss (!simpset)) 3); |
|
461 (*DELETE the first quantified formula: it's now useless*) |
|
462 by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2); |
|
463 by (fast_tac (!claset addss (!simpset)) 2); |
|
464 (*Now for the Fake case*) |
|
465 by (subgoal_tac |
|
466 "Crypt {|Nonce NA, Agent Ba, Key K, Xa|} (serverKey A) : \ |
|
467 \ parts (synthesize (analyze (sees Enemy evsa)) Un (sees Enemy evsa))" 1); |
|
468 by (fast_tac (!claset addSEs [impOfSubs parts_mono]) 2); |
|
469 by (best_tac (!claset addDs [impOfSubs analyze_subset_parts] |
|
470 addss (!simpset)) 1); |
|
471 val encrypted_form = result(); |
|
472 |
|
473 |
|
474 (*For eliminating the A ~= Enemy condition from the previous result*) |
|
475 goal thy |
|
476 "!!evs. evs : traces ==> \ |
|
477 \ ALL S A NA B K X. \ |
|
478 \ Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \ |
|
479 \ : setOfList evs --> \ |
|
480 \ S = Server | S = Enemy"; |
|
481 be traces.induct 1; |
|
482 be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*) |
|
483 by (ALLGOALS Asm_full_simp_tac); |
|
484 (*We are left with NS3*) |
|
485 by (subgoal_tac "S = Server | S = Enemy" 1); |
|
486 (*First justify this assumption!*) |
|
487 by (fast_tac (!claset addSEs [allE, mp] addss (!simpset)) 2); |
|
488 by (Step_tac 1); |
|
489 bd (setOfList_I1 RS Says_Server_message_form) 1; |
|
490 by (ALLGOALS Full_simp_tac); |
|
491 (*Final case. Clear out needless quantifiers to speed the following step*) |
|
492 by (eres_inst_tac [("V","ALL x. ?P(x)")] thin_rl 1); |
|
493 bd (normalize_thm [RSspec,RSmp] encrypted_form) 1; |
|
494 br (parts.Inj RS conjI) 1; |
|
495 auto(); |
|
496 qed_spec_mp "Server_or_Enemy"; |
|
497 |
|
498 |
|
499 |
|
500 (*Describes the form of X when the following message is sent; |
|
501 use Says_Server_message_form if applicable*) |
|
502 goal thy |
|
503 "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \ |
|
504 \ : setOfList evs; \ |
|
505 \ evs : traces \ |
|
506 \ |] ==> (EX evt:traces. K = newK evt & \ |
|
507 \ X = (Crypt {|Key K, Agent A|} (serverKey B)))"; |
|
508 by (forward_tac [Server_or_Enemy] 1); |
|
509 ba 1; |
|
510 by (Step_tac 1); |
|
511 by (fast_tac (!claset addSDs [Says_Server_message_form] addss (!simpset)) 1); |
|
512 by (forward_tac [normalize_thm [RSspec,RSmp] encrypted_form] 1); |
|
513 br (parts.Inj RS conjI) 1; |
|
514 by (Auto_tac()); |
|
515 qed "Says_S_message_form"; |
|
516 |
|
517 goal thy |
|
518 "!!evs. [| evs = Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} \ |
|
519 \ (serverKey A)) # evs'; \ |
|
520 \ evs : traces \ |
|
521 \ |] ==> (EX evt:traces. evs' : traces & \ |
|
522 \ K = newK evt & \ |
|
523 \ X = (Crypt {|Key K, Agent A|} (serverKey B)))"; |
|
524 by (forward_tac [traces_eq_ConsE] 1); |
|
525 by (dtac (setOfList_eqI1 RS Says_S_message_form) 2); |
|
526 by (Auto_tac()); |
|
527 qed "Says_S_message_form_eq"; |
|
528 |
|
529 |
|
530 |
|
531 |
|
532 (**** |
|
533 The following is to prove theorems of the form |
|
534 |
|
535 Key K : analyze (insert (Key (newK evt)) |
|
536 (insert (Key (serverKey C)) (sees Enemy evs))) ==> |
|
537 Key K : analyze (insert (Key (serverKey C)) (sees Enemy evs)) |
|
538 |
|
539 A more general formula must be proved inductively. |
|
540 |
|
541 ****) |
|
542 |
|
543 |
|
544 (*Not useful in this form, but it says that session keys are not used |
|
545 to encrypt messages containing other keys, in the actual protocol. |
|
546 We require that agents should behave like this subsequently also.*) |
|
547 goal thy |
|
548 "!!evs. evs : traces ==> \ |
|
549 \ (Crypt X (newK evt)) : parts (sees Enemy evs) & \ |
|
550 \ Key K : parts {X} --> Key K : parts (sees Enemy evs)"; |
|
551 be traces.induct 1; |
|
552 be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*) |
|
553 by (hyp_subst_tac 5); (*NS3: apply evsa = Says S A (Crypt ...) # ... *) |
|
554 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes))); |
|
555 (*Case NS3*) |
|
556 by (res_inst_tac [("x1","Xa")] (insert_commute RS ssubst) 2); |
|
557 by (Asm_full_simp_tac 2); |
|
558 (*Deals with Faked messages*) |
|
559 by (best_tac (!claset addDs [impOfSubs analyze_subset_parts, |
|
560 impOfSubs parts_insert_subset_Un] |
|
561 addss (!simpset)) 1); |
|
562 result(); |
|
563 |
|
564 |
|
565 (** Specialized rewrites for this proof **) |
|
566 |
|
567 Delsimps [image_insert]; |
|
568 Addsimps [image_insert RS sym]; |
|
569 |
|
570 goal thy "insert (Key (newK x)) (sees A evs) = \ |
|
571 \ Key `` (newK``{x}) Un (sees A evs)"; |
|
572 by (Fast_tac 1); |
|
573 val insert_Key_singleton = result(); |
|
574 |
|
575 goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \ |
|
576 \ Key `` (f `` (insert x E)) Un C"; |
|
577 by (Fast_tac 1); |
|
578 val insert_Key_image = result(); |
|
579 |
|
580 |
|
581 goal thy |
|
582 "!!evs. evs : traces ==> \ |
|
583 \ ALL K E. (Key K : analyze (insert (Key (serverKey C)) \ |
|
584 \ (Key``(newK``E) Un (sees Enemy evs)))) = \ |
|
585 \ (K : newK``E | \ |
|
586 \ Key K : analyze (insert (Key (serverKey C)) \ |
|
587 \ (sees Enemy evs)))"; |
|
588 be traces.induct 1; |
|
589 be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*) |
|
590 by (dtac Says_S_message_form_eq 5 THEN assume_tac 5); |
|
591 by (REPEAT ((eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac) 5)); |
|
592 by (ALLGOALS |
|
593 (asm_full_simp_tac |
|
594 (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK] |
|
595 @ pushes) |
|
596 setloop split_tac [expand_if]))); |
|
597 (*Cases NS2 and NS3!! Simple, thanks to auto case splits*) |
|
598 by (REPEAT (Fast_tac 3)); |
|
599 (*Base case*) |
|
600 by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); |
|
601 (** LEVEL 7 **) |
|
602 (*Fake case*) |
|
603 by (REPEAT (Safe_step_tac 1)); |
|
604 by (fast_tac (!claset addSEs [impOfSubs (analyze_mono)]) 2); |
|
605 by (subgoal_tac |
|
606 "Key K : analyze \ |
|
607 \ (synthesize \ |
|
608 \ (analyze (insert (Key (serverKey C)) \ |
|
609 \ (Key``(newK``E) Un (sees Enemy evsa)))))" 1); |
|
610 (*First, justify this subgoal*) |
|
611 (*Discard the quantified formula for better speed*) |
|
612 by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2); |
|
613 by (eres_inst_tac [("V","?Q ~: ?QQ")] thin_rl 2); |
|
614 by (best_tac (!claset addIs [impOfSubs (analyze_mono RS synthesize_mono)] |
|
615 addSEs [impOfSubs analyze_mono]) 2); |
|
616 by (Asm_full_simp_tac 1); |
|
617 by (deepen_tac (!claset addIs [impOfSubs analyze_mono]) 0 1); |
|
618 qed_spec_mp "analyze_image_newK"; |
|
619 |
|
620 |
|
621 goal thy |
|
622 "!!evs. evs : traces ==> \ |
|
623 \ Key K : analyze (insert (Key (newK evt)) \ |
|
624 \ (insert (Key (serverKey C)) \ |
|
625 \ (sees Enemy evs))) = \ |
|
626 \ (K = newK evt | \ |
|
627 \ Key K : analyze (insert (Key (serverKey C)) \ |
|
628 \ (sees Enemy evs)))"; |
|
629 by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analyze_image_newK, |
|
630 insert_Key_singleton]) 1); |
|
631 by (Fast_tac 1); |
|
632 qed "analyze_insert_Key_newK"; |
|
633 |
|
634 |
|
635 |
|
636 |
|
637 XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX; |
|
638 |
|
639 |
|
640 goal thy |
|
641 "!!evs. [| evs = Says Server (Friend i) \ |
|
642 \ (Crypt {|N, Agent(Friend j), K, X|} K') # evs'; \ |
|
643 \ evs : traces; i~=k \ |
|
644 \ |] ==> \ |
|
645 \ K = newK evs'"; ???????????????? |
|
646 |
|
647 |
|
648 goals_limit:=2; |
|
649 goal thy |
|
650 "!!evs. [| Says S A \ |
|
651 \ (Crypt {|N, Agent B, Key K, X|} (serverKey A)) : setOfList evs; \ |
|
652 \ evs : traces \ |
|
653 \ |] ==> \ |
|
654 \ ALL A' N' B' X'. \ |
|
655 \ Says Server A' \ |
|
656 \ (Crypt {|N', Agent B', Key K, X'|} (serverKey A')) : \ |
|
657 \ setOfList evs --> X = X'"; |
|
658 be rev_mp 1; |
|
659 be traces.induct 1; |
|
660 be subst 4; (*NS2: discard evsa = Says A Server... as irrelevant!*) |
|
661 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes))); |
|
662 by (REPEAT_FIRST (resolve_tac [conjI, impI, allI] ORELSE' etac conjE |
|
663 ORELSE' hyp_subst_tac)); |
|
664 |
|
665 by (ALLGOALS (full_simp_tac (!simpset addsimps [not_Cons_self]))); |
|
666 by (Step_tac 1); |
|
667 fe Crypt_synthesize; |
|
668 by (fast_tac (!claset addss (!simpset)) 2); |
|
669 |
|
670 |
|
671 |
|
672 by (Step_tac 1); |
|
673 by (asm_full_simp_tac (!simpset addsimps[analyze_subset_parts RS contra_subsetD]) 1); |
|
674 val Enemy_not_see_encrypted_key_lemma = result(); |
|
675 |
|
676 |
|
677 |
|
678 |
|
679 AddSEs [less_irrefl]; |
|
680 |
|
681 (*Crucial security property: Enemy does not see the keys sent in msg NS2 |
|
682 -- even if another key is compromised*) |
|
683 goal thy |
|
684 "!!evs. [| Says Server (Friend i) \ |
|
685 \ (Crypt {|N, Agent(Friend j), K, X|} K') : setOfList evs; \ |
|
686 \ evs : traces; Friend i ~= C; Friend j ~= C \ |
|
687 \ |] ==> \ |
|
688 \ K ~: analyze (insert (Key (serverKey C)) (sees Enemy evs))"; |
|
689 be rev_mp 1; |
|
690 be traces.induct 1; |
|
691 be subst 4; (*NS2: discard evsa = Says A Server... as irrelevant!*) |
|
692 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes))); |
|
693 (*Next 3 steps infer that K has the form "Key (newK evs'" ... *) |
|
694 by (REPEAT_FIRST (resolve_tac [conjI, impI])); |
|
695 by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac)); |
|
696 by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac)); |
|
697 by (ALLGOALS |
|
698 (asm_full_simp_tac |
|
699 (!simpset addsimps ([analyze_subset_parts RS contra_subsetD, |
|
700 analyze_insert_Key_newK] @ pushes) |
|
701 setloop split_tac [expand_if]))); |
|
702 |
|
703 (*NS2*) |
|
704 by (Fast_tac 2); |
|
705 (** LEVEL 9 **) |
|
706 (*Now for the Fake case*) |
|
707 br notI 1; |
|
708 by (subgoal_tac |
|
709 "Key (newK evs') : \ |
|
710 \ analyze (synthesize (analyze (insert (Key (serverKey C)) \ |
|
711 \ (sees Enemy evsa))))" 1); |
|
712 be (impOfSubs analyze_mono) 2; |
|
713 by (deepen_tac (!claset addIs [analyze_mono RS synthesize_mono RSN |
|
714 (2,rev_subsetD), |
|
715 impOfSubs synthesize_increasing, |
|
716 impOfSubs analyze_increasing]) 0 2); |
|
717 (*Proves the Fake goal*) |
|
718 by (fast_tac (!claset addss (!simpset)) 1); |
|
719 |
|
720 (**LEVEL 16**) |
|
721 (*Now for NS3*) |
|
722 (*NS3, case 1: that message from the Server was just sent*) |
|
723 by (ALLGOALS (forward_tac [traces_ConsE])); |
|
724 by (forward_tac [setOfList_I1 RS Says_Server_message_form] 1); |
|
725 by (Full_simp_tac 1); |
|
726 by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac)); |
|
727 (*Can simplify the Crypt messages: their key is secure*) |
|
728 by (dres_inst_tac [("psi", "?X ~: ?H")] asm_rl 1); |
|
729 by (asm_full_simp_tac |
|
730 (!simpset addsimps (pushes @ [analyze_insert_Crypt, |
|
731 analyze_subset_parts RS contra_subsetD])) 1); |
|
732 |
|
733 (**LEVEL 20, one subgoal left! **) |
|
734 (*NS3, case 2: that message from the Server was sent earlier*) |
|
735 |
|
736 (*simplify the good implication*) |
|
737 by (Asm_full_simp_tac 1); |
|
738 by (eres_inst_tac [("V","?P-->?Q")] thin_rl 1); (*delete the bad implication*) |
|
739 by ((forward_tac [Says_Server_message_form] THEN' assume_tac) 1); |
|
740 by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac)); |
|
741 by (Full_simp_tac 1); |
|
742 |
|
743 (**LEVEL 25 **) |
|
744 |
|
745 by ((forward_tac [setOfList_I1 RS Says_S_message_form]) 1); |
|
746 by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac)); |
|
747 by (asm_full_simp_tac (!simpset addsimps (analyze_insert_Key_newK::pushes)) 1); |
|
748 by (step_tac (!claset delrules [impCE]) 1); |
|
749 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes))); |
|
750 |
|
751 |
|
752 by (Step_tac 1); |
|
753 by (Fast_tac 1); |
|
754 |
|
755 (*May do this once we have proved that the keys coincide*) |
|
756 by (subgoal_tac "i = ia & N = Nonce NA & Friend j = C & K' = serverKey (Friend ia)" 1); |
|
757 by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac)); |
|
758 |
|
759 (**LEVEL 29 **) |
|
760 |
|
761 by (asm_full_simp_tac (!simpset addsimps (pushes)) 1); |
|
762 |
|
763 |
|
764 (*ALL THAT REMAINS IS TO PROVE THE SUBGOAL!*) |
|
765 |
|
766 |
|
767 |
|
768 |
|
769 |
|
770 by (Step_tac 1); |
|
771 by (Fast_tac 1); |
|
772 |
|
773 |
|
774 |
|
775 |
|
776 by (forward_tac [setOfList_I1 RSN (2, Server_or_Enemy)] 1); |
|
777 |
|
778 |
|
779 (!simpset addsimps ([analyze_subset_parts RS keysFor_mono RS contra_subsetD])) 1); |
|
780 |
|
781 |
|
782 by (excluded_middle_tac "evs'a=evt" 1); |
|
783 (*Keys agree? Then should have B = Friend j, so encrypted msg is secure*) |
|
784 by (subgoal_tac "B = Friend j" 2); |
|
785 by (REPEAT_FIRST hyp_subst_tac); |
|
786 by (asm_full_simp_tac |
|
787 (!simpset addsimps ([analyze_subset_parts RS contra_subsetD])) 2); |
|
788 (*Keys differ? Then they cannot clash*) |
|
789 |
|
790 br notI 1; |
|
791 bd (impOfSubs analyze_insert_Crypt_subset) 1; |
|
792 |
|
793 |
|
794 ????????????????????????????????????????????????????????????????; |
|
795 |
|
796 (**LEVEL 35 **) |
|
797 |
|
798 (*In this case, the Key in X (newK evs') is younger than |
|
799 the Key we are worried about (newK evs'a). And nobody has used the |
|
800 new Key yet, so it can be pulled out of the "analyze".*) |
|
801 by (asm_full_simp_tac |
|
802 (!simpset addsimps ([analyze_subset_parts RS keysFor_mono RS contra_subsetD])) 1); |
|
803 by (Fast_tac 1); |
|
804 (*In this case, Enemy has seen the (encrypted!) message at hand...*) |
|
805 by (dres_inst_tac [("psi", "?X ~: ?H")] asm_rl 1); |
|
806 by (asm_full_simp_tac (!simpset addsimps ([insert_absorb]@pushes)) 1); |
|
807 |
|
808 (**LEVEL 39 **) |
|
809 |
|
810 br notI 1; |
|
811 bd (impOfSubs analyze_insert_Crypt_subset) 1; |
|
812 by (asm_full_simp_tac |
|
813 (!simpset addsimps ([analyze_subset_parts RS keysFor_mono RS contra_subsetD])) 1); |
|
814 |
|
815 |
|
816 by (excluded_middle_tac "evs'a=evt" 1); |
|
817 (*Keys agree? Then should have B = Friend j, so encrypted msg is secure*) |
|
818 by (subgoal_tac "B = Friend j" 2); |
|
819 by (REPEAT_FIRST hyp_subst_tac); |
|
820 by (asm_full_simp_tac |
|
821 (!simpset addsimps ([analyze_subset_parts RS contra_subsetD])) 2); |
|
822 (*Keys differ? Then they cannot clash*) |
|
823 |
|
824 br notI 1; |
|
825 bd (impOfSubs analyze_insert_Crypt_subset) 1; |
|
826 |
|
827 |
|
828 |
|
829 |
|
830 |
|
831 |
|
832 |
|
833 (**LEVEL 28 OLD VERSION, with extra case split on ia=k **) |
|
834 |
|
835 by (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1); |
|
836 by (excluded_middle_tac "ia=k" 1); |
|
837 (*Case where the key is compromised*) |
|
838 by (hyp_subst_tac 2); |
|
839 by (asm_full_simp_tac (!simpset addsimps pushes) 2); |
|
840 by (full_simp_tac (!simpset addsimps [insert_commute]) 2); |
|
841 |
|
842 (**LEVEL 33 **) |
|
843 |
|
844 XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX; |
|
845 proof_timing:=true; |
|
846 AddSEs [less_irrefl]; |
|
847 |
|
848 |
|
849 (*Case where the key is secure*) |
|
850 by (dres_inst_tac [("psi", "?X ~: ?H")] asm_rl 1); |
|
851 |
|
852 (*pretend we have the right lemma!*) |
|
853 (*EITHER the message was just sent by the Server, OR is a replay from the Enemy |
|
854 -- in either case it has the right form, only the age differs |
|
855 *) |
|
856 by (subgoal_tac "EX evt. K = newK evt & X = (Crypt {|Key K, Agent(Friend ia)|} (serverKey B)) & (evt = evs' | (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey (Friend ia))) : sees Enemy evs')" 1); |
|
857 by (REPEAT_FIRST (eresolve_tac [exE, disjE, conjE] ORELSE' hyp_subst_tac)); |
|
858 by (asm_full_simp_tac (!simpset addsimps pushes) 1); |
|
859 by (res_inst_tac [("x1","Crypt ?U (?K ia)")] (insert_commute RS ssubst) 1); |
|
860 br notI 1; |
|
861 |
|
862 bd (impOfSubs analyze_insert_Crypt_subset) 1; |
|
863 |
|
864 (**LEVEL 40 **) |
|
865 |
|
866 (*In this case, the Key in X (newK evs') is younger than |
|
867 the Key we are worried about (newK evs'a). And nobody has used the |
|
868 new Key yet, so it can be pulled out of the "analyze".*) |
|
869 by (asm_full_simp_tac |
|
870 (!simpset addsimps ([analyze_subset_parts RS keysFor_mono RS contra_subsetD])) 1); |
|
871 by (Fast_tac 1); |
|
872 (*In this case, Enemy already knows about the message at hand...*) |
|
873 by (dres_inst_tac [("psi", "?X ~: ?H")] asm_rl 1); |
|
874 by (asm_full_simp_tac (!simpset addsimps ([insert_absorb]@pushes)) 1); |
|
875 |
|
876 (**LEVEL 44 **) |
|
877 |
|
878 by (excluded_middle_tac "evs'a=evt" 1); |
|
879 (*Keys agree? Then should have B = Friend j, so encrypted msg is secure*) |
|
880 by (subgoal_tac "B = Friend j" 2); |
|
881 by (REPEAT_FIRST hyp_subst_tac); |
|
882 by (asm_full_simp_tac |
|
883 (!simpset addsimps ([analyze_subset_parts RS contra_subsetD])) 2); |
|
884 (*Keys differ? Then they cannot clash*) |
|
885 |
|
886 br notI 1; |
|
887 bd (impOfSubs analyze_insert_Crypt_subset) 1; |
|
888 |
|
889 by (asm_full_simp_tac |
|
890 (!simpset addsimps (pushes@[analyze_subset_parts RS keysFor_mono RS contra_subsetD])) 1); |
|
891 by (Fast_tac 1); |
|
892 |
|
893 |
|
894 |
|
895 by (excluded_middle_tac "evs'a=evt" 1); |
|
896 (*Keys agree? Then should have B = Friend j, so encrypted msg is secure*) |
|
897 by (subgoal_tac "B = Friend j & ia=i" 2); |
|
898 by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac)); |
|
899 by (asm_full_simp_tac |
|
900 (!simpset addsimps ([analyze_subset_parts RS contra_subsetD])) 2); |
|
901 (*Keys differ? Then they cannot clash*) |
|
902 |
|
903 br notI 1; |
|
904 bd (impOfSubs analyze_insert_Crypt_subset) 1; |
|
905 |
|
906 by (asm_full_simp_tac |
|
907 (!simpset addsimps (pushes@[analyze_subset_parts RS keysFor_mono RS contra_subsetD])) 1); |
|
908 by (Fast_tac 1); |
|
909 |
|
910 |
|
911 Level 51 |
|
912 !!evs. [| Says Server (Friend i) (Crypt {|N, Agent (Friend j), K, X|} K') : |
|
913 setOfList evs; |
|
914 evs : traces; i ~= k; j ~= k |] ==> |
|
915 K ~: analyze (insert (Key (serverKey (Friend k))) (sees Enemy evs)) |
|
916 1. !!evs A B K NA S X evsa evs' ia evs'a evt. |
|
917 [| i ~= k; j ~= k; |
|
918 Says S (Friend ia) |
|
919 (Crypt |
|
920 {|Nonce NA, Agent B, Key (newK evt), |
|
921 Crypt {|Key (newK evt), Agent (Friend ia)|} (serverKey B)|} |
|
922 (serverKey (Friend ia))) # |
|
923 evs' : |
|
924 traces; |
|
925 Friend ia ~= B; |
|
926 Says (Friend ia) Server {|Agent (Friend ia), Agent B, Nonce NA|} : |
|
927 setOfList evs'; |
|
928 Says Server (Friend i) |
|
929 (Crypt |
|
930 {|N, Agent (Friend j), Key (newK evs'a), |
|
931 Crypt {|Key (newK evs'a), Agent (Friend i)|} |
|
932 (serverKey (Friend j))|} |
|
933 K') : |
|
934 setOfList evs'; |
|
935 evs' : traces; length evs'a < length evs'; ia ~= k; |
|
936 Crypt |
|
937 {|Nonce NA, Agent B, Key (newK evt), |
|
938 Crypt {|Key (newK evt), Agent (Friend ia)|} (serverKey B)|} |
|
939 (serverKey (Friend ia)) : |
|
940 sees Enemy evs'; |
|
941 Key (newK evs'a) ~: |
|
942 analyze (insert (Key (serverKey (Friend k))) (sees Enemy evs')); |
|
943 evs'a ~= evt; |
|
944 Key (newK evs'a) : |
|
945 analyze |
|
946 (insert (Key (newK evt)) |
|
947 (insert (Key (serverKey (Friend k))) (sees Enemy evs'))) |] ==> |
|
948 False |
|
949 |
|
950 |
|
951 |
|
952 |
|
953 YYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYY; |
|
954 |
|
955 |
|
956 push_proof(); |
|
957 goal thy |
|
958 "!!evs. [| evs = Says S (Friend i) \ |
|
959 \ (Crypt {|N, Agent(Friend j), K, X|} K') # evs'; \ |
|
960 \ evs : traces; i~=k \ |
|
961 \ |] ==> \ |
|
962 \ K ~: analyze (insert (Key (serverKey (Friend k))) (sees Enemy evs))"; |
|
963 be rev_mp 1; |
|
964 be traces.induct 1; |
|
965 be subst 4; (*NS2: discard evsa = Says A Server... as irrelevant!*) |
|
966 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes))); |
|
967 by (Step_tac 1); |
|
968 by (asm_full_simp_tac (!simpset addsimps[analyze_subset_parts RS contra_subsetD]) 1); |
|
969 val Enemy_not_see_encrypted_key_lemma = result(); |
|
970 |
|
971 |
|
972 |
|
973 |
|
974 by (asm_full_simp_tac |
|
975 (!simpset addsimps (pushes @ |
|
976 [analyze_subset_parts RS contra_subsetD, |
|
977 traces_ConsE RS Enemy_not_see_serverKey])) 1); |
|
978 |
|
979 by (asm_full_simp_tac |
|
980 (!simpset addsimps [analyze_subset_parts RS keysFor_mono RS contra_subsetD, |
|
981 traces_ConsE RS new_keys_not_used]) 1); |
|
982 by (Fast_tac 1); |
|
983 |
|
984 |
|
985 |
|
986 |
|
987 (*Precisely formulated as needed below. Perhaps redundant, as simplification |
|
988 with the aid of analyze_subset_parts RS contra_subsetD might do the |
|
989 same thing.*) |
|
990 goal thy |
|
991 "!!evs. [| evs : traces; A ~= Enemy; A ~= Friend j |] ==> \ |
|
992 \ Key (serverKey A) ~: \ |
|
993 \ analyze (insert (Key (serverKey (Friend j))) (sees Enemy evs))"; |
|
994 br (analyze_subset_parts RS contra_subsetD) 1; |
|
995 by (Asm_simp_tac 1); |
|
996 qed "insert_not_analyze_serverKey"; |
|
997 |
|
998 |
|
999 |
|
1000 |
|
1001 by (asm_full_simp_tac |
|
1002 (!simpset addsimps (pushes @ |
|
1003 [insert_not_analyze_serverKey, |
|
1004 traces_ConsE RS insert_not_analyze_serverKey])) 1); |
|
1005 |
|
1006 |
|
1007 by (stac analyze_insert_Crypt 1); |
|
1008 |
|
1009 |
|
1010 |
|
1011 |
|
1012 |
|
1013 |
|
1014 |
|
1015 |
|
1016 |
|
1017 |
|
1018 |
|
1019 |
|
1020 (*NS3, case 1: that message from the Server was just sent*) |
|
1021 by (asm_full_simp_tac (!simpset addsimps pushes) 1); |
|
1022 |
|
1023 (*NS3, case 2: that message from the Server was sent earlier*) |
|
1024 by (REPEAT_FIRST (eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac)); |
|
1025 by (mp_tac 1); |
|
1026 by (asm_full_simp_tac (!simpset addsimps pushes) 1); |
|
1027 |
|
1028 by (Step_tac 1); |
|
1029 by (asm_full_simp_tac |
|
1030 (!simpset addsimps [traces_ConsE RS insert_not_analyze_serverKey]) 1); |
|
1031 |
|
1032 |
|
1033 |
|
1034 (*pretend we have the right lemma!*) |
|
1035 by (subgoal_tac "(EX evt. X = (Crypt {|Key(newK evt), Agent(Friend ia)|} (serverKey B)))" 1); |
|
1036 by (REPEAT_FIRST (eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac)); |
|
1037 by (asm_full_simp_tac (!simpset addsimps pushes) 1); |
|
1038 |
|
1039 by (excluded_middle_tac "ia=k" 1); |
|
1040 (*Case where the key is compromised*) |
|
1041 by (hyp_subst_tac 2); |
|
1042 by (stac insert_commute 2); (*Pushes in the "insert X" for simplification*) |
|
1043 by (Asm_full_simp_tac 2); |
|
1044 |
|
1045 |
|
1046 |
|
1047 by (asm_full_simp_tac (!simpset addsimps pushes) 1); |
|
1048 |
|
1049 by (REPEAT_FIRST Safe_step_tac); |
|
1050 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes))); |
|
1051 |
|
1052 |
|
1053 by (REPEAT (Safe_step_tac 1)); |
|
1054 |
|
1055 |
|
1056 |
|
1057 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes))); |
|
1058 |
|
1059 by (REPEAT_FIRST (eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac)); |
|
1060 |
|
1061 by (eres_inst_tac [("V","?P-->?Q")] thin_rl 1); (*deletes the bad implication*) |
|
1062 by ((forward_tac [Says_Server_message_form] THEN' |
|
1063 fast_tac (!claset addSEs [traces_ConsE])) 1); |
|
1064 by (REPEAT_FIRST (eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac)); |
|
1065 |
|
1066 |
|
1067 |
|
1068 XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX; |
|
1069 proof_timing:=true; |
|
1070 |
|
1071 (*Case where the key is secure*) |
|
1072 by (dres_inst_tac [("psi", "?X ~: ?H")] asm_rl 1); |
|
1073 by (asm_full_simp_tac |
|
1074 (!simpset addsimps [traces_ConsE RS insert_not_analyze_serverKey]) 1); |
|
1075 |
|
1076 |
|
1077 |
|
1078 by (full_simp_tac (!simpset addsimps [insert_Key_Agent_delay, |
|
1079 insert_Key_Crypt_delay]) 1); |
|
1080 |
|
1081 by (forward_tac [setOfList_I1 RS Says_Server_message_form] 1); |
|
1082 by (REPEAT_FIRST (eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac)); |
|
1083 |
|
1084 |
|
1085 by (asm_full_simp_tac |
|
1086 (!simpset addsimps [traces_ConsE RS insert_not_analyze_serverKey]) 1); |
|
1087 |
|
1088 |
|
1089 by (stac insert_commute 1); (*Pushes in the "insert X" for simplification*) |
|
1090 by (stac analyze_insert_Crypt 1); |
|
1091 |
|
1092 by (asm_full_simp_tac |
|
1093 (!simpset addsimps [insert_not_analyze_serverKey, |
|
1094 traces_ConsE RS insert_not_analyze_serverKey]) 1); |
|
1095 |
|
1096 |
|
1097 1. !!evs A B K NA S X evsa evs' ia evs'a. |
|
1098 [| i ~= k; j ~= k; |
|
1099 Says S (Friend ia) |
|
1100 (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey (Friend ia))) # |
|
1101 evs' : |
|
1102 traces; |
|
1103 Friend ia ~= B; |
|
1104 Says (Friend ia) Server {|Agent (Friend ia), Agent B, Nonce NA|} : |
|
1105 setOfList evs'; |
|
1106 Says Server (Friend i) |
|
1107 (Crypt |
|
1108 {|N, Agent (Friend j), Key (newK evs'a), |
|
1109 Crypt {|Key (newK evs'a), Agent (Friend i)|} |
|
1110 (serverKey (Friend j))|} |
|
1111 K') : |
|
1112 setOfList evs'; |
|
1113 Key (newK evs'a) ~: |
|
1114 analyze |
|
1115 (insert |
|
1116 (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey (Friend ia))) |
|
1117 (insert (Key (serverKey (Friend k))) (sees Enemy evs'))); |
|
1118 length evs'a < length evs' |] ==> |
|
1119 Key (newK evs'a) ~: |
|
1120 analyze |
|
1121 (insert X |
|
1122 (insert |
|
1123 (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey (Friend ia))) |
|
1124 (insert (Key (serverKey (Friend k))) (sees Enemy evs')))) |
|
1125 |
|
1126 |
|
1127 by (Asm_full_simp_tac 1); |
|
1128 |
|
1129 |
|
1130 by (Simp_tac 2); |
|
1131 |
|
1132 |
|
1133 by (Simp_tac 2); |
|
1134 |
|
1135 by (simp_tac (HOL_ss addsimps [insert_commute]) 2); |
|
1136 |
|
1137 |
|
1138 by (simp_tac (HOL_ss addsimps [analyze_insert_insert]) 2); |
|
1139 by (Asm_full_simp_tac 2); |
|
1140 by (simp_tac (!simpset addsimps [insert_absorb]) 2); |
|
1141 |
|
1142 |
|
1143 by (stac analyze_insert_Decrypt 2); |
|
1144 |
|
1145 |
|
1146 goal thy "analyze (insert X (insert Y H)) = analyze (insert X (analyze (insert Y H)))"; |
|
1147 br analyze_insert_cong 1; |
|
1148 by (Simp_tac 1); |
|
1149 qed "analyze_insert_insert"; |
|
1150 |
|
1151 |
|
1152 |
|
1153 |
|
1154 |
|
1155 |
|
1156 |
|
1157 1. !!evs A B K NA S X evsa evs' ia evs'a. |
|
1158 [| i ~= k; j ~= k; |
|
1159 Says S (Friend ia) |
|
1160 (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey (Friend ia))) # |
|
1161 evs' : |
|
1162 traces; |
|
1163 Friend ia ~= B; |
|
1164 Says (Friend ia) Server {|Agent (Friend ia), Agent B, Nonce NA|} : |
|
1165 setOfList evs'; |
|
1166 Says Server (Friend i) |
|
1167 (Crypt |
|
1168 {|N, Agent (Friend j), Key (newK evs'a), |
|
1169 Crypt {|Key (newK evs'a), Agent (Friend i)|} |
|
1170 (serverKey (Friend j))|} |
|
1171 K') : |
|
1172 setOfList evs'; |
|
1173 length evs'a < length evs'; ia ~= k; |
|
1174 Key (newK evs'a) ~: |
|
1175 analyze (insert (Key (serverKey (Friend k))) (sees Enemy evs')) |] ==> |
|
1176 Key (newK evs'a) ~: |
|
1177 analyze |
|
1178 (insert X |
|
1179 (insert |
|
1180 (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey (Friend ia))) |
|
1181 (insert (Key (serverKey (Friend k))) (sees Enemy evs')))) |
|
1182 |
|
1183 |
|
1184 by (ALLGOALS Asm_full_simp_tac); |
|
1185 |
|
1186 by (Asm_full_simp_tac 1); |
|
1187 |
|
1188 by (asm_simp_tac (!simpset addsimps [insert_not_analyze_serverKey]) 1); |
|
1189 fr insert_not_analyze_serverKey; |
|
1190 by (fast_tac (!claset addSEs [traces_ConsE]) 1); |
|
1191 |
|
1192 by (forward_tac [traces_ConsE] 1); |
|
1193 |
|
1194 |
|
1195 |
|
1196 by (asm_full_simp_tac (!simpset addsimps [analyze_subset_parts RS contra_subsetD]) 1); |
|
1197 |
|
1198 |
|
1199 |
|
1200 auto(); |
|
1201 |
|
1202 by (REPEAT_FIRST (resolve_tac [conjI, impI] (*DELETE NEXT TWO LINES??*) |
|
1203 ORELSE' eresolve_tac [conjE] |
|
1204 ORELSE' hyp_subst_tac)); |
|
1205 |
|
1206 by (forward_tac [Says_Server_message_form] 2); |
|
1207 |
|
1208 bd Says_Server_message_form 2; |
|
1209 by (fast_tac (!claset addSEs [traces_ConsE]) 2); |
|
1210 auto(); |
|
1211 by (ALLGOALS (full_simp_tac (!simpset addsimps [insert_Key_delay]))); |
|
1212 |
|
1213 (*SUBGOAL 1: use analyze_insert_Crypt to pull out |
|
1214 Crypt{|...|} (serverKey (Friend i)) |
|
1215 SUBGOAL 2: cannot do this, as we don't seem to have ia~=j |
|
1216 *) |
|
1217 |
|
1218 |
|
1219 |
|
1220 qed "Enemy_not_see_encrypted_key"; |
|
1221 |
|
1222 |
|
1223 goal thy |
|
1224 "!!evs. [| Says Server (Friend i) \ |
|
1225 \ (Crypt {|N, Agent B, K|} K') : setOfList evs; \ |
|
1226 \ evs : traces; i~=j \ |
|
1227 \ |] ==> K ~: analyze (sees (Friend j) evs)"; |
|
1228 br (sees_agent_subset_sees_Enemy RS analyze_mono RS contra_subsetD) 1; |
|
1229 by (ALLGOALS (asm_simp_tac (!simpset addsimps [Enemy_not_see_encrypted_key]))); |
|
1230 qed "Friend_not_see_encrypted_key"; |
|
1231 |
|
1232 goal thy |
|
1233 "!!evs. [| Says Server (Friend i) \ |
|
1234 \ (Crypt {|N, Agent B, K|} K') : setOfList evs; \ |
|
1235 \ A ~: {Friend i, Server}; \ |
|
1236 \ evs : traces \ |
|
1237 \ |] ==> K ~: analyze (sees A evs)"; |
|
1238 by (eres_inst_tac [("P", "A~:?X")] rev_mp 1); |
|
1239 by (agent.induct_tac "A" 1); |
|
1240 by (ALLGOALS Simp_tac); |
|
1241 by (asm_simp_tac (!simpset addsimps [eq_sym_conv, |
|
1242 Friend_not_see_encrypted_key]) 1); |
|
1243 br ([analyze_mono, Enemy_not_see_encrypted_key] MRS contra_subsetD) 1; |
|
1244 (* hyp_subst_tac would deletes the equality assumption... *) |
|
1245 by (ALLGOALS (rtac n_not_Suc_n ORELSE' Fast_tac)); |
|
1246 qed "Agent_not_see_encrypted_key"; |
|
1247 |
|
1248 |
|
1249 (*Neatly packaged, perhaps in a useless form*) |
|
1250 goalw thy [knownBy_def] |
|
1251 "!!evs. [| Says Server (Friend i) \ |
|
1252 \ (Crypt {|N, Agent B, K|} K') : setOfList evs; \ |
|
1253 \ evs : traces \ |
|
1254 \ |] ==> knownBy evs K <= {Friend i, Server}"; |
|
1255 |
|
1256 by (Step_tac 1); |
|
1257 br ccontr 1; |
|
1258 by (fast_tac (!claset addDs [Agent_not_see_encrypted_key]) 1); |
|
1259 qed "knownBy_encrypted_key"; |
|
1260 |
|
1261 |
320 |
1262 |
321 |
1263 |
322 XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX; |
1264 XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX; |
323 |
1265 |
324 ZZZZZZZZZZZZZZZZ; |
1266 ZZZZZZZZZZZZZZZZ; |