(* (C) Copyright Andreas Viktor Hess, DTU, 2015-2018 All Rights Reserved. Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: - Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. - Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. - Neither the name of the copyright holder nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) (* Title: IntruderDeduction.thy Author: Andreas Viktor Hess, DTU *) section {* Theory: Dolev-Yao Intruder Model *} theory IntruderDeduction imports Messages Unification2 begin subsection {* Dolev-Yao intruder model locale *} locale intruder_model = fixes arity :: "'fun::countable \ nat" and public :: "'fun \ bool" and Ana :: "('fun,'var::countable) term \ (('fun,'var) terms \ ('fun,'var) terms)" assumes Ana_keys_FV: "\t K T. Ana t = (K,T) \ FV\<^sub>s\<^sub>e\<^sub>t K \ FV t" and Ana_keys_finite: "\t K T. Ana t = (K,T) \ finite K" and Ana_keys_wf: "\t k K T f S. Ana t = (K,T) \ (\g S'. Fun g S' \ t \ length S' = arity g) \ k \ K \ Fun f S \ k \ length S = arity f" and Ana_var[simp]: "\x. Ana (Var x) = ({},{})" and Ana_fun_subterm: "\f X K T. Ana (Fun f X) = (K,T) \ T \ set X" and Ana_subst: "\t \ K M. \Ana t = (K,M); K \ {} \ M \ {}\ \ Ana (t \ \) = (K \set \,M \set \)" and infinite_vars[simp]: "infinite (UNIV::'var set)" and infinite_public_consts[simp]: "infinite {c. public c \ arity c = 0}" and no_private_funs[simp]: "\f. arity f > 0 \ public f" begin lemma Ana_subterm: assumes "Ana t = (K,T)" shows "T \ subterms t" proof (cases t) case Var thus ?thesis using Ana_var assms by auto next case Fun thus ?thesis using Ana_fun_subterm assms by force qed lemma Ana_finite: assumes "Ana t = (K,M)" shows "finite K" "finite M" by (metis Ana_keys_finite[OF assms], metis Ana_subterm[OF assms] finite_Un subterms_finite sup.strict_order_iff) lemma Ana_vars: assumes "Ana t = (K,M)" shows "FV\<^sub>s\<^sub>e\<^sub>t K \ FV t" "FV\<^sub>s\<^sub>e\<^sub>t M \ FV t" apply (rule Ana_keys_FV[OF assms]) using Ana_subterm[OF assms] subtermeqI[THEN subtermeq_vars_subset] by auto definition \ where "\ \ UNIV::'var set" definition \n ("\\<^sup>_") where "\\<^sup>n \ {f::'fun. arity f = n}" definition \npub ("\\<^sub>p\<^sub>u\<^sub>b\<^sup>_") where "\\<^sub>p\<^sub>u\<^sub>b\<^sup>n \ {f. public f} \ \\<^sup>n" definition \npriv ("\\<^sub>p\<^sub>r\<^sub>i\<^sub>v\<^sup>_") where "\\<^sub>p\<^sub>r\<^sub>i\<^sub>v\<^sup>n \ {f. \public f} \ \\<^sup>n" definition \\<^sub>p\<^sub>u\<^sub>b where "\\<^sub>p\<^sub>u\<^sub>b \ (\n. \\<^sub>p\<^sub>u\<^sub>b\<^sup>n)" definition \\<^sub>p\<^sub>r\<^sub>i\<^sub>v where "\\<^sub>p\<^sub>r\<^sub>i\<^sub>v \ (\n. \\<^sub>p\<^sub>r\<^sub>i\<^sub>v\<^sup>n)" definition \ where "\ \ (\n. \\<^sup>n)" definition \ where "\ \ \\<^sup>0" definition \\<^sub>p\<^sub>u\<^sub>b where "\\<^sub>p\<^sub>u\<^sub>b \ {f. public f} \ \" definition \\<^sub>p\<^sub>r\<^sub>i\<^sub>v where "\\<^sub>p\<^sub>r\<^sub>i\<^sub>v \ {f. \public f} \ \" definition \\<^sub>f where "\\<^sub>f \ \ - \" definition \\<^sub>f\<^sub>p\<^sub>u\<^sub>b where "\\<^sub>f\<^sub>p\<^sub>u\<^sub>b \ \\<^sub>f \ \\<^sub>p\<^sub>u\<^sub>b" definition \\<^sub>f\<^sub>p\<^sub>r\<^sub>i\<^sub>v where "\\<^sub>f\<^sub>p\<^sub>r\<^sub>i\<^sub>v \ \\<^sub>f \ \\<^sub>p\<^sub>r\<^sub>i\<^sub>v" declare \_def[simp] \n_def[simp] \npub_def[simp] \npriv_def[simp] \\<^sub>p\<^sub>u\<^sub>b_def[simp] \\<^sub>p\<^sub>r\<^sub>i\<^sub>v_def[simp] \_def[simp] \_def[simp] \\<^sub>p\<^sub>u\<^sub>b_def[simp] \\<^sub>p\<^sub>r\<^sub>i\<^sub>v_def[simp] \\<^sub>f_def[simp] \\<^sub>f\<^sub>p\<^sub>u\<^sub>b_def[simp] \\<^sub>f\<^sub>p\<^sub>r\<^sub>i\<^sub>v_def[simp] lemma disjoint_fun_syms: "\\<^sub>f \ \ = {}" by auto lemma id_union_univ: "\\<^sub>f \ \ = UNIV" "\ = UNIV" by auto lemma const_arity_eq_zero[dest]: "c \ \ \ arity c = 0" by simp lemma const_pub_arity_eq_zero[dest]: "c \ \\<^sub>p\<^sub>u\<^sub>b \ arity c = 0 \ public c" by simp lemma const_priv_arity_eq_zero[dest]: "c \ \\<^sub>p\<^sub>r\<^sub>i\<^sub>v \ arity c = 0 \ \public c" by simp lemma fun_arity_gt_zero[dest]: "f \ \\<^sub>f \ arity f > 0" by fastforce lemma pub_fun_public[dest]: "f \ \\<^sub>f\<^sub>p\<^sub>u\<^sub>b \ public f" by fastforce lemma pub_fun_arity_gt_zero[dest]: "f \ \\<^sub>f\<^sub>p\<^sub>u\<^sub>b \ arity f > 0" by fastforce lemma countable_vars[simp]: "countable \" by (rule countableI_type) lemma countable_fun_syms[simp]: "countable \\<^sub>f" "countable \" "countable (UNIV::'fun set)" by (rule countableI_type)+ lemma \\<^sub>f_unfold: "\\<^sub>f = {f::'fun. arity f > 0}" by auto lemma \_unfold: "\ = {f::'fun. arity f = 0}" by auto lemma \pub_unfold: "\\<^sub>p\<^sub>u\<^sub>b = {f::'fun. arity f = 0 \ public f}" by auto lemma \priv_unfold: "\\<^sub>p\<^sub>r\<^sub>i\<^sub>v = {f::'fun. arity f = 0 \ \public f}" by auto lemma \npub_unfold: "\\<^sub>p\<^sub>u\<^sub>b\<^sup>n = {f::'fun. arity f = n \ public f}" by auto lemma \npriv_unfold: "\\<^sub>p\<^sub>r\<^sub>i\<^sub>v\<^sup>n = {f::'fun. arity f = n \ \public f}" by auto lemma \fpub_unfold: "\\<^sub>f\<^sub>p\<^sub>u\<^sub>b = {f::'fun. arity f > 0 \ public f}" by auto lemma \fpriv_unfold: "\\<^sub>f\<^sub>p\<^sub>r\<^sub>i\<^sub>v = {f::'fun. arity f > 0 \ \public f}" by auto lemma \n_m_eq: "\(\\<^sup>n) \ {}; (\\<^sup>n) = (\\<^sup>m)\ \ n = m" by auto lemma infinite_fun_syms[simp]: "infinite {c. public c \ arity c > 0} \ infinite \\<^sub>f" "infinite \" "infinite \\<^sub>p\<^sub>u\<^sub>b" "infinite (UNIV::'fun set)" using finite_Collect_conjI infinite_public_consts apply (metis \\<^sub>f_unfold, metis \n_def \_def) using infinite_public_consts \pub_unfold apply (simp add: Collect_conj_eq) by (metis UNIV_I finite_subset subsetI infinite_public_consts(1)) lemma id_univ_proper_subset[simp]: "\\<^sub>f \ UNIV" "(\f. arity f > 0) \ \ \ UNIV" using finite.emptyI inf_top.right_neutral top.not_eq_extremum apply (metis disjoint_fun_syms infinite_fun_syms(2) inf_commute) by (metis top.not_eq_extremum UNIV_I const_arity_eq_zero less_irrefl) subsubsection {* Term well-formedness *} definition wf\<^sub>t\<^sub>r\<^sub>m where "wf\<^sub>t\<^sub>r\<^sub>m t \ \f T. Fun f T \ t \ length T = arity f" lemma Ana_keys_wf': "Ana t = (K,T) \ wf\<^sub>t\<^sub>r\<^sub>m t \ k \ K \ wf\<^sub>t\<^sub>r\<^sub>m k" using Ana_keys_wf unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by metis lemma wf_trm_Var[simp]: "wf\<^sub>t\<^sub>r\<^sub>m (Var x)" unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by simp lemma wf_trm_img_subst: "(\t \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \. wf\<^sub>t\<^sub>r\<^sub>m t) \ wf\<^sub>t\<^sub>r\<^sub>m (\ v)" unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by (cases "\ v \ img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \") auto lemma wf_trmI[intro]: assumes "\x. x \ set X \ wf\<^sub>t\<^sub>r\<^sub>m x" "length X = arity f" shows "wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)" using assms unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto lemma wf_trm_subst: assumes "\v. wf\<^sub>t\<^sub>r\<^sub>m (\ v)" "wf\<^sub>t\<^sub>r\<^sub>m t" shows "wf\<^sub>t\<^sub>r\<^sub>m (t \ \)" using \wf\<^sub>t\<^sub>r\<^sub>m t\ proof (induction t) case (Fun f X) hence "\x. x \ set X \ wf\<^sub>t\<^sub>r\<^sub>m x" by (meson wf\<^sub>t\<^sub>r\<^sub>m_def Fun_param_is_subterm subtermeq_trans subtermseq_if_subterms) hence "\x. x \ set X \ wf\<^sub>t\<^sub>r\<^sub>m (x \ \)" using Fun.IH by auto moreover have "length (map (\x. x \ \) X) = arity f" using \wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)\ unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto ultimately show ?case by fastforce qed (simp add: \\v. wf\<^sub>t\<^sub>r\<^sub>m (\ v)\) lemma wf_trm_subst_singleton: assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "wf\<^sub>t\<^sub>r\<^sub>m t'" shows "wf\<^sub>t\<^sub>r\<^sub>m (t \ Var(v := t'))" proof - have "\w. wf\<^sub>t\<^sub>r\<^sub>m ((Var(v := t')) w)" using \wf\<^sub>t\<^sub>r\<^sub>m t'\ unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by simp thus ?thesis using wf_trm_subst[OF _ \wf\<^sub>t\<^sub>r\<^sub>m t\, of "Var(v := t')"] by simp qed lemma wf_trm_subterm: "\wf\<^sub>t\<^sub>r\<^sub>m t; s \ t\ \ wf\<^sub>t\<^sub>r\<^sub>m s" unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by (induct t) auto lemma wf_trm_subtermeq: assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "s \ t" shows "wf\<^sub>t\<^sub>r\<^sub>m s" proof (cases "s = t") case False thus "wf\<^sub>t\<^sub>r\<^sub>m s" using assms(2) wf_trm_subterm[OF assms(1)] by simp qed (metis assms(1)) lemma unify_list_wf_trm: assumes "Unification.unify E B = Some U" "\(s,t) \ set E. wf\<^sub>t\<^sub>r\<^sub>m s \ wf\<^sub>t\<^sub>r\<^sub>m t" and "\(v,t) \ set B. wf\<^sub>t\<^sub>r\<^sub>m t" shows "\(v,t) \ set U. wf\<^sub>t\<^sub>r\<^sub>m t" using assms proof (induction E B arbitrary: U rule: Unification.unify.induct) case (1 B U) thus ?case by auto next case (2 f X g Y E B U) have wf_fun: "wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)" "wf\<^sub>t\<^sub>r\<^sub>m (Fun g Y)" using "2.prems"(2) by auto from "2.prems"(1) obtain E' where *: "decompose (Fun f X) (Fun g Y) = Some E'" and [simp]: "f = g" "length X = length Y" "E' = zip X Y" and **: "Unification.unify (E'@E) B = Some U" by (auto split: option.splits) hence "\t t'. (t,t') \ set E' \ t \ Fun f X \ t' \ Fun g Y" by (metis zip_arg_subterm) hence "\t t'. (t,t') \ set E' \ wf\<^sub>t\<^sub>r\<^sub>m t \ wf\<^sub>t\<^sub>r\<^sub>m t'" using wf_trm_subterm wf_fun \f = g\ by blast+ thus ?case using "2.IH"[OF * ** _ "2.prems"(3)] "2.prems"(2) by fastforce next case (3 v t E B) hence *: "\(w,x) \ set ((v, t) # B). wf\<^sub>t\<^sub>r\<^sub>m x" and **: "\(s,t) \ set E. wf\<^sub>t\<^sub>r\<^sub>m s \ wf\<^sub>t\<^sub>r\<^sub>m t" "wf\<^sub>t\<^sub>r\<^sub>m t" by auto show ?case proof (cases "t = Var v") case True thus ?thesis using "3.prems" "3.IH"(1) by auto next case False hence "v \ FV t" using "3.prems"(1) by auto hence "Unification.unify (subst_list (subst v t) E) ((v, t)#B) = Some U" using \t \ Var v\ "3.prems"(1) by auto moreover have "\(s, t) \ set (subst_list (subst v t) E). wf\<^sub>t\<^sub>r\<^sub>m s \ wf\<^sub>t\<^sub>r\<^sub>m t" using wf_trm_subst_singleton[OF _ \wf\<^sub>t\<^sub>r\<^sub>m t\] "3.prems"(2) unfolding subst_list_def subst_def by auto ultimately show ?thesis using "3.IH"(2)[OF \t \ Var v\ \v \ FV t\ _ _ *] by metis qed next case (4 f X v E B U) hence *: "\(w,x) \ set ((v, Fun f X) # B). wf\<^sub>t\<^sub>r\<^sub>m x" and **: "\(s,t) \ set E. wf\<^sub>t\<^sub>r\<^sub>m s \ wf\<^sub>t\<^sub>r\<^sub>m t" "wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)" by auto have "v \ FV (Fun f X)" using "4.prems"(1) by force hence "Unification.unify (subst_list (subst v (Fun f X)) E) ((v, Fun f X)#B) = Some U" using "4.prems"(1) by auto moreover have "\(s, t) \ set (subst_list (subst v (Fun f X)) E). wf\<^sub>t\<^sub>r\<^sub>m s \ wf\<^sub>t\<^sub>r\<^sub>m t" using wf_trm_subst_singleton[OF _ \wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)\] "4.prems"(2) unfolding subst_list_def subst_def by auto ultimately show ?case using "4.IH"[OF \v \ FV (Fun f X)\ _ _ *] by metis qed lemma mgu_wf_trm: assumes "mgu s t = Some \" "wf\<^sub>t\<^sub>r\<^sub>m s" "wf\<^sub>t\<^sub>r\<^sub>m t" shows "wf\<^sub>t\<^sub>r\<^sub>m (\ v)" proof - from assms obtain \' where "subst_of \' = \" "\(v,t) \ set \'. wf\<^sub>t\<^sub>r\<^sub>m t" using unify_list_wf_trm[of "[(s,t)]" "[]"] by (auto split: option.splits) thus ?thesis proof (induction \' arbitrary: \ v rule: List.rev_induct) case (snoc x \' \ v) def \ \ "subst_of \'" hence "\v. wf\<^sub>t\<^sub>r\<^sub>m (\ v)" using snoc.prems(2) snoc.IH[of \] by fastforce moreover obtain w t where x: "x = (w,t)" by (metis surj_pair) hence \: "\ = Var(w := t) \\<^sub>s \" using snoc.prems(1) by (simp add: subst_def \_def) moreover have "wf\<^sub>t\<^sub>r\<^sub>m t" using snoc.prems(2) x by auto ultimately show ?case by (simp add: subst_compose_def wf_trm_subst) qed (simp add: wf\<^sub>t\<^sub>r\<^sub>m_def) qed subsubsection {* Transparent function decomposition *} definition transparent::"'fun \ bool" where "transparent f \ public f \ f \ \\<^sub>f \ (\X. Ana (Fun f X) = ({},set X))" definition \\<^sub>t\<^sub>r\<^sub>p where "\\<^sub>t\<^sub>r\<^sub>p \ {f. transparent f}" declare \\<^sub>t\<^sub>r\<^sub>p_def[simp] lemma transp_public[dest]: "transparent f \ public f" by (metis transparent_def) lemma transp_fun[dest]: "transparent f \ f \ \\<^sub>f" by (metis transparent_def) lemma transp_Ana[dest]: "transparent f \ Ana (Fun f X) = ({},set X)" by (metis transparent_def) fun trp::"('fun,'var) term \ ('fun,'var) terms" where "trp (Var x) = {Var x}" | "trp (Fun f X) = insert (Fun f X) (if transparent f then \x \ set X. trp x else {})" abbreviation trp\<^sub>s\<^sub>e\<^sub>t where "trp\<^sub>s\<^sub>e\<^sub>t S \ \(trp ` S)" abbreviation subterm\<^sub>t\<^sub>r\<^sub>p (infix "\\<^sub>t\<^sub>r\<^sub>p" 50) where "t \\<^sub>t\<^sub>r\<^sub>p t' \ t \ trp t'" lemma finite_trp[simp]: "finite (trp t)" by (induct t rule: trp.induct) auto lemma trp_refl[simp]: "t \\<^sub>t\<^sub>r\<^sub>p t" by (induct t rule: trp.induct) simp_all lemma trp_subst_apply_subset: "(trp t) \set \ \ trp (t \ \)" by (induct t, auto) lemma trp_subterms_subset: "trp t \ subterms t" by (induct t) auto lemma trpD[dest?]: "t \\<^sub>t\<^sub>r\<^sub>p t' \ t \ t'" by (induct t' rule: subterms.induct, auto, meson UN_E empty_iff) lemma trpI[intro?]: "t \ M \ t \ trp\<^sub>s\<^sub>e\<^sub>t M" by fastforce lemma trpI'[intro?]: "\transparent f; t \ set X\ \ t \\<^sub>t\<^sub>r\<^sub>p Fun f X" by force lemma trp_mono: "M \ M' \ trp\<^sub>s\<^sub>e\<^sub>t M \ trp\<^sub>s\<^sub>e\<^sub>t M'" by auto lemma trp_FV_is_trm_FV: "FV\<^sub>s\<^sub>e\<^sub>t (trp t) = FV t" by (induct t) auto lemma trp_union_FV_is_set_FV: "FV\<^sub>s\<^sub>e\<^sub>t (trp\<^sub>s\<^sub>e\<^sub>t M) = FV\<^sub>s\<^sub>e\<^sub>t M" using trp_FV_is_trm_FV by auto lemma trp_member_FV: "t \ trp\<^sub>s\<^sub>e\<^sub>t M \ FV t \ FV\<^sub>s\<^sub>e\<^sub>t M" by (metis FV\<^sub>s\<^sub>e\<^sub>t_def UN_upper trp_union_FV_is_set_FV) lemma trp_subst_apply_subset_set: "trp\<^sub>s\<^sub>e\<^sub>t S \set \ \ trp\<^sub>s\<^sub>e\<^sub>t (S \set \)" proof fix x assume "x \ trp\<^sub>s\<^sub>e\<^sub>t S \set \" then obtain y z where "trp z \ trp\<^sub>s\<^sub>e\<^sub>t S" "x = y \ \" "y \\<^sub>t\<^sub>r\<^sub>p z" "z \ S" by auto hence "x \ trp z \set \" by simp hence "x \\<^sub>t\<^sub>r\<^sub>p (z \ \)" using trp_subst_apply_subset by auto thus "x \ trp\<^sub>s\<^sub>e\<^sub>t (S \set \)" using \z \ S\ by auto qed lemma trp_fun_member: assumes "t \\<^sub>t\<^sub>r\<^sub>p (Fun f X)" "t \ Fun f X" shows "transparent f" "\x \ set X. t \\<^sub>t\<^sub>r\<^sub>p x" proof - have "t \ {Fun f X}" using assms(2) by simp thus "transparent f" using assms(1) by fastforce thus "\x \ set X. t \\<^sub>t\<^sub>r\<^sub>p x" using assms by auto qed lemma trp_member_trp_subset: "t \\<^sub>t\<^sub>r\<^sub>p t' \ trp t \ trp t'" proof (induction t' rule: trp.induct) case (2 f X) thus ?case by (cases "transparent f") auto qed simp lemma trp_member_trp_subset_union: "t \ trp\<^sub>s\<^sub>e\<^sub>t M \ trp t \ trp\<^sub>s\<^sub>e\<^sub>t M" using trp_mono trp_member_trp_subset by fastforce lemma trp_member_trp_subset_union_subst: "t \ trp\<^sub>s\<^sub>e\<^sub>t M \ trp (t \ \) \ trp\<^sub>s\<^sub>e\<^sub>t (M \set \)" using trp_subst_apply_subset_set[of \ M] by (force intro!: trp_member_trp_subset_union) lemma trp_var_is_FV[dest?]: "Var v \\<^sub>t\<^sub>r\<^sub>p t \ v \ FV t" using trpD vars_iff_subtermeq by metis subsubsection {* Intruder Deduction Definitions *} inductive intruder_synth::"('fun,'var) terms \ ('fun,'var) term \ bool" (infix "\\<^sub>c" 50) where AxiomC[simp]: "t \ M \ M \\<^sub>c t" | ComposeC[simp]: "\length X = arity f; public f; \x. x \ (set X) \ M \\<^sub>c x\ \ M \\<^sub>c Fun f X" inductive intruder_deduct::"('fun,'var) terms \ ('fun,'var) term \ bool" (infix "\" 50) where Axiom[simp]: "t \ M \ M \ t" | Compose[simp]: "\length X = arity f; public f; \x. x \ set X \ M \ x\ \ M \ Fun f X" | Decompose: "\M \ t; Ana t = (K, T); \k. k \ K \ M \ k; t\<^sub>i \ T\ \ M \ t\<^sub>i" definition analyzed::"('fun,'var) terms \ bool" where "analyzed M \ \t. M \ t \ M \\<^sub>c t" definition decomp_closure::"('fun,'var) terms \ ('fun,'var) terms \ bool" where "decomp_closure M M' \ \t. M \ t \ (\t' \ M. t \ t') \ t \ M'" inductive public_ground_wf_term::"('fun,'var) term \ bool" where PGWT[simp]: "\public f; arity f = length X; \x. x \ set X \ public_ground_wf_term x\ \ public_ground_wf_term (Fun f X)" abbreviation "public_ground_wf_terms \ {t. public_ground_wf_term t}" lemma pgwt_infinite: "infinite public_ground_wf_terms" proof - let ?F = "(\c. Fun c []) ` \\<^sub>p\<^sub>u\<^sub>b" have "\f. bij_betw f \\<^sub>p\<^sub>u\<^sub>b ?F" using bij_betwI'[of \\<^sub>p\<^sub>u\<^sub>b _ ?F] by fastforce hence "infinite ?F" by (metis bij_betw_finite infinite_fun_syms(3)) moreover have "?F \ public_ground_wf_terms" using \pub_unfold public_ground_wf_term.intros[of _ "[]"] by fastforce ultimately show ?thesis using infinite_super by blast qed declare analyzed_def[simp] declare decomp_closure_def[simp] lemma public_const_deduct: assumes "c \ \\<^sub>p\<^sub>u\<^sub>b" shows "M \ Fun c []" "M \\<^sub>c Fun c []" proof - have "arity c = 0" "public c" using const_arity_eq_zero \c \ \\<^sub>p\<^sub>u\<^sub>b\ by auto thus "M \ Fun c []" "M \\<^sub>c Fun c []" using intruder_synth.ComposeC[OF _ \public c\, of "[]"] intruder_deduct.Compose[OF _ \public c\, of "[]"] by auto qed lemma public_const_deduct'[simp]: assumes "arity c = 0" "public c" shows "M \ Fun c []" "M \\<^sub>c Fun c []" using intruder_deduct.Compose[of "[]" c] intruder_synth.ComposeC[of "[]" c] assms by simp_all lemma pgwt_public: "\public_ground_wf_term t; Fun f X \ t\ \ public f" by (induct t rule: public_ground_wf_term.induct) auto lemma pgwt_ground: "public_ground_wf_term t \ FV t = {}" by (induct t rule: public_ground_wf_term.induct) auto lemma pgwt_fun: "public_ground_wf_term t \ \f X. t = Fun f X" using pgwt_ground[of t] by (cases t) auto lemma pgwt_arity: "\public_ground_wf_term t; Fun f X \ t\ \ arity f = length X" by (induct t rule: public_ground_wf_term.induct) auto lemma pgwt_wellformed: "public_ground_wf_term t \ wf\<^sub>t\<^sub>r\<^sub>m t" by (induct t rule: public_ground_wf_term.induct) auto lemma pgwt_deducible: "public_ground_wf_term t \ M \\<^sub>c t" by (induct t rule: public_ground_wf_term.induct) auto lemma pgwt_is_empty_synth: "public_ground_wf_term t \ {} \\<^sub>c t" proof - { fix M::"('fun,'var) term set" assume "M \\<^sub>c t" "M = {}" hence "public_ground_wf_term t" by (induct t rule: intruder_synth.induct) auto } thus ?thesis using pgwt_deducible by auto qed lemma trp_deduct_decompose: assumes "s \\<^sub>t\<^sub>r\<^sub>p t" "M \ t" shows "M \ s" using assms proof (induction t rule: trp.induct) case (2 f X) thus ?case proof (cases "s = Fun f X") case False then obtain x where x: "transparent f" "x \ set X" "s \\<^sub>t\<^sub>r\<^sub>p x" using "2.prems"(1) trp_fun_member by blast hence "Ana (Fun f X) = ({},set X)" unfolding transparent_def by auto hence "M \ x" using Decompose[OF \M \ Fun f X\ _ _ \x \ set X\] by auto thus ?thesis using "2.IH"[OF x] by metis qed simp qed simp lemma trp_deduct_decompose': assumes "trp\<^sub>s\<^sub>e\<^sub>t M \ t" shows "M \ t" proof - { fix M' assume "M' \ t" "M' = trp\<^sub>s\<^sub>e\<^sub>t M" hence "M \ t" proof (induction t rule: intruder_deduct.induct) case (Decompose M' t K T t') hence "\k. k \ K \ M \ k" "M \ t" by auto thus ?case using intruder_deduct.Decompose[of M t K T] \Ana t = (K, T)\ \t' \ T\ by metis qed (auto simp add: trp_deduct_decompose) } thus ?thesis using assms by simp qed lemma ideduct_synth_subst_apply: assumes "{} \\<^sub>c t" "\v. M \\<^sub>c \ v" shows "M \\<^sub>c t \ \" proof - { fix M'::"('fun,'var) term set" assume "M' \\<^sub>c t" "M' = {}" hence "M \\<^sub>c t \ \" proof (induction t rule: intruder_synth.induct) case (ComposeC X f M') hence "length (map (\t. t \ \) X) = arity f" "\x. x \ set (map (\t. t \ \) X) \ M \\<^sub>c x" by auto thus ?case using intruder_synth.ComposeC[of "map (\t. t \ \) X" f M] \public f\ by fastforce qed simp } thus ?thesis using assms by metis qed subsubsection {* Specialized induction rules that do not quantify over the intruder knowledge *} lemma intruder_deduct_induct[consumes 1, case_names Axiom Compose Decompose]: assumes "M \ t" "\t. t \ M \ P M t" "\X f. \length X = arity f; public f; \x. x \ set X \ M \ x; \x. x \ set X \ P M x\ \ P M (Fun f X)" "\t K T t\<^sub>i. \M \ t; P M t; Ana t = (K, T); \k. k \ K \ M \ k; \k. k \ K \ P M k; t\<^sub>i \ T\ \ P M t\<^sub>i" shows "P M t" using assms by (induct rule: intruder_deduct.induct) blast+ lemma intruder_synth_induct[consumes 1, case_names AxiomC ComposeC]: assumes "M \\<^sub>c t" "\t. t \ M \ P M t" "\X f. \length X = arity f; public f; \x. x \ set X \ M \\<^sub>c x; \x. x \ set X \ P M x\ \ P M (Fun f X)" shows "P M t" using assms by (induct rule: intruder_synth.induct) auto subsubsection {* Monotonicity lemmas *} lemma ideduct_mono: "\M \ t; M \ M'\ \ M' \ t" proof (induction rule: intruder_deduct.induct) case (Decompose M t K T t\<^sub>i) have "\k. k \ K \ M' \ k" using Decompose.IH \M \ M'\ by simp moreover have "M' \ t" using Decompose.IH \M \ M'\ by simp ultimately show ?case using Decompose.hyps intruder_deduct.Decompose by blast qed auto lemma ideduct_synth_mono: "\M \\<^sub>c t; M \ M'\ \ M' \\<^sub>c t" by (induct rule: intruder_synth.induct) auto lemma (in intruder_model) ideduct_reduce: "\M \ M' \ t; \t'. t' \ M' \ M \ t'\ \ M \ t" proof (induction rule: intruder_deduct_induct) case Decompose thus ?case using intruder_deduct.Decompose by blast qed auto lemma ideduct_synth_reduce: "\M \ M' \\<^sub>c t; \t'. t' \ M' \ M \\<^sub>c t'\ \ M \\<^sub>c t" by (induct rule: intruder_synth_induct) auto lemma ideduct_ik_eq: assumes "\t \ M. M' \ t" shows "M' \ t \ M' \ M \ t" by (meson assms ideduct_mono ideduct_reduce sup_ge1) lemma ideduct_mono_eq: assumes "\t. M \ t \ M' \ t" shows "M \ N \ t \ M' \ N \ t" proof show "M \ N \ t \ M' \ N \ t" proof (induction t rule: intruder_deduct_induct) case (Axiom t) thus ?case proof (cases "t \ M") case True hence "M \ t" using intruder_deduct.Axiom by metis thus ?thesis using assms ideduct_mono[of M' t "M' \ N"] by simp qed auto next case (Compose X f) thus ?case using intruder_deduct.Compose by auto next case (Decompose t K T t\<^sub>i) thus ?case using intruder_deduct.Decompose[of "M' \ N" t K T] by auto qed show "M' \ N \ t \ M \ N \ t" proof (induction t rule: intruder_deduct_induct) case (Axiom t) thus ?case proof (cases "t \ M'") case True hence "M' \ t" using intruder_deduct.Axiom by metis thus ?thesis using assms ideduct_mono[of M t "M \ N"] by simp qed auto next case (Compose X f) thus ?case using intruder_deduct.Compose by auto next case (Decompose t K T t\<^sub>i) thus ?case using intruder_deduct.Decompose[of "M \ N" t K T] by auto qed qed lemma deduct_synth_subterm: assumes "M \\<^sub>c t" "s \ subterms t" "\m \ M. \s \ subterms m. M \\<^sub>c s" shows "M \\<^sub>c s" using assms by (induct t rule: intruder_synth.induct) auto lemma deduct_if_synth[intro, dest]: "M \\<^sub>c t \ M \ t" by (induct rule: intruder_synth.induct) auto lemma synth_if_deduct_empty: "{} \ t \ {} \\<^sub>c t" proof (induction t rule: intruder_deduct_induct) case (Decompose t K M m) then obtain f T where "t = Fun f T" "m \ set T" using Ana_fun_subterm Ana_var by (cases t) fastforce+ with Decompose.IH(1) show ?case by (induction rule: intruder_synth_induct) auto qed auto lemma ideduct_deduct_synth_mono_eq: assumes "\t. M \ t \ M' \\<^sub>c t" "M \ M'" and "\t. M' \ N \ t \ M' \ N \ D \\<^sub>c t" shows "M \ N \ t \ M' \ N \ D \\<^sub>c t" proof - have "\m \ M'. M \ m" using assms(1) by auto hence "\t. M \ t \ M' \ t" by (metis assms(1,2) deduct_if_synth ideduct_reduce sup.absorb2) hence "\t. M' \ N \ t \ M \ N \ t" by (meson ideduct_mono_eq) thus ?thesis by (meson assms(3)) qed lemma deduct_if_trp_synth: "trp\<^sub>s\<^sub>e\<^sub>t M \\<^sub>c t \ M \ t" using deduct_if_synth trp_deduct_decompose' by metis lemma ideduct_subst: "M \ t \ M \set \ \ t \ \" proof (induction t rule: intruder_deduct_induct) case (Compose T f) hence "length (map (\t. t \ \) T) = arity f" "\t. t \ set T \ M \set \ \ t \ \" by auto thus ?case using intruder_deduct.Compose[OF _ Compose.hyps(2), of "map (\t. t \ \) T"] by auto next case (Decompose t K M' m') hence "Ana (t \ \) = (K \set \, M' \set \)" "\k. k \ K \set \ \ M \set \ \ k" "m' \ \ \ M' \set \" using Ana_subst[OF Decompose.hyps(2)] by auto thus ?case using intruder_deduct.Decompose[OF Decompose.IH(1)] by metis qed simp lemma ideduct_synth_subst: "M \\<^sub>c t \ M \set \ \\<^sub>c t \ \" proof (induction t rule: intruder_synth_induct) case (ComposeC T f) hence "length (map (\t. t \ \) T) = arity f" "\t. t \ set T \ M \set \ \\<^sub>c t \ \" by auto thus ?case using intruder_synth.ComposeC[OF _ ComposeC.hyps(2), of "map (\t. t \ \) T"] by auto qed simp lemma ideduct_vars: assumes "M \ t" shows "FV t \ FV\<^sub>s\<^sub>e\<^sub>t M" using assms proof (induction t rule: intruder_deduct_induct) case (Decompose t K T t\<^sub>i) thus ?case using Ana_vars(2) FV_subset by blast qed auto lemma ideduct_synth_vars: assumes "M \\<^sub>c t" shows "FV t \ FV\<^sub>s\<^sub>e\<^sub>t M" using assms by (induct t rule: intruder_synth_induct) auto subsubsection {* Intruder knowledge closure theorem *} lemma deducts_eq_if_analyzed: "analyzed M \ M \ t \ M \\<^sub>c t" by auto lemma closure_is_superset: "decomp_closure M M' \ M \ M'" by force lemma deduct_if_closure_deduct: "\M' \ t; decomp_closure M M'\ \ M \ t" proof (induction t rule: intruder_deduct.induct) case (Decompose M' t K T t\<^sub>i) thus ?case using intruder_deduct.Decompose[OF _ \Ana t = (K,T)\ _ \t\<^sub>i \ T\] by simp qed auto lemma deduct_if_closure_synth: "\decomp_closure M M'; M' \\<^sub>c t\ \ M \ t" using deduct_if_closure_deduct by blast lemma closure_subterms_composable: assumes "decomp_closure M M'" and "M' \\<^sub>c t'" "M' \ t" "t \ t'" shows "M' \\<^sub>c t" using \M' \\<^sub>c t'\ assms proof (induction t' rule: intruder_synth.induct) case (AxiomC t' M') have "M \ t" using \M' \ t\ deduct_if_closure_deduct AxiomC.prems(1) by blast moreover { have "\s \ M. t' \ s" using \t' \ M'\ AxiomC.prems(1) unfolding decomp_closure_def by blast hence "\s \ M. t \ s" using \t \ t'\ subtermeq_trans by auto } ultimately have "t \ M'" using AxiomC.prems(1) unfolding decomp_closure_def by blast thus ?case by simp next case (ComposeC X f M') let ?t' = "Fun f X" { assume "t = ?t'" have "M' \\<^sub>c t" using \M' \\<^sub>c ?t'\ \t = ?t'\ by simp } moreover { assume "t \ ?t'" have "\x \ set X. t \ x" using \t \ ?t'\ \t \ ?t'\ by simp hence "M' \\<^sub>c t" using ComposeC.IH ComposeC.prems(1,3) ComposeC.hyps(3) by blast } ultimately show ?case using cases_simp[of "t = ?t'" "M' \\<^sub>c t"] by simp qed lemma closure_analyzed: assumes "decomp_closure M M'" shows "analyzed M'" proof - { fix t assume "M' \ t" have "M' \\<^sub>c t" using \M' \ t\ assms proof (induction t rule: intruder_deduct.induct) case (Decompose M' t K T t\<^sub>i) hence "M' \ t\<^sub>i" using Decompose.hyps intruder_deduct.Decompose by blast moreover have "t\<^sub>i \ t" using Decompose.hyps(4) Ana_subterm[OF Decompose.hyps(2)] unfolding subtermeq_def by blast moreover have "M' \\<^sub>c t" using Decompose.IH(1) Decompose.prems by blast ultimately show "M' \\<^sub>c t\<^sub>i" using closure_subterms_composable Decompose.prems by blast qed auto } moreover have "\t. M \\<^sub>c t \ M \ t" by auto ultimately show ?thesis by auto qed lemma ik_has_synth_ik_closure: fixes M :: "('fun,'var) terms" shows "\M'. (\t. M \ t \ M' \\<^sub>c t) \ decomp_closure M M' \ (finite M \ finite M')" proof - let ?M' = "{t. M \ t \ (\t' \ M. t \ t')}" have M'_closes: "decomp_closure M ?M'" by simp hence "M \ ?M'" using closure_is_superset by simp have "\t. ?M' \\<^sub>c t \ M \ t" using deduct_if_closure_synth[OF M'_closes] by blast moreover have "\t. M \ t \ ?M' \ t" using ideduct_mono[OF _ \M \ ?M'\] by simp moreover have "analyzed ?M'" using closure_analyzed[OF M'_closes] . ultimately have "\t. M \ t \ ?M' \\<^sub>c t" unfolding analyzed_def by blast moreover have "finite M \ finite ?M'" by auto ultimately show ?thesis using M'_closes by blast qed subsubsection {* Transparently analysable subterms can be inferred without decomposition *} lemma trp_subterm_synth_deduct: assumes "trp\<^sub>s\<^sub>e\<^sub>t M \\<^sub>c t" "s \\<^sub>t\<^sub>r\<^sub>p t" shows "trp\<^sub>s\<^sub>e\<^sub>t M \\<^sub>c s" using assms proof (induction t rule: intruder_synth_induct) case (AxiomC t) hence "s \ trp\<^sub>s\<^sub>e\<^sub>t M" using trp_member_trp_subset_union[of t M] by auto thus ?case by simp next case (ComposeC X f) thus ?case proof (cases "s = Fun f X") case False hence "transparent f" using \s \\<^sub>t\<^sub>r\<^sub>p (Fun f X)\ using trp_fun_member(1) by blast then obtain x where "x \ set X" "s \\<^sub>t\<^sub>r\<^sub>p x" using \s \\<^sub>t\<^sub>r\<^sub>p (Fun f X)\ \s \ Fun f X\ by auto thus ?thesis using ComposeC.IH by metis qed simp qed subsubsection {* Lemmas concerning transparent function decomposition with substitutions *} lemma var_in_trp_if_in_subst_diff: assumes "t \\<^sub>t\<^sub>r\<^sub>p t' \ \" "t \ trp t' \set \" shows "\v. Var v \\<^sub>t\<^sub>r\<^sub>p t' \ t \\<^sub>t\<^sub>r\<^sub>p \ v" using assms proof (induction t') case (Fun f X) hence "t \ Fun f X \ \" using subst_all_member trp_refl by blast have "transparent f" proof (rule ccontr) assume "\transparent f" hence "trp (Fun f X \ \) = {Fun f X \ \}" by simp thus False using \t \\<^sub>t\<^sub>r\<^sub>p Fun f X \ \\ \t \ Fun f X \ \\ by auto qed have trp_unfold: "trp (Fun f X) = insert (Fun f X) (UNION (set X) trp)" using \transparent f\ by simp hence *: "\x \ set X. t \ trp x \set \" using \t \ trp (Fun f X) \set \\ subst_all_mono[of _ "trp (Fun f X)" \] by auto have **: "\x \ set X. t \\<^sub>t\<^sub>r\<^sub>p x \ \" using \t \\<^sub>t\<^sub>r\<^sub>p Fun f X \ \\ \t \ Fun f X \ \\ by (auto simp add: \transparent f\) from * ** obtain x where x: "x \ set X" "t \\<^sub>t\<^sub>r\<^sub>p x \ \" "t \ trp x \set \" by auto hence "\v. Var v \\<^sub>t\<^sub>r\<^sub>p x \ t \\<^sub>t\<^sub>r\<^sub>p (\ v)" using Fun.IH by metis thus ?case using \x \ set X\ trp_unfold by auto qed simp lemma var_in_trp_if_in_subst_diff_set: assumes "t \ trp\<^sub>s\<^sub>e\<^sub>t (M \set \)" "t \ (trp\<^sub>s\<^sub>e\<^sub>t M) \set \" shows "\v. Var v \ trp\<^sub>s\<^sub>e\<^sub>t M \ t \\<^sub>t\<^sub>r\<^sub>p \ v \ t \ \ v" proof - from assms(1) obtain t' where t': "t' \ M" "t \\<^sub>t\<^sub>r\<^sub>p t' \ \" by auto hence "t' \ trp\<^sub>s\<^sub>e\<^sub>t M" by fastforce hence "trp t' \ trp\<^sub>s\<^sub>e\<^sub>t M" using \t' \ M\ by blast hence "trp t' \set \ \ trp\<^sub>s\<^sub>e\<^sub>t M \set \" by (simp add: subst_all_mono) hence "t \ trp t' \set \" using assms(2) by auto then obtain v where "Var v \\<^sub>t\<^sub>r\<^sub>p t'" "t \\<^sub>t\<^sub>r\<^sub>p \ v" using var_in_trp_if_in_subst_diff[OF t'(2)] by metis hence "Var v \ trp\<^sub>s\<^sub>e\<^sub>t M" using \t' \ trp\<^sub>s\<^sub>e\<^sub>t M\ \t' \ M\ by blast thus ?thesis using subst_all_member[OF \Var v \ trp\<^sub>s\<^sub>e\<^sub>t M\, of \] \t \\<^sub>t\<^sub>r\<^sub>p \ v\ \t \ trp\<^sub>s\<^sub>e\<^sub>t M \set \\ by auto qed lemma trp_subst_union_unfold: "trp\<^sub>s\<^sub>e\<^sub>t (M \set \) = (trp\<^sub>s\<^sub>e\<^sub>t M \set \) \ \{trp (\ v) | v. Var v \ trp\<^sub>s\<^sub>e\<^sub>t M}" proof let ?A = "trp\<^sub>s\<^sub>e\<^sub>t (M \set \)" let ?B = "trp\<^sub>s\<^sub>e\<^sub>t M \set \" let ?C = "\{trp (\ v) | v. Var v \ trp\<^sub>s\<^sub>e\<^sub>t M}" show "?B \ ?C \ ?A" proof - have "?B \ ?A" using trp_subst_apply_subset_set by metis moreover have "?C \ ?A" proof fix t assume "t \ ?C" then obtain v where "t \\<^sub>t\<^sub>r\<^sub>p (\ v)" "Var v \ trp\<^sub>s\<^sub>e\<^sub>t M" by auto thus "t \ trp\<^sub>s\<^sub>e\<^sub>t (M \set \)" using trp_member_trp_subset_union_subst[of "Var v" M \] by auto qed ultimately show ?thesis by simp qed show "?A \ ?B \ ?C" proof fix t assume "t \ ?A" thus "t \ ?B \ ?C" proof (cases "t \ ?B") case False then obtain v where "Var v \ trp\<^sub>s\<^sub>e\<^sub>t M" "t \\<^sub>t\<^sub>r\<^sub>p (\ v)" using var_in_trp_if_in_subst_diff_set \t \ ?A\ by metis hence "t \ ?C" by blast thus "t \ ?B \ ?C" by auto qed auto qed qed end end