827 re-ordered.*} |
827 re-ordered.*} |
828 lemmas pushes = pushKeys pushCrypts |
828 lemmas pushes = pushKeys pushCrypts |
829 |
829 |
830 |
830 |
831 subsection{*Tactics useful for many protocol proofs*} |
831 subsection{*Tactics useful for many protocol proofs*} |
|
832 (*<*) |
832 ML |
833 ML |
833 {* |
834 {* |
834 val invKey = thm "invKey" |
|
835 val keysFor_def = thm "keysFor_def" |
|
836 val symKeys_def = thm "symKeys_def" |
|
837 val parts_mono = thm "parts_mono"; |
|
838 val analz_mono = thm "analz_mono"; |
|
839 val Key_image_eq = thm "Key_image_eq"; |
|
840 val Nonce_Key_image_eq = thm "Nonce_Key_image_eq"; |
|
841 val keysFor_Un = thm "keysFor_Un"; |
|
842 val keysFor_mono = thm "keysFor_mono"; |
|
843 val keysFor_image_Key = thm "keysFor_image_Key"; |
|
844 val Crypt_imp_invKey_keysFor = thm "Crypt_imp_invKey_keysFor"; |
|
845 val MPair_parts = thm "MPair_parts"; |
|
846 val parts_increasing = thm "parts_increasing"; |
|
847 val parts_insertI = thm "parts_insertI"; |
|
848 val parts_empty = thm "parts_empty"; |
|
849 val parts_emptyE = thm "parts_emptyE"; |
|
850 val parts_singleton = thm "parts_singleton"; |
|
851 val parts_Un_subset1 = thm "parts_Un_subset1"; |
|
852 val parts_Un_subset2 = thm "parts_Un_subset2"; |
|
853 val parts_insert = thm "parts_insert"; |
|
854 val parts_insert2 = thm "parts_insert2"; |
|
855 val parts_UN_subset1 = thm "parts_UN_subset1"; |
|
856 val parts_UN_subset2 = thm "parts_UN_subset2"; |
|
857 val parts_UN = thm "parts_UN"; |
|
858 val parts_insert_subset = thm "parts_insert_subset"; |
|
859 val parts_partsD = thm "parts_partsD"; |
|
860 val parts_trans = thm "parts_trans"; |
|
861 val parts_cut = thm "parts_cut"; |
|
862 val parts_cut_eq = thm "parts_cut_eq"; |
|
863 val parts_insert_eq_I = thm "parts_insert_eq_I"; |
|
864 val parts_image_Key = thm "parts_image_Key"; |
|
865 val MPair_analz = thm "MPair_analz"; |
|
866 val analz_increasing = thm "analz_increasing"; |
835 val analz_increasing = thm "analz_increasing"; |
867 val analz_subset_parts = thm "analz_subset_parts"; |
836 val analz_subset_parts = thm "analz_subset_parts"; |
868 val not_parts_not_analz = thm "not_parts_not_analz"; |
|
869 val parts_analz = thm "parts_analz"; |
837 val parts_analz = thm "parts_analz"; |
870 val analz_parts = thm "analz_parts"; |
838 val analz_parts = thm "analz_parts"; |
871 val analz_insertI = thm "analz_insertI"; |
839 val analz_insertI = thm "analz_insertI"; |
872 val analz_empty = thm "analz_empty"; |
|
873 val analz_Un = thm "analz_Un"; |
|
874 val analz_insert_Crypt_subset = thm "analz_insert_Crypt_subset"; |
|
875 val analz_image_Key = thm "analz_image_Key"; |
|
876 val analz_analzD = thm "analz_analzD"; |
|
877 val analz_trans = thm "analz_trans"; |
|
878 val analz_cut = thm "analz_cut"; |
|
879 val analz_insert_eq = thm "analz_insert_eq"; |
|
880 val analz_subset_cong = thm "analz_subset_cong"; |
|
881 val analz_cong = thm "analz_cong"; |
|
882 val analz_insert_cong = thm "analz_insert_cong"; |
|
883 val analz_trivial = thm "analz_trivial"; |
|
884 val analz_UN_analz = thm "analz_UN_analz"; |
|
885 val synth_mono = thm "synth_mono"; |
|
886 val synth_increasing = thm "synth_increasing"; |
|
887 val synth_Un = thm "synth_Un"; |
|
888 val synth_insert = thm "synth_insert"; |
|
889 val synth_synthD = thm "synth_synthD"; |
|
890 val synth_trans = thm "synth_trans"; |
|
891 val synth_cut = thm "synth_cut"; |
|
892 val Agent_synth = thm "Agent_synth"; |
|
893 val Number_synth = thm "Number_synth"; |
|
894 val Nonce_synth_eq = thm "Nonce_synth_eq"; |
|
895 val Key_synth_eq = thm "Key_synth_eq"; |
|
896 val Crypt_synth_eq = thm "Crypt_synth_eq"; |
|
897 val keysFor_synth = thm "keysFor_synth"; |
|
898 val parts_synth = thm "parts_synth"; |
|
899 val analz_analz_Un = thm "analz_analz_Un"; |
|
900 val analz_synth_Un = thm "analz_synth_Un"; |
|
901 val analz_synth = thm "analz_synth"; |
|
902 val parts_insert_subset_Un = thm "parts_insert_subset_Un"; |
|
903 val Fake_parts_insert = thm "Fake_parts_insert"; |
840 val Fake_parts_insert = thm "Fake_parts_insert"; |
904 val Fake_analz_insert = thm "Fake_analz_insert"; |
841 val Fake_analz_insert = thm "Fake_analz_insert"; |
905 val analz_conj_parts = thm "analz_conj_parts"; |
|
906 val analz_disj_parts = thm "analz_disj_parts"; |
|
907 val MPair_synth_analz = thm "MPair_synth_analz"; |
|
908 val Crypt_synth_analz = thm "Crypt_synth_analz"; |
|
909 val Hash_synth_analz = thm "Hash_synth_analz"; |
|
910 val pushes = thms "pushes"; |
|
911 |
|
912 |
842 |
913 (*Prove base case (subgoal i) and simplify others. A typical base case |
843 (*Prove base case (subgoal i) and simplify others. A typical base case |
914 concerns Crypt K X \<notin> Key`shrK`bad and cannot be proved by rewriting |
844 concerns Crypt K X \<notin> Key`shrK`bad and cannot be proved by rewriting |
915 alone.*) |
845 alone.*) |
916 fun prove_simple_subgoals_tac i = |
846 fun prove_simple_subgoals_tac i = |