835 |
835 |
836 subsection{*Tactics useful for many protocol proofs*} |
836 subsection{*Tactics useful for many protocol proofs*} |
837 (*<*) |
837 (*<*) |
838 ML |
838 ML |
839 {* |
839 {* |
840 structure MessageSET = |
|
841 struct |
|
842 |
|
843 (*Prove base case (subgoal i) and simplify others. A typical base case |
|
844 concerns Crypt K X \<notin> Key`shrK`bad and cannot be proved by rewriting |
|
845 alone.*) |
|
846 fun prove_simple_subgoals_tac (cs, ss) i = |
|
847 force_tac (cs, ss addsimps [@{thm image_eq_UN}]) i THEN |
|
848 ALLGOALS (asm_simp_tac ss) |
|
849 |
|
850 (*Analysis of Fake cases. Also works for messages that forward unknown parts, |
840 (*Analysis of Fake cases. Also works for messages that forward unknown parts, |
851 but this application is no longer necessary if analz_insert_eq is used. |
841 but this application is no longer necessary if analz_insert_eq is used. |
852 Abstraction over i is ESSENTIAL: it delays the dereferencing of claset |
842 Abstraction over i is ESSENTIAL: it delays the dereferencing of claset |
853 DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *) |
843 DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *) |
854 |
844 |
863 eresolve_tac [asm_rl, @{thm synth.Inj}]; |
853 eresolve_tac [asm_rl, @{thm synth.Inj}]; |
864 |
854 |
865 fun Fake_insert_simp_tac ss i = |
855 fun Fake_insert_simp_tac ss i = |
866 REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i; |
856 REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i; |
867 |
857 |
868 fun atomic_spy_analz_tac (cs,ss) = SELECT_GOAL |
858 fun atomic_spy_analz_tac ctxt = |
|
859 let val ss = simpset_of ctxt and cs = claset_of ctxt in |
|
860 SELECT_GOAL |
869 (Fake_insert_simp_tac ss 1 |
861 (Fake_insert_simp_tac ss 1 |
870 THEN |
862 THEN |
871 IF_UNSOLVED (Blast.depth_tac |
863 IF_UNSOLVED (Blast.depth_tac |
872 (cs addIs [@{thm analz_insertI}, |
864 (cs addIs [@{thm analz_insertI}, |
873 impOfSubs @{thm analz_subset_parts}]) 4 1)) |
865 impOfSubs @{thm analz_subset_parts}]) 4 1)) |
874 |
866 end; |
875 fun spy_analz_tac (cs,ss) i = |
867 |
876 DETERM |
868 fun spy_analz_tac ctxt i = |
877 (SELECT_GOAL |
869 let val ss = simpset_of ctxt and cs = claset_of ctxt in |
878 (EVERY |
870 DETERM |
879 [ (*push in occurrences of X...*) |
871 (SELECT_GOAL |
880 (REPEAT o CHANGED) |
872 (EVERY |
881 (res_inst_tac (Simplifier.the_context ss) |
873 [ (*push in occurrences of X...*) |
882 [(("x", 1), "X")] (insert_commute RS ssubst) 1), |
874 (REPEAT o CHANGED) |
883 (*...allowing further simplifications*) |
875 (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1), |
884 simp_tac ss 1, |
876 (*...allowing further simplifications*) |
885 REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])), |
877 simp_tac ss 1, |
886 DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i) |
878 REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])), |
887 |
879 DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i) |
888 end |
880 end; |
889 *} |
881 *} |
890 (*>*) |
882 (*>*) |
891 |
883 |
892 |
884 |
893 (*By default only o_apply is built-in. But in the presence of eta-expansion |
885 (*By default only o_apply is built-in. But in the presence of eta-expansion |
934 done |
926 done |
935 |
927 |
936 lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD] |
928 lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD] |
937 |
929 |
938 method_setup spy_analz = {* |
930 method_setup spy_analz = {* |
939 Scan.succeed (fn ctxt => |
931 Scan.succeed (SIMPLE_METHOD' o spy_analz_tac) *} |
940 SIMPLE_METHOD' (MessageSET.spy_analz_tac (clasimpset_of ctxt))) *} |
|
941 "for proving the Fake case when analz is involved" |
932 "for proving the Fake case when analz is involved" |
942 |
933 |
943 method_setup atomic_spy_analz = {* |
934 method_setup atomic_spy_analz = {* |
944 Scan.succeed (fn ctxt => |
935 Scan.succeed (SIMPLE_METHOD' o atomic_spy_analz_tac) *} |
945 SIMPLE_METHOD' (MessageSET.atomic_spy_analz_tac (clasimpset_of ctxt))) *} |
|
946 "for debugging spy_analz" |
936 "for debugging spy_analz" |
947 |
937 |
948 method_setup Fake_insert_simp = {* |
938 method_setup Fake_insert_simp = {* |
949 Scan.succeed (fn ctxt => |
939 Scan.succeed (SIMPLE_METHOD' o Fake_insert_simp_tac o simpset_of) *} |
950 SIMPLE_METHOD' (MessageSET.Fake_insert_simp_tac (simpset_of ctxt))) *} |
|
951 "for debugging spy_analz" |
940 "for debugging spy_analz" |
952 |
941 |
953 end |
942 end |