equal
deleted
inserted
replaced
678 txt{*fake*} |
678 txt{*fake*} |
679 apply blast |
679 apply blast |
680 txt{*K4*} |
680 txt{*K4*} |
681 apply (force dest!: Crypt_imp_keysFor) |
681 apply (force dest!: Crypt_imp_keysFor) |
682 txt{*K6*} |
682 txt{*K6*} |
683 apply (metis Says_imp_spies Says_ticket_parts analz.Fst analz.Inj analz_conj_parts unique_CryptKey) |
683 apply (metis MPair_parts Says_imp_parts_knows_Spy unique_CryptKey) |
684 done |
684 done |
685 |
685 |
686 text{*Needs a unicity theorem, hence moved here*} |
686 text{*Needs a unicity theorem, hence moved here*} |
687 lemma servK_authentic_ter: |
687 lemma servK_authentic_ter: |
688 "\<lbrakk> Says Kas A |
688 "\<lbrakk> Says Kas A |