equal
deleted
inserted
replaced
669 text{*A fresh N cannot be associated with any other |
669 text{*A fresh N cannot be associated with any other |
670 (with respect to a given trace). *} |
670 (with respect to a given trace). *} |
671 lemma N_fresh_not_KeyCryptNonce: |
671 lemma N_fresh_not_KeyCryptNonce: |
672 "\<forall>C. DK \<noteq> priEK C ==> Nonce N \<notin> used evs --> ~ KeyCryptNonce DK N evs" |
672 "\<forall>C. DK \<noteq> priEK C ==> Nonce N \<notin> used evs --> ~ KeyCryptNonce DK N evs" |
673 apply (induct_tac "evs") |
673 apply (induct_tac "evs") |
|
674 apply (rename_tac [2] a evs') |
674 apply (case_tac [2] "a") |
675 apply (case_tac [2] "a") |
675 apply (auto simp add: parts_insert2) |
676 apply (auto simp add: parts_insert2) |
676 done |
677 done |
677 |
678 |
678 lemma not_KeyCryptNonce_cardSK [rule_format (no_asm)]: |
679 lemma not_KeyCryptNonce_cardSK [rule_format (no_asm)]: |