811 declare parts.Body [rule del] |
811 declare parts.Body [rule del] |
812 |
812 |
813 |
813 |
814 text{*Rewrites to push in Key and Crypt messages, so that other messages can |
814 text{*Rewrites to push in Key and Crypt messages, so that other messages can |
815 be pulled out using the @{text analz_insert} rules*} |
815 be pulled out using the @{text analz_insert} rules*} |
816 ML |
816 |
817 {* |
817 lemmas pushKeys [standard] = |
818 fun insComm x y = OldGoals.inst "x" x (OldGoals.inst "y" y insert_commute); |
818 insert_commute [of "Key K" "Agent C"] |
819 |
819 insert_commute [of "Key K" "Nonce N"] |
820 bind_thms ("pushKeys", |
820 insert_commute [of "Key K" "Number N"] |
821 map (insComm "Key ?K") |
821 insert_commute [of "Key K" "Pan PAN"] |
822 ["Agent ?C", "Nonce ?N", "Number ?N", "Pan ?PAN", |
822 insert_commute [of "Key K" "Hash X"] |
823 "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"]); |
823 insert_commute [of "Key K" "MPair X Y"] |
824 |
824 insert_commute [of "Key K" "Crypt X K'"] |
825 bind_thms ("pushCrypts", |
825 |
826 map (insComm "Crypt ?X ?K") |
826 lemmas pushCrypts [standard] = |
827 ["Agent ?C", "Nonce ?N", "Number ?N", "Pan ?PAN", |
827 insert_commute [of "Crypt X K" "Agent C"] |
828 "Hash ?X'", "MPair ?X' ?Y"]); |
828 insert_commute [of "Crypt X K" "Nonce N"] |
829 *} |
829 insert_commute [of "Crypt X K" "Number N"] |
|
830 insert_commute [of "Crypt X K" "Pan PAN"] |
|
831 insert_commute [of "Crypt X K" "Hash X'"] |
|
832 insert_commute [of "Crypt X K" "MPair X' Y"] |
830 |
833 |
831 text{*Cannot be added with @{text "[simp]"} -- messages should not always be |
834 text{*Cannot be added with @{text "[simp]"} -- messages should not always be |
832 re-ordered.*} |
835 re-ordered.*} |
833 lemmas pushes = pushKeys pushCrypts |
836 lemmas pushes = pushKeys pushCrypts |
834 |
837 |