785 declare parts.Body [rule del] |
785 declare parts.Body [rule del] |
786 |
786 |
787 |
787 |
788 text{*Rewrites to push in Key and Crypt messages, so that other messages can |
788 text{*Rewrites to push in Key and Crypt messages, so that other messages can |
789 be pulled out using the @{text analz_insert} rules*} |
789 be pulled out using the @{text analz_insert} rules*} |
790 ML |
790 |
791 {* |
791 lemmas pushKeys [standard] = |
792 fun insComm x y = OldGoals.inst "x" x (OldGoals.inst "y" y insert_commute); |
792 insert_commute [of "Key K" "Agent C"] |
793 |
793 insert_commute [of "Key K" "Nonce N"] |
794 bind_thms ("pushKeys", |
794 insert_commute [of "Key K" "Number N"] |
795 map (insComm "Key ?K") |
795 insert_commute [of "Key K" "Hash X"] |
796 ["Agent ?C", "Nonce ?N", "Number ?N", |
796 insert_commute [of "Key K" "MPair X Y"] |
797 "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"]); |
797 insert_commute [of "Key K" "Crypt X K'"] |
798 |
798 |
799 bind_thms ("pushCrypts", |
799 lemmas pushCrypts [standard] = |
800 map (insComm "Crypt ?X ?K") |
800 insert_commute [of "Crypt X K" "Agent C"] |
801 ["Agent ?C", "Nonce ?N", "Number ?N", |
801 insert_commute [of "Crypt X K" "Agent C"] |
802 "Hash ?X'", "MPair ?X' ?Y"]); |
802 insert_commute [of "Crypt X K" "Nonce N"] |
803 *} |
803 insert_commute [of "Crypt X K" "Number N"] |
|
804 insert_commute [of "Crypt X K" "Hash X'"] |
|
805 insert_commute [of "Crypt X K" "MPair X' Y"] |
804 |
806 |
805 text{*Cannot be added with @{text "[simp]"} -- messages should not always be |
807 text{*Cannot be added with @{text "[simp]"} -- messages should not always be |
806 re-ordered. *} |
808 re-ordered. *} |
807 lemmas pushes = pushKeys pushCrypts |
809 lemmas pushes = pushKeys pushCrypts |
808 |
810 |