using intruder_deduct_restricted.AxiomR[of t M] assms
unfolding intruder_deduct_hom_def
by blast
lemma intruder_deduct_hom_ComposeH[simp]:
assumes "length X = arity f" "public f" "\<And>x. x \<in> set X \<Longrightarrow> \<langle>M; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m x"
and "homogeneous\<^sub>l\<^sub>s\<^sub>t (Fun f X) \<A> Sec" "Fun f X \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
shows "\<langle>M; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m Fun f X"
proof -
let ?Q = "\<lambda>t. homogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Sec \<and> t \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
show ?thesis
using intruder_deduct_restricted.ComposeR[of X f M ?Q] assms
unfolding intruder_deduct_hom_def
by blast
qed
lemma intruder_deduct_hom_DecomposeH:
assumes "\<langle>M; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m t" "Ana t = (K, T)" "\<And>k. k \<in> set K \<Longrightarrow> \<langle>M; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m k" "t\<^sub>i \<in> set T"
using SMP_union[of "trms\<^sub>l\<^sub>s\<^sub>t A" "trms\<^sub>l\<^sub>s\<^sub>t B"] trms\<^sub>l\<^sub>s\<^sub>t_append[of A B] unfolding GSMP_def by auto
lemma GSMP_union: "GSMP (A \<union> B) = GSMP A \<union> GSMP B"
using SMP_union[of A B] unfolding GSMP_def by auto
lemma GSMP_Union: "GSMP (trms\<^sub>l\<^sub>s\<^sub>t A) = (\<Union>l. GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l A))"
proof -
define P where "P \<equiv> (\<lambda>l. trms_proj\<^sub>l\<^sub>s\<^sub>t l A)"
define Q where "Q \<equiv> trms\<^sub>l\<^sub>s\<^sub>t A"
have "SMP (\<Union>l. P l) = (\<Union>l. SMP (P l))" "Q = (\<Union>l. P l)"
unfolding P_def Q_def by (metis SMP_Union, metis trms\<^sub>l\<^sub>s\<^sub>t_union)
hence "GSMP Q = (\<Union>l. GSMP (P l))" unfolding GSMP_def by auto
thus ?thesis unfolding P_def Q_def by metis
qed
lemma in_GSMP_in_proj: "t \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t A) \<Longrightarrow> \<exists>n. t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t n A)"
using GSMP_Union[of A] by blast
lemma in_proj_in_GSMP: "t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t n A) \<Longrightarrow> t \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t A)"
using GSMP_Union[of A] by blast
lemma GSMP_disjointE:
assumes A: "GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t n A) (trms_proj\<^sub>l\<^sub>s\<^sub>t m A) Sec"
shows "GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t n A) \<inter> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t m A) \<subseteq> Sec \<union> {m. {} \<turnstile>\<^sub>c m}"
using assms unfolding GSMP_disjoint_def by auto
lemma GSMP_disjoint_term:
assumes "GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>) (trms_proj\<^sub>l\<^sub>s\<^sub>t l' \<A>) Sec"
shows "t \<notin> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>) \<or> t \<notin> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l' \<A>) \<or> t \<in> Sec \<or> {} \<turnstile>\<^sub>c t"
shows "ik\<^sub>s\<^sub>t (proj_unl n A) \<cdot>\<^sub>s\<^sub>e\<^sub>t I \<subseteq> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t n A)"
proof
fix t assume "t \<in> ik\<^sub>s\<^sub>t (proj_unl n A) \<cdot>\<^sub>s\<^sub>e\<^sub>t I"
hence *: "t \<in> trms_proj\<^sub>l\<^sub>s\<^sub>t n A \<cdot>\<^sub>s\<^sub>e\<^sub>t I" by auto
then obtain s where "s \<in> trms_proj\<^sub>l\<^sub>s\<^sub>t n A" "t = s \<cdot> I" by auto
hence "t \<in> SMP (trms_proj\<^sub>l\<^sub>s\<^sub>t n A)" using SMP_I I(1,2) wf_trm_subst_range_iff[of I] by simp
moreover have "fv t = {}"
using * interpretation_grounds_all'[OF I(3)]
by auto
ultimately show "t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t n A)" unfolding GSMP_def by simp
qed
lemma declassified_proj_ik_subset: "declassified\<^sub>l\<^sub>s\<^sub>t A I \<subseteq> ik\<^sub>s\<^sub>t (proj_unl n A) \<cdot>\<^sub>s\<^sub>e\<^sub>t I"
proof (induction A)
case (Cons a A) thus ?case
using proj_ik_append[of n "[a]" A] by (auto simp add: declassified\<^sub>l\<^sub>s\<^sub>t_def)
qed (simp add: declassified\<^sub>l\<^sub>s\<^sub>t_def)
shows "subterms\<^sub>s\<^sub>e\<^sub>t (declassified\<^sub>l\<^sub>s\<^sub>t A I) \<subseteq> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t n A)"
proof
fix t assume t: "t \<in> subterms\<^sub>s\<^sub>e\<^sub>t (declassified\<^sub>l\<^sub>s\<^sub>t A I)"
then obtain t' where t': "t' \<in> declassified\<^sub>l\<^sub>s\<^sub>t A I" "t \<sqsubseteq> t'" by moura
hence "t' \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t n A)" using declassified_proj_GSMP_subset[OF assms] by blast
thus "t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t n A)"
using SMP.Subterm[of t' "trms_proj\<^sub>l\<^sub>s\<^sub>t n A" t] ground_subterm[OF _ t'(2)] t'(2)
unfolding GSMP_def by fast
qed
lemma declassified_secrets_subset:
assumes A: "\<forall>n m. n \<noteq> m \<longrightarrow> GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t n A) (trms_proj\<^sub>l\<^sub>s\<^sub>t m A) Sec"
and I: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t I" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range I)" "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t I"
shows "declassified\<^sub>l\<^sub>s\<^sub>t A I \<subseteq> Sec \<union> {m. {} \<turnstile>\<^sub>c m}"
using declassified_proj_GSMP_subset[OF I] A at_least_2_labels
unfolding GSMP_disjoint_def by blast
lemma declassified_subterms_secrets_subset:
assumes A: "\<forall>n m. n \<noteq> m \<longrightarrow> GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t n A) (trms_proj\<^sub>l\<^sub>s\<^sub>t m A) Sec"
and I: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t I" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range I)" "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t I"
using declassified_subterms_proj_GSMP_subset[OF I, of A label_witness1]
declassified_subterms_proj_GSMP_subset[OF I, of A label_witness2]
A at_least_2_labels
unfolding GSMP_disjoint_def by fast
lemma declassified_proj_eq: "declassified\<^sub>l\<^sub>s\<^sub>t A I = declassified\<^sub>l\<^sub>s\<^sub>t (proj n A) I"
unfolding declassified\<^sub>l\<^sub>s\<^sub>t_def proj_def by auto
lemma declassified_append: "declassified\<^sub>l\<^sub>s\<^sub>t (A@B) I = declassified\<^sub>l\<^sub>s\<^sub>t A I \<union> declassified\<^sub>l\<^sub>s\<^sub>t B I"
unfolding declassified\<^sub>l\<^sub>s\<^sub>t_def by auto
lemma declassified_prefix_subset: "prefix A B \<Longrightarrow> declassified\<^sub>l\<^sub>s\<^sub>t A I \<subseteq> declassified\<^sub>l\<^sub>s\<^sub>t B I"
using declassified_append unfolding prefix_def by auto
subsection \<open>Lemmata: Homogeneous and Heterogeneous Terms\<close>
lemma proj_specific_secrets_anti_mono:
assumes "proj_specific l t \<A> Sec" "Sec' \<subseteq> Sec"
shows "proj_specific l t \<A> Sec'"
using assms unfolding proj_specific_def by fast
lemma heterogeneous_secrets_anti_mono:
assumes "heterogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Sec" "Sec' \<subseteq> Sec"
shows "heterogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Sec'"
using assms proj_specific_secrets_anti_mono unfolding heterogeneous\<^sub>l\<^sub>s\<^sub>t_def by metis
lemma homogeneous_secrets_mono:
assumes "homogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Sec'" "Sec' \<subseteq> Sec"
shows "homogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Sec"
using assms heterogeneous_secrets_anti_mono by blast
lemma heterogeneous_supterm:
assumes "heterogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Sec" "t \<sqsubseteq> t'"
assumes "t \<sqsubseteq> t'" "proj_specific l t' \<A> Sec"
shows "proj_specific l t \<A> Sec \<or> t \<in> Sec \<or> {} \<turnstile>\<^sub>c t"
using GSMP_subterm[OF _ assms(1)] assms(2) by (auto simp add: proj_specific_def)
lemma heterogeneous_term_is_Fun:
assumes "heterogeneous\<^sub>l\<^sub>s\<^sub>t t A S" shows "\<exists>f T. t = Fun f T"
using assms by (cases t) (auto simp add: GSMP_def heterogeneous\<^sub>l\<^sub>s\<^sub>t_def proj_specific_def)
lemma proj_specific_is_homogeneous:
assumes \<A>: "\<forall>l l'. l \<noteq> l' \<longrightarrow> GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>) (trms_proj\<^sub>l\<^sub>s\<^sub>t l' \<A>) Sec"
and t: "proj_specific l m \<A> Sec"
shows "homogeneous\<^sub>l\<^sub>s\<^sub>t m \<A> Sec"
proof
assume "heterogeneous\<^sub>l\<^sub>s\<^sub>t m \<A> Sec"
then obtain s l' where s: "s \<in> subterms m" "proj_specific l' s \<A> Sec" "l \<noteq> l'"
unfolding heterogeneous\<^sub>l\<^sub>s\<^sub>t_def by moura
hence "s \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)" "s \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l' \<A>)"
using t by (auto simp add: GSMP_def proj_specific_def)
using \<A> s(3) by (auto simp add: GSMP_disjoint_def)
thus False using s(2) by (auto simp add: proj_specific_def)
qed
lemma deduct_synth_homogeneous:
assumes "{} \<turnstile>\<^sub>c t"
shows "homogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Sec"
proof -
have "\<forall>s \<in> subterms t. {} \<turnstile>\<^sub>c s" using deduct_synth_subterm[OF assms] by auto
thus ?thesis unfolding heterogeneous\<^sub>l\<^sub>s\<^sub>t_def proj_specific_def by auto
qed
lemma GSMP_proj_is_homogeneous:
assumes "\<forall>l l'. l \<noteq> l' \<longrightarrow> GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t l A) (trms_proj\<^sub>l\<^sub>s\<^sub>t l' A) Sec"
and "t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l A)" "t \<notin> Sec"
shows "homogeneous\<^sub>l\<^sub>s\<^sub>t t A Sec"
proof
assume "heterogeneous\<^sub>l\<^sub>s\<^sub>t t A Sec"
then obtain s l' where s: "s \<in> subterms t" "proj_specific l' s A Sec" "l \<noteq> l'"
unfolding heterogeneous\<^sub>l\<^sub>s\<^sub>t_def by moura
hence "s \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l A)" "s \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l' A)"
using assms by (auto simp add: GSMP_def proj_specific_def)
hence "s \<in> Sec \<or> {} \<turnstile>\<^sub>c s" using assms(1) s(3) by (auto simp add: GSMP_disjoint_def)
thus False using s(2) by (auto simp add: proj_specific_def)
qed
lemma homogeneous_is_not_proj_specific:
assumes "homogeneous\<^sub>l\<^sub>s\<^sub>t m \<A> Sec"
shows "\<exists>l::'lbl. \<not>proj_specific l m \<A> Sec"
proof -
let ?P = "\<lambda>l s. proj_specific l s \<A> Sec"
have "\<forall>l1 l2. \<forall>s1\<in>subterms m. \<forall>s2\<in>subterms m. (l1 \<noteq> l2 \<longrightarrow> (\<not>?P l1 s1 \<or> \<not>?P l2 s2))"
using assms heterogeneous\<^sub>l\<^sub>s\<^sub>t_def by metis
then obtain l1 l2 where "l1 \<noteq> l2" "\<not>?P l1 m \<or> \<not>?P l2 m"
by (metis term.order_refl at_least_2_labels)
thus ?thesis by metis
qed
lemma secrets_are_homogeneous:
assumes "\<forall>s \<in> Sec. P s \<longrightarrow> (\<forall>s' \<in> subterms s. {} \<turnstile>\<^sub>c s' \<or> s' \<in> Sec)" "s \<in> Sec" "P s"
shows "homogeneous\<^sub>l\<^sub>s\<^sub>t s \<A> Sec"
using assms by (auto simp add: heterogeneous\<^sub>l\<^sub>s\<^sub>t_def proj_specific_def)
lemma GSMP_is_homogeneous:
assumes \<A>: "\<forall>l l'. l \<noteq> l' \<longrightarrow> GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>) (trms_proj\<^sub>l\<^sub>s\<^sub>t l' \<A>) Sec"
and t: "t \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)" "t \<notin> Sec"
shows "homogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Sec"
proof -
obtain n where n: "t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t n \<A>)" using in_GSMP_in_proj[OF t(1)] by moura
show ?thesis using GSMP_proj_is_homogeneous[OF \<A> n t(2)] by metis
qed
lemma GSMP_intersection_is_homogeneous:
assumes \<A>: "\<forall>l l'. l \<noteq> l' \<longrightarrow> GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>) (trms_proj\<^sub>l\<^sub>s\<^sub>t l' \<A>) Sec"
and t: "t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>) \<inter> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l' \<A>)" "l \<noteq> l'"
shows "homogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Sec"
proof -
define M where "M \<equiv> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)"
define M' where "M' \<equiv> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l' \<A>)"
have t_in: "t \<in> M \<inter> M'" "t \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
using * secrets_are_homogeneous[of Sec "\<lambda>t. t \<in> M \<inter> M'", OF _ _ t_in(1)]
by fast
qed (metis GSMP_is_homogeneous[OF \<A> t_in(2)])
qed
lemma GSMP_is_homogeneous':
assumes \<A>: "\<forall>l l'. l \<noteq> l' \<longrightarrow> GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>) (trms_proj\<^sub>l\<^sub>s\<^sub>t l' \<A>) Sec"
and t: "t \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
shows "homogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Sec"
using GSMP_is_homogeneous[OF \<A> t(1)] GSMP_intersection_is_homogeneous[OF \<A>] t(2)
by blast
lemma declassified_secrets_are_homogeneous:
assumes \<A>: "\<forall>l l'. l \<noteq> l' \<longrightarrow> GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>) (trms_proj\<^sub>l\<^sub>s\<^sub>t l' \<A>) Sec"
and \<I>: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<I>)" "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>"
and s: "s \<in> declassified\<^sub>l\<^sub>s\<^sub>t \<A> \<I>"
shows "homogeneous\<^sub>l\<^sub>s\<^sub>t s \<A> Sec"
proof -
have s_in: "s \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
using declassified_proj_GSMP_subset[OF \<I>, of \<A> label_witness1]
in_proj_in_GSMP[of s label_witness1 \<A>] s
by blast
show ?thesis
proof (cases "s \<in> Sec")
case True thus ?thesis
using declassified_subterms_secrets_subset[OF \<A> \<I>]
secrets_are_homogeneous[of Sec "\<lambda>s. s \<in> declassified\<^sub>l\<^sub>s\<^sub>t \<A> \<I>", OF _ _ s]
by fast
qed (metis GSMP_is_homogeneous[OF \<A> s_in])
qed
lemma Ana_keys_homogeneous:
assumes \<A>: "\<forall>l l'. l \<noteq> l' \<longrightarrow> GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>) (trms_proj\<^sub>l\<^sub>s\<^sub>t l' \<A>) Sec"
and t: "t \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
lemma deduct_if_hom_deduct: "\<langle>M;A;S\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m m \<Longrightarrow> M \<turnstile> m"
using deduct_if_restricted_deduct unfolding intruder_deduct_hom_def by blast
lemma hom_deduct_if_hom_ik:
assumes "\<langle>M;A;Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m m" "\<forall>m \<in> M. homogeneous\<^sub>l\<^sub>s\<^sub>t m A Sec \<and> m \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t A)"
shows "homogeneous\<^sub>l\<^sub>s\<^sub>t m A Sec \<and> m \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t A)"
proof -
let ?Q = "\<lambda>m. homogeneous\<^sub>l\<^sub>s\<^sub>t m A Sec \<and> m \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t A)"
have "?Q t'" when "?Q t" "t' \<sqsubseteq> t" for t t'
using homogeneous_subterm[OF _ that(2)] GSMP_subterm[OF _ that(2)] that(1)
by blast
thus ?thesis
using assms(1) restricted_deduct_if_restricted_ik[OF _ assms(2)]
and t: "\<langle>\<Union>l. M l; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m t"
shows "t \<notin> Sec - Discl" (is ?A)
"\<forall>l. t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>) \<longrightarrow> \<langle>M l; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m t" (is ?B)
proof -
have M': "\<forall>l. \<forall>m \<in> M l. m \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
proof (intro allI ballI)
fix l m show "m \<in> M l \<Longrightarrow> m \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)" using M(2) in_proj_in_GSMP[of m l \<A>] by blast
qed
show ?A ?B using t
proof (induction t rule: intruder_deduct_hom_induct)
case (AxiomH t)
then obtain lt where t_in_proj_ik: "t \<in> M lt" by moura
show t_not_Sec: "t \<notin> Sec - Discl"
proof
assume "t \<in> Sec - Discl"
hence "\<forall>l. \<not>(\<langle>M l;\<A>;Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m t)" using Sec by auto
thus False using intruder_deduct_hom_AxiomH[OF t_in_proj_ik] by metis
qed
have 1: "\<forall>l. t \<in> M l \<longrightarrow> t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)"
using M(2,3) AxiomH by auto
have 3: "\<And>l1 l2. l1 \<noteq> l2 \<Longrightarrow> t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l1 \<A>) \<inter> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l2 \<A>)
\<Longrightarrow> {} \<turnstile>\<^sub>c t \<or> t \<in> Discl"
using \<A> t_not_Sec by (auto simp add: par_comp_def GSMP_disjoint_def)
have 4: "homogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Sec" "t \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)" using M(1) M' t_in_proj_ik by auto
{ fix l assume "t \<in> Discl"
hence "t \<in> M l" using M(3) by auto
hence "\<langle>M l; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m t" by auto
} hence 5: "\<forall>l. t \<in> Discl \<longrightarrow> \<langle>M l; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m t" by metis
show "\<forall>l. t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>) \<longrightarrow> \<langle>M l; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m t"
by (metis (lifting) Int_iff empty_subsetI
1 3 4 5 t_in_proj_ik
intruder_deduct_hom_AxiomH[of t _ \<A> Sec]
deduct_hom_if_synth[of t \<A> Sec "{}"]
ideduct_hom_mono[of "{}" \<A> Sec t])
next
case (ComposeH T f)
show "\<forall>l. Fun f T \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>) \<longrightarrow> \<langle>M l; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m Fun f T"
proof (intro allI impI)
fix l
assume "Fun f T \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)"
hence "\<And>t. t \<in> set T \<Longrightarrow> t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)"
using GSMP_subterm[OF _ subtermeqI''] by auto
thus "\<langle>M l; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m Fun f T"
using ComposeH.IH(2) intruder_deduct_hom_ComposeH[OF ComposeH.hyps(1,2) _ ComposeH.hyps(4,5)]
by simp
qed
thus "Fun f T \<notin> Sec - Discl"
using Sec ComposeH.hyps(5) trms\<^sub>l\<^sub>s\<^sub>t_union[of \<A>] GSMP_Union[of \<A>]
by (metis (no_types, lifting) UN_iff)
next
case (DecomposeH t K T t\<^sub>i)
have ti_subt: "t\<^sub>i \<sqsubseteq> t" using Ana_subterm[OF DecomposeH.hyps(2)] \<open>t\<^sub>i \<in> set T\<close> by auto
have t: "homogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Sec" "t \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
using DecomposeH.hyps(1) hom_deduct_if_hom_ik M(1) M'
case True thus ?thesis using intruder_deduct.Axiom[OF t_in_ik_proj] by metis
next
case False thus ?thesis using T ideduct_mono[of "{}" t] by auto
qed
next
case False
hence "t \<notin> Sec - Discl" "\<not>{} \<turnstile>\<^sub>c t" "t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)" using Axiom by auto
hence "(\<forall>l'. l \<noteq> l' \<longrightarrow> t \<notin> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l' \<A>)) \<or> t \<in> Discl"
using \<A> unfolding GSMP_disjoint_def par_comp_def by auto
hence "(\<forall>l'. l \<noteq> l' \<longrightarrow> t \<notin> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l' \<A>)) \<or> t \<in> M l \<or> {} \<turnstile>\<^sub>c t" using M by auto
thus ?thesis using Axiom deduct_if_synth[THEN ideduct_mono] t_in_ik_proj
by (metis (no_types, lifting) False M(2) intruder_deduct.Axiom subsetCE)
qed
next
case (Compose T f)
hence "Fun f T \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)" using Compose.prems by auto
hence "\<And>t. t \<in> set T \<Longrightarrow> t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)" unfolding GSMP_def by auto
hence IH: "\<And>t. t \<in> set T \<Longrightarrow> M l \<turnstile> t \<or> (\<exists>s \<in> Sec - Discl. \<exists>l. M l \<turnstile> s)"
using Compose.IH by auto
show ?case
proof (cases "\<forall>t \<in> set T. M l \<turnstile> t")
case True thus ?thesis by (metis intruder_deduct.Compose[OF Compose.hyps(1,2)])
qed (metis IH)
next
case (Decompose t K T t\<^sub>i)
have hom_ik: "\<forall>l. \<forall>m\<in>M l. homogeneous\<^sub>l\<^sub>s\<^sub>t m \<A> Sec \<and> m \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
proof (intro allI ballI conjI)
fix l m assume m: "m \<in> M l"
thus "homogeneous\<^sub>l\<^sub>s\<^sub>t m \<A> Sec" using M(1) by simp
show "m \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)" using in_proj_in_GSMP[of m l \<A>] M(2) m by blast
obtain a A n where a: "\<A> = A@[a]" "a = (ln n, b) \<or> a = (\<star>, b)"
using unlabel_snoc_inv[OF snoc.hyps(2)[symmetric]] by moura
hence A: "\<A> = A@[(ln n, b)] \<or> \<A> = A@[(\<star>, b)]" by metis
have 1: "B = unlabel A" using a snoc.hyps(2) unlabel_append[of A "[a]"] by auto
have 2: "par_comp A Sec" using par_comp_prefix snoc.prems(1) a by metis
have 3: "\<lbrakk>{}; unlabel A\<rbrakk>\<^sub>d \<I>" by (metis 1 snoc.prems(2) snoc.hyps(2) strand_sem_split(3))
have IH: "(\<forall>l. \<lbrakk>{}; proj_unl l A\<rbrakk>\<^sub>d \<I>) \<or> (\<exists>\<A>'. prefix \<A>' A \<and> ?L \<A>')"
by (rule snoc.hyps(1)[OF 1 2 3])
show ?case
proof (cases "\<forall>l. \<lbrakk>{}; proj_unl l A\<rbrakk>\<^sub>d \<I>")
case False
then obtain \<A>' where \<A>': "prefix \<A>' A" "?L \<A>'" by (metis IH)
hence "prefix \<A>' (A@[a])" using a prefix_prefix[of _ A "[a]"] by simp
thus ?thesis using \<A>'(2) a by auto
next
case True
note IH' = True
show ?thesis
proof (cases b)
case (Send t)
hence "ik\<^sub>s\<^sub>t (unlabel A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> t \<cdot> \<I>"
using a \<open>\<lbrakk>{}; unlabel \<A>\<rbrakk>\<^sub>d \<I>\<close> strand_sem_split(2)[of "{}" "unlabel A" "unlabel [a]" \<I>]
unlabel_append[of A "[a]"]
by auto
hence *: "(\<Union>l. (ik\<^sub>s\<^sub>t (proj_unl l A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>)) \<turnstile> t \<cdot> \<I>"
using proj_ik_union_is_unlabel_ik image_UN by metis
have "ik\<^sub>s\<^sub>t (proj_unl l \<A>) = ik\<^sub>s\<^sub>t (proj_unl l A)" for l
using Send A
by (metis append_Nil2 ik\<^sub>s\<^sub>t.simps(3) proj_unl_cons(3) proj_nil(2)
singleton_lst_proj(1,2) proj_ik_append)
hence **: "ik\<^sub>s\<^sub>t (proj_unl l A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<subseteq> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)" for l
using ik_proj_subst_GSMP_subset[OF \<I>(3,4,2), of _ \<A>]
by auto
note Discl =
declassified_proj_ik_subset[of A \<I>]
declassified_proj_GSMP_subset[OF \<I>(3,4,2), of A]
declassified_secrets_subset[OF disj \<I>(3,4,2)]
declassified_append[of A "[a]" \<I>]
have Sec: "ground Sec"
using \<A> by (auto simp add: par_comp_def)
have "\<forall>m\<in>ik\<^sub>s\<^sub>t (proj_unl l \<A>) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>. homogeneous\<^sub>l\<^sub>s\<^sub>t m \<A> Sec \<or> m \<in> Sec-declassified\<^sub>l\<^sub>s\<^sub>t A \<I>"
"\<forall>m\<in>ik\<^sub>s\<^sub>t (proj_unl l \<A>) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>. m \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
"ik\<^sub>s\<^sub>t (proj_unl l \<A>) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<subseteq> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)"
for l
using declassified_secrets_are_homogeneous[OF disj \<I>(3,4,2)]
GSMP_proj_is_homogeneous[OF disj]
ik_proj_subst_GSMP_subset[OF \<I>(3,4,2), of _ \<A>]
using ik_proj_subst_GSMP_subset[OF \<I>(3,4,2), of _ \<A>]
GSMP_Union[of \<A>]
by auto
moreover have "ik\<^sub>s\<^sub>t (proj_unl l [a]) = {}" for l
using Send proj_ik\<^sub>s\<^sub>t_is_proj_rcv_set[of _ "[a]"] a(2) by auto
ultimately have M:
"\<forall>l. \<forall>m\<in>ik\<^sub>s\<^sub>t (proj_unl l A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>. homogeneous\<^sub>l\<^sub>s\<^sub>t m \<A> Sec \<or> m \<in> Sec-declassified\<^sub>l\<^sub>s\<^sub>t A \<I>"
"\<forall>l. ik\<^sub>s\<^sub>t (proj_unl l A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<subseteq> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)"
using a(1) proj_ik_append[of _ A "[a]"] by auto
have prefix_A: "prefix A \<A>" using A by auto
have "s \<cdot> \<I> = s"
when "s \<in> Sec" for s
using that Sec by auto
hence leakage_case: "\<lbrakk>{}; proj_unl l A@[Send s]\<rbrakk>\<^sub>d \<I>"
when "s \<in> Sec - declassified\<^sub>l\<^sub>s\<^sub>t A \<I>" "ik\<^sub>s\<^sub>t (proj_unl l A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> s" for l s
using that strand_sem_append(2) IH' by auto
have proj_deduct_case_n:
"\<forall>m. m \<noteq> n \<longrightarrow> \<lbrakk>{}; proj_unl m (A@[a])\<rbrakk>\<^sub>d \<I>"
"ik\<^sub>s\<^sub>t (proj_unl n A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> t \<cdot> \<I> \<Longrightarrow> \<lbrakk>{}; proj_unl n (A@[a])\<rbrakk>\<^sub>d \<I>"
when "a = (ln n, Send t)"
using that IH' proj_append(2)[of _ A]
by auto
have proj_deduct_case_star:
"\<lbrakk>{}; proj_unl l (A@[a])\<rbrakk>\<^sub>d \<I>"
when "a = (\<star>, Send t)" "ik\<^sub>s\<^sub>t (proj_unl l A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> t \<cdot> \<I>" for l
using that IH' proj_append(2)[of _ A]
by auto
show ?thesis
proof (cases "\<exists>l. \<exists>m \<in> ik\<^sub>s\<^sub>t (proj_unl l A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>. m \<in> Sec - declassified\<^sub>l\<^sub>s\<^sub>t A \<I>")
case True
then obtain l s where ls: "s \<in> Sec - declassified\<^sub>l\<^sub>s\<^sub>t A \<I>" "ik\<^sub>s\<^sub>t (proj_unl l A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> s"
using intruder_deduct.Axiom by metis
thus ?thesis using leakage_case prefix_A by blast
next
case False
hence M': "\<forall>l. \<forall>m\<in>ik\<^sub>s\<^sub>t (proj_unl l A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>. homogeneous\<^sub>l\<^sub>s\<^sub>t m \<A> Sec" using M(1) by blast
note deduct_proj_lemma =
par_comp_deduct_proj[OF snoc.prems(1) M' M(2) _ *, of "declassified\<^sub>l\<^sub>s\<^sub>t A \<I>" n]
from a(2) show ?thesis
proof
assume "a = (ln n, b)"
hence "a = (ln n, Send t)" "t \<cdot> \<I> \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t n \<A>)"
using Send a(1) trms_proj\<^sub>l\<^sub>s\<^sub>t_append[of n A "[a]"]
GSMP_wt_substI[OF _ \<I>(3,4,2)]
by (metis, force)
hence
"a = (ln n, Send t)"
"\<forall>m. m \<noteq> n \<longrightarrow> \<lbrakk>{}; proj_unl m (A@[a])\<rbrakk>\<^sub>d \<I>"
"ik\<^sub>s\<^sub>t (proj_unl n A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> t \<cdot> \<I> \<Longrightarrow> \<lbrakk>{}; proj_unl n (A@[a])\<rbrakk>\<^sub>d \<I>"
"t \<cdot> \<I> \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t n \<A>)"
using proj_deduct_case_n
by auto
hence "(\<forall>l. \<lbrakk>{}; proj_unl l \<A>\<rbrakk>\<^sub>d \<I>) \<or>
(\<exists>s \<in> Sec-declassified\<^sub>l\<^sub>s\<^sub>t A \<I>. \<exists>l. ik\<^sub>s\<^sub>t (proj_unl l A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> s)"
using deduct_proj_lemma A a Discl
by fast
thus ?thesis using leakage_case prefix_A by metis
next
assume "a = (\<star>, b)"
hence ***: "a = (\<star>, Send t)" "t \<cdot> \<I> \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)" for l
lemma wf\<^sub>l\<^sub>s\<^sub>t\<^sub>s_eqs_wf\<^sub>l\<^sub>s\<^sub>t\<^sub>s'[simp]: "wf\<^sub>l\<^sub>s\<^sub>t\<^sub>s S = wf\<^sub>l\<^sub>s\<^sub>t\<^sub>s' S []"
unfolding wf\<^sub>l\<^sub>s\<^sub>t\<^sub>s_def wf\<^sub>l\<^sub>s\<^sub>t\<^sub>s'_def unlabel_def by auto
and B'_wf: "list_all (wf\<^sub>t\<^sub>r\<^sub>m' arity) B'"
and A_inst: "has_all_wt_instances_of \<Gamma> (set A') (set A)"
and B_inst: "has_all_wt_instances_of \<Gamma> (set B') (set (B \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>))"
and A_SMP_repr: "finite_SMP_representation arity Ana \<Gamma> A"
and B_SMP_repr: "finite_SMP_representation arity Ana \<Gamma> (B \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>)"
and AB_trms_disj:
"\<forall>t \<in> set A. \<forall>s \<in> set (B \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>). \<Gamma> t = \<Gamma> s \<and> mgu t s \<noteq> None \<longrightarrow>
(intruder_synth' public arity {} t \<and> intruder_synth' public arity {} s) \<or>
((\<exists>u \<in> Sec. is_wt_instance_of_cond \<Gamma> t u) \<and> (\<exists>u \<in> Sec. is_wt_instance_of_cond \<Gamma> s u))"
and Sec_wf: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s Sec"