Theory Parallel_Compositionality

(*  Title:      Parallel_Compositionality.thy
    Author:     Andreas Viktor Hess, DTU
    Author:     Sebastian A. Mödersheim, DTU
    Author:     Achim D. Brucker, The University of Sheffield
    SPDX-License-Identifier: BSD-3-Clause
*)

section ‹Parallel Compositionality of Security Protocols›
theory Parallel_Compositionality
imports Typing_Result Labeled_Strands
begin

text‹\label{sec:Parallel-Compositionality}›

subsection ‹Definitions: Labeled Typed Model Locale›
locale labeled_typed_model = typed_model arity public Ana Γ
  for arity::"'fun ⇒ nat"
    and public::"'fun ⇒ bool"
    and Ana::"('fun,'var) term ⇒ (('fun,'var) term list × ('fun,'var) term list)"
    and Γ::"('fun,'var) term ⇒ ('fun,'atom::finite) term_type"
  +
  fixes label_witness1 and label_witness2::"'lbl"
  assumes at_least_2_labels: "label_witness1 ≠ label_witness2"
begin

text ‹The Ground Sub-Message Patterns (GSMP)›
definition GSMP::"('fun,'var) terms ⇒ ('fun,'var) terms" where
  "GSMP P ≡ {t ∈ SMP P. fv t = {}}"

definition typing_cond where
  "typing_cond 𝒜 ≡
    wfst {} 𝒜 ∧
    fvst 𝒜 ∩ bvarsst 𝒜 = {} ∧
    tfrst 𝒜 ∧
    wftrms (trmsst 𝒜) ∧
    Ana_invar_subst (ikst 𝒜 ∪ assignment_rhsst 𝒜)"


subsection ‹Definitions: GSMP Disjointness and Parallel Composability›
definition GSMP_disjoint where
  "GSMP_disjoint P1 P2 Secrets ≡ GSMP P1 ∩ GSMP P2 ⊆ Secrets ∪ {m. {} ⊢c m}"

definition declassifiedlst where
  "declassifiedlst (𝒜::('fun,'var,'lbl) labeled_strand) ℐ ≡
    {s. ⋃{set ts | ts. (⋆, Receive ts) ∈ set (𝒜 ⋅lst ℐ)} ⊢ s}"

definition par_comp where
  "par_comp (𝒜::('fun,'var,'lbl) labeled_strand) (Secrets::('fun,'var) terms) ≡ 
    (∀l1 l2. l1 ≠ l2 ⟶ GSMP_disjoint (trms_projlst l1 𝒜) (trms_projlst l2 𝒜) Secrets) ∧
    (∀s ∈ Secrets. ¬{} ⊢c s) ∧
    ground Secrets"

definition strand_leakslst where
  "strand_leakslst 𝒜 Sec ℐ ≡ (∃t ∈ Sec - declassifiedlst 𝒜 ℐ. ∃l. (ℐ ⊨ ⟨proj_unl l 𝒜@[Send1 t]⟩))"


subsection ‹Definitions: GSMP-Restricted Intruder Deduction Variant›
definition intruder_deduct_hom::
  "('fun,'var) terms ⇒ ('fun,'var,'lbl) labeled_strand ⇒ ('fun,'var) term ⇒ bool"
  (‹⟨_;_⟩ ⊢GSMP _› 50)
where
  "⟨M; 𝒜⟩ ⊢GSMP t ≡ ⟨M; λt. t ∈ GSMP (trmslst 𝒜)⟩ ⊢r t"

lemma intruder_deduct_hom_AxiomH[simp]:
  assumes "t ∈ M"
  shows "⟨M; 𝒜⟩ ⊢GSMP t"
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" "⋀x. x ∈ set X ⟹ ⟨M; 𝒜⟩ ⊢GSMP x"
  and "Fun f X ∈ GSMP (trmslst 𝒜)"
  shows "⟨M; 𝒜⟩ ⊢GSMP Fun f X"
using intruder_deduct_restricted.ComposeR[of X f M "λt. t ∈ GSMP (trmslst 𝒜)"] assms
unfolding intruder_deduct_hom_def
by blast

lemma intruder_deduct_hom_DecomposeH:
  assumes "⟨M; 𝒜⟩ ⊢GSMP t" "Ana t = (K, T)" "⋀k. k ∈ set K ⟹ ⟨M; 𝒜⟩ ⊢GSMP k" "ti ∈ set T"
  shows "⟨M; 𝒜⟩ ⊢GSMP ti"
using intruder_deduct_restricted.DecomposeR[of M "λt. t ∈ GSMP (trmslst 𝒜)" t] assms
unfolding intruder_deduct_hom_def
by blast

lemma intruder_deduct_hom_induct[consumes 1, case_names AxiomH ComposeH DecomposeH]:
  assumes "⟨M; 𝒜⟩ ⊢GSMP t" "⋀t. t ∈ M ⟹ P M t"
          "⋀X f. ⟦length X = arity f; public f;
                  ⋀x. x ∈ set X ⟹ ⟨M; 𝒜⟩ ⊢GSMP x;
                  ⋀x. x ∈ set X ⟹ P M x;
                  Fun f X ∈ GSMP (trmslst 𝒜)
                  ⟧ ⟹ P M (Fun f X)"
          "⋀t K T ti. ⟦⟨M; 𝒜⟩ ⊢GSMP t; P M t; Ana t = (K, T);
                       ⋀k. k ∈ set K ⟹ ⟨M; 𝒜⟩ ⊢GSMP k;
                       ⋀k. k ∈ set K ⟹ P M k; ti ∈ set T⟧ ⟹ P M ti"
  shows "P M t"
using intruder_deduct_restricted_induct[of M "λt. t ∈ GSMP (trmslst 𝒜)" t "λM Q t. P M t"] assms
unfolding intruder_deduct_hom_def
by blast

lemma ideduct_hom_mono:
  "⟦⟨M; 𝒜⟩ ⊢GSMP t; M ⊆ M'⟧ ⟹ ⟨M'; 𝒜⟩ ⊢GSMP t"
using ideduct_restricted_mono[of M _ t M']
unfolding intruder_deduct_hom_def
by fast


subsection ‹Lemmata: GSMP›
lemma GSMP_disjoint_empty[simp]:
  "GSMP_disjoint {} A Sec" "GSMP_disjoint A {} Sec"
unfolding GSMP_disjoint_def GSMP_def by fastforce+

lemma GSMP_mono:
  assumes "N ⊆ M"
  shows "GSMP N ⊆ GSMP M"
using SMP_mono[OF assms] unfolding GSMP_def by fast

lemma GSMP_SMP_mono:
  assumes "SMP N ⊆ SMP M"
  shows "GSMP N ⊆ GSMP M"
using assms unfolding GSMP_def by fast

lemma GSMP_subterm:
  assumes "t ∈ GSMP M" "t' ⊑ t"
  shows "t' ∈ GSMP M"
using SMP.Subterm[of t M t'] ground_subterm[of t t'] assms unfolding GSMP_def by auto

lemma GSMP_subterms: "subtermsset (GSMP M) = GSMP M"
using GSMP_subterm[of _ M] by blast

lemma GSMP_Ana_key:
  assumes "t ∈ GSMP M" "Ana t = (K,T)" "k ∈ set K"
  shows "k ∈ GSMP M"
using SMP.Ana[of t M K T k] Ana_keys_fv[of t K T] assms unfolding GSMP_def by auto

lemma GSMP_union: "GSMP (A ∪ B) = GSMP A ∪ GSMP B"
using SMP_union[of A B] unfolding GSMP_def by auto

lemma GSMP_Union: "GSMP (trmslst A) = (⋃l. GSMP (trms_projlst l A))"
proof -
  define P where "P ≡ (λl. trms_projlst l A)"
  define Q where "Q ≡ trmslst A"
  have "SMP (⋃l. P l) = (⋃l. SMP (P l))" "Q = (⋃l. P l)"
    unfolding P_def Q_def by (metis SMP_Union, metis trmslst_union)
  hence "GSMP Q = (⋃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 ∈ GSMP (trmslst A) ⟹ ∃n. t ∈ GSMP (trms_projlst n A)"
using GSMP_Union[of A] by blast

lemma in_proj_in_GSMP: "t ∈ GSMP (trms_projlst n A) ⟹ t ∈ GSMP (trmslst A)"
using GSMP_Union[of A] by blast

lemma GSMP_disjointE:
  assumes A: "GSMP_disjoint (trms_projlst n A) (trms_projlst m A) Sec"
  shows "GSMP (trms_projlst n A) ∩ GSMP (trms_projlst m A) ⊆ Sec ∪ {m. {} ⊢c m}"
using assms unfolding GSMP_disjoint_def by auto

lemma GSMP_disjoint_term:
  assumes "GSMP_disjoint (trms_projlst l 𝒜) (trms_projlst l' 𝒜) Sec"
  shows "t ∉ GSMP (trms_projlst l 𝒜) ∨ t ∉ GSMP (trms_projlst l' 𝒜) ∨ t ∈ Sec ∨ {} ⊢c t"
using assms unfolding GSMP_disjoint_def by blast

lemma GSMP_wt_subst_subset:
  assumes "t ∈ GSMP (M ⋅set ℐ)" "wtsubst ℐ" "wftrms (subst_range ℐ)"
  shows "t ∈ GSMP M"
using SMP_wt_subst_subset[OF _ assms(2,3), of t M] assms(1) unfolding GSMP_def by simp

lemma GSMP_wt_substI:
  assumes "t ∈ M" "wtsubst I" "wftrms (subst_range I)" "interpretationsubst I"
  shows "t ⋅ I ∈ GSMP M"
proof -
  have "t ∈ SMP M" using assms(1) by auto
  hence *: "t ⋅ I ∈ SMP M" using SMP.Substitution assms(2,3) wf_trm_subst_range_iff[of I] by simp
  moreover have "fv (t ⋅ I) = {}"
    using assms(1) interpretation_grounds_all'[OF assms(4)]
    by auto
  ultimately show ?thesis unfolding GSMP_def by simp
qed

lemma GSMP_disjoint_subset:
  assumes "GSMP_disjoint L R S" "L' ⊆ L" "R' ⊆ R"
  shows "GSMP_disjoint L' R' S"
using assms(1) SMP_mono[OF assms(2)] SMP_mono[OF assms(3)]
by (auto simp add: GSMP_def GSMP_disjoint_def)


subsection ‹Lemmata: Intruder Knowledge and Declassification›
lemma declassifiedlst_alt_def:
  "declassifiedlst 𝒜 ℐ = {s. (⋃{set ts | ts. (⋆, Receive ts) ∈ set 𝒜}) ⋅set ℐ ⊢ s}"
proof -
  have 0:
    "(l, receive⟨ts⟩st) ∈ set (𝒜 ⋅lst ℐ) = (∃ts'. (l, receive⟨ts'⟩st) ∈ set 𝒜 ∧ ts = ts' ⋅list ℐ)"
    (is "?A 𝒜 = ?B 𝒜")
    for ts l
  proof
    show "?A 𝒜 ⟹ ?B 𝒜"
    proof (induction 𝒜)
      case (Cons a 𝒜)
      obtain k b where a: "a = (k,b)" by (metis surj_pair)
      show ?case
      proof (cases "?A 𝒜")
        case False
        hence "(l,receive⟨ts⟩st) = a ⋅lstp ℐ" using Cons.prems by auto
        thus ?thesis unfolding a by (cases b) auto
      qed (use Cons.IH in auto)
    qed simp

    show "?B 𝒜 ⟹ ?A 𝒜" 
    proof (induction 𝒜)
      case (Cons a 𝒜)
      obtain k b where a: "a = (k,b)" by (metis surj_pair)
      show ?case
      proof (cases "?B 𝒜")
        case False
        hence "∃ts'. a = (l, receive⟨ts'⟩st) ∧ ts = ts' ⋅list ℐ" using Cons.prems by auto
        thus ?thesis unfolding a by (cases b) auto
      qed (use Cons.IH in auto)
    qed simp
  qed


  let ?M = "λA. ⋃{set ts |ts. (⋆, receive⟨ts⟩st) ∈ set A}"

  have 1: "?M (𝒜 ⋅lst ℐ) = ?M 𝒜 ⋅set ℐ" (is "?A = ?B")
  proof
    show "?A ⊆ ?B"
    proof
      fix t assume t: "t ∈ ?A"
      then obtain ts where ts: "t ∈ set ts" "(⋆, receive⟨ts⟩st) ∈ set (𝒜 ⋅lst ℐ)" by blast
      thus "t ∈ ?B" using 0[of ⋆ ts] by fastforce
    qed
    show "?B ⊆ ?A"
    proof
      fix t assume t: "t ∈ ?B"
      then obtain ts where ts: "t ∈ set ts ⋅set ℐ" "(⋆, receive⟨ts⟩st) ∈ set 𝒜" by blast
      hence "(⋆, receive⟨ts ⋅list ℐ⟩st) ∈ set (𝒜 ⋅lst ℐ)" using 0[of ⋆ "ts ⋅list ℐ"] by blast
      thus "t ∈ ?A" using ts(1) by force
    qed
  qed

  show ?thesis using 1 unfolding declassifiedlst_def by argo
qed

lemma declassifiedlst_star_receive_supset:
  "{t | t ts. (⋆, Receive ts) ∈ set 𝒜 ∧ t ∈ set ts} ⋅set ℐ ⊆ declassifiedlst 𝒜 ℐ"
unfolding declassifiedlst_alt_def by (fastforce intro: intruder_deduct.Axiom)

lemma ik_proj_subst_GSMP_subset:
  assumes I: "wtsubst I" "wftrms (subst_range I)" "interpretationsubst I"
  shows "ikst (proj_unl n A) ⋅set I ⊆ GSMP (trms_projlst n A)"
proof
  fix t assume "t ∈ ikst (proj_unl n A) ⋅set I"
  hence *: "t ∈ trms_projlst n A ⋅set I" by auto
  then obtain s where "s ∈ trms_projlst n A" "t = s ⋅ I" by auto
  hence "t ∈ SMP (trms_projlst 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 ∈ GSMP (trms_projlst n A)" unfolding GSMP_def by simp
qed

lemma ik_proj_subst_subterms_GSMP_subset:
  assumes I: "wtsubst I" "wftrms (subst_range I)" "interpretationsubst I"
  shows "subtermsset (ikst (proj_unl n A) ⋅set I) ⊆ GSMP (trms_projlst n A)" (is "?A ⊆ ?B")
proof
  fix t assume "t ⊑set ikst (proj_unl n A) ⋅set I"
  then obtain s where "s ∈ ikst (proj_unl n A) ⋅set I" "t ⊑ s" by fast
  thus "t ∈ ?B"
    using ik_proj_subst_GSMP_subset[OF I, of n A] ground_subterm[of s t]
          SMP.Subterm[of s "trmslst (proj n A)" t]
    unfolding GSMP_def 
    by blast
qed

lemma declassified_proj_eq: "declassifiedlst A I = declassifiedlst (proj n A) I"
unfolding declassifiedlst_alt_def proj_def by auto

lemma declassified_prefix_subset:
  assumes AB: "prefix A B"
  shows "declassifiedlst A I ⊆ declassifiedlst B I"
proof
  fix t assume t: "t ∈ declassifiedlst A I"
  obtain C where C: "B = A@C" using prefixE[OF AB] by metis
  show "t ∈ declassifiedlst B I"
    using t ideduct_mono[of
              "⋃{set ts |ts. (⋆, receive⟨ts⟩st) ∈ set A} ⋅set I" t 
              "⋃{set ts |ts. (⋆, receive⟨ts⟩st) ∈ set B} ⋅set I"]
    unfolding C declassifiedlst_alt_def by auto
qed

lemma declassified_proj_ik_subset:
  "declassifiedlst A I ⊆ {s. ikst (proj_unl n A) ⋅set I ⊢ s}"
    (is "?A A ⊆ ?P A A")
proof -
  have *: "⋃{set ts |ts. (⋆, receive⟨ts⟩st) ∈ set A} ⋅set I ⊆ ikst (proj_unl n A) ⋅set I"
    using proj_ikst_is_proj_rcv_set by fastforce
  show ?thesis
    using ideduct_mono[OF _ *] unfolding declassifiedlst_alt_def by blast
qed

lemma deduct_proj_priv_term_prefix_ex:
  assumes A: "ikst (proj_unl l A) ⋅set I ⊢ t"
    and t: "¬{} ⊢c t"
  shows "∃B k s. (k = ⋆ ∨ k = ln l) ∧ prefix (B@[(k,receive⟨s⟩st)]) A ∧
                 declassifiedlst ((B@[(k,receive⟨s⟩st)])) I = declassifiedlst A I ∧
                 ikst (proj_unl l (B@[(k,receive⟨s⟩st)])) = ikst (proj_unl l A)"
using A
proof (induction A rule: List.rev_induct)
  case Nil
  have "ikst (proj_unl l []) ⋅set I = {}" by auto
  thus ?case using Nil t deducts_eq_if_empty_ik[of t] by argo
next
  case (snoc a A)
  obtain k b where a: "a = (k,b)" by (metis surj_pair)
  let ?P = "k = ⋆ ∨ k = (ln l)"
  let ?Q = "∃ts. b = receive⟨ts⟩st"

  have 0: "ikst (proj_unl l (A@[a])) = ikst (proj_unl l A)" when "?P ⟹ ¬?Q"
    using that ikst_snoc_no_receive_eq[OF that, of I "proj_unl l A"]
    unfolding ikst_is_rcv_set a by (cases "k = ⋆ ∨ k = (ln l)") auto

  have 1: "declassifiedlst (A@[a]) I = declassifiedlst A I" when "?P ⟹ ¬?Q"
    using that snoc.prems unfolding declassifiedlst_alt_def a
    by (metis (no_types, lifting) UnCI UnE empty_iff insert_iff list.set prod.inject set_append)

  note 2 = snoc.prems snoc.IH 0 1

  show ?case
  proof (cases ?P)
    case True
    note T = this
    thus ?thesis
    proof (cases ?Q)
      case True thus ?thesis using T unfolding a by blast
    qed (use 2 in auto)
  qed (use 2 in auto)
qed


subsection ‹Lemmata: Homogeneous and Heterogeneous Terms (Deprecated Theory)›
text ‹The following theory is no longer needed for the compositionality result›
context
begin
private definition proj_specific where
  "proj_specific n t 𝒜 Secrets ≡ t ∈ GSMP (trms_projlst n 𝒜) - (Secrets ∪ {m. {} ⊢c m})"

private definition heterogeneouslst where
  "heterogeneouslst t 𝒜 Secrets ≡ (
    (∃l1 l2. ∃s1 ∈ subterms t. ∃s2 ∈ subterms t.
      l1 ≠ l2 ∧ proj_specific l1 s1 𝒜 Secrets ∧ proj_specific l2 s2 𝒜 Secrets))"

private abbreviation homogeneouslst where
  "homogeneouslst t 𝒜 Secrets ≡ ¬heterogeneouslst t 𝒜 Secrets"

private definition intruder_deduct_hom'::
  "('fun,'var) terms ⇒ ('fun,'var,'lbl) labeled_strand ⇒ ('fun,'var) terms ⇒ ('fun,'var) term
  ⇒ bool" (‹⟨_;_;_⟩ ⊢hom _› 50)
where
  "⟨M; 𝒜; Sec⟩ ⊢hom t ≡ ⟨M; λt. homogeneouslst t 𝒜 Sec ∧ t ∈ GSMP (trmslst 𝒜)⟩ ⊢r t"

private lemma GSMP_disjoint_fst_specific_not_snd_specific:
  assumes "GSMP_disjoint (trms_projlst l 𝒜) (trms_projlst l' 𝒜) Sec" "l ≠ l'"
  and "proj_specific l m 𝒜 Sec"
  shows "¬proj_specific l' m 𝒜 Sec"
using assms by (fastforce simp add: GSMP_disjoint_def proj_specific_def)

private lemma GSMP_disjoint_snd_specific_not_fst_specific:
  assumes "GSMP_disjoint (trms_projlst l 𝒜) (trms_projlst l' 𝒜) Sec"
  and "proj_specific l' m 𝒜 Sec"
  shows "¬proj_specific l m 𝒜 Sec"
using assms by (auto simp add: GSMP_disjoint_def proj_specific_def)

private lemma GSMP_disjoint_intersection_not_specific:
  assumes "GSMP_disjoint (trms_projlst l 𝒜) (trms_projlst l' 𝒜) Sec"
  and "t ∈ Sec ∨ {} ⊢c t"
  shows "¬proj_specific l t 𝒜 Sec" "¬proj_specific l t 𝒜 Sec"
using assms by (auto simp add: GSMP_disjoint_def proj_specific_def)

private lemma proj_specific_secrets_anti_mono:
  assumes "proj_specific l t 𝒜 Sec" "Sec' ⊆ Sec"
  shows "proj_specific l t 𝒜 Sec'"
using assms unfolding proj_specific_def by fast

private lemma heterogeneous_secrets_anti_mono:
  assumes "heterogeneouslst t 𝒜 Sec" "Sec' ⊆ Sec"
  shows "heterogeneouslst t 𝒜 Sec'"
using assms proj_specific_secrets_anti_mono unfolding heterogeneouslst_def by metis

private lemma homogeneous_secrets_mono:
  assumes "homogeneouslst t 𝒜 Sec'" "Sec' ⊆ Sec"
  shows "homogeneouslst t 𝒜 Sec"
using assms heterogeneous_secrets_anti_mono by blast

private lemma heterogeneous_supterm:
  assumes "heterogeneouslst t 𝒜 Sec" "t ⊑ t'"
  shows "heterogeneouslst t' 𝒜 Sec"
proof -
  obtain l1 l2 s1 s2 where *:
      "l1 ≠ l2"
      "s1 ⊑ t" "proj_specific l1 s1 𝒜 Sec"
      "s2 ⊑ t" "proj_specific l2 s2 𝒜 Sec"
    using assms(1) unfolding heterogeneouslst_def by fast
  thus ?thesis
    using term.order_trans[OF *(2) assms(2)] term.order_trans[OF *(4) assms(2)]
    by (auto simp add: heterogeneouslst_def)
qed

private lemma homogeneous_subterm:
  assumes "homogeneouslst t 𝒜 Sec" "t' ⊑ t"
  shows "homogeneouslst t' 𝒜 Sec"
by (metis assms heterogeneous_supterm)

private lemma proj_specific_subterm:
  assumes "t ⊑ t'" "proj_specific l t' 𝒜 Sec"
  shows "proj_specific l t 𝒜 Sec ∨ t ∈ Sec ∨ {} ⊢c t"
using GSMP_subterm[OF _ assms(1)] assms(2) by (auto simp add: proj_specific_def)

private lemma heterogeneous_term_is_Fun:
  assumes "heterogeneouslst t A S" shows "∃f T. t = Fun f T"
using assms by (cases t) (auto simp add: GSMP_def heterogeneouslst_def proj_specific_def)

private lemma proj_specific_is_homogeneous:
  assumes 𝒜: "∀l l'. l ≠ l' ⟶ GSMP_disjoint (trms_projlst l 𝒜) (trms_projlst l' 𝒜) Sec"
  and t: "proj_specific l m 𝒜 Sec"
  shows "homogeneouslst m 𝒜 Sec"
proof
  assume "heterogeneouslst m 𝒜 Sec"
  then obtain s l' where s: "s ∈ subterms m" "proj_specific l' s 𝒜 Sec" "l ≠ l'"
    unfolding heterogeneouslst_def by atomize_elim auto
  hence "s ∈ GSMP (trms_projlst l 𝒜)" "s ∈ GSMP (trms_projlst l' 𝒜)"
    using t by (auto simp add: GSMP_def proj_specific_def)
  hence "s ∈ Sec ∨ {} ⊢c s"
    using 𝒜 s(3) by (auto simp add: GSMP_disjoint_def)
  thus False using s(2) by (auto simp add: proj_specific_def)
qed

private lemma deduct_synth_homogeneous:
  assumes "{} ⊢c t"
  shows "homogeneouslst t 𝒜 Sec"
proof -
  have "∀s ∈ subterms t. {} ⊢c s" using deduct_synth_subterm[OF assms] by auto
  thus ?thesis unfolding heterogeneouslst_def proj_specific_def by auto
qed

private lemma GSMP_proj_is_homogeneous:
  assumes "∀l l'. l ≠ l' ⟶ GSMP_disjoint (trms_projlst l A) (trms_projlst l' A) Sec"
  and "t ∈ GSMP (trms_projlst l A)" "t ∉ Sec"
  shows "homogeneouslst t A Sec"
proof
  assume "heterogeneouslst t A Sec"
  then obtain s l' where s: "s ∈ subterms t" "proj_specific l' s A Sec" "l ≠ l'"
    unfolding heterogeneouslst_def by atomize_elim auto
  hence "s ∈ GSMP (trms_projlst l A)" "s ∈ GSMP (trms_projlst l' A)"
    using assms by (auto simp add: GSMP_def proj_specific_def)
  hence "s ∈ Sec ∨ {} ⊢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

private lemma homogeneous_is_not_proj_specific:
  assumes "homogeneouslst m 𝒜 Sec"
  shows "∃l::'lbl. ¬proj_specific l m 𝒜 Sec"
proof -
  let ?P = "λl s. proj_specific l s 𝒜 Sec"
  have "∀l1 l2. ∀s1∈subterms m. ∀s2∈subterms m. (l1 ≠ l2 ⟶ (¬?P l1 s1 ∨ ¬?P l2 s2))"
    using assms heterogeneouslst_def by metis
  then obtain l1 l2 where "l1 ≠ l2" "¬?P l1 m ∨ ¬?P l2 m"
    by (metis term.order_refl at_least_2_labels)
  thus ?thesis by metis
qed

private lemma secrets_are_homogeneous:
  assumes "∀s ∈ Sec. P s ⟶ (∀s' ∈ subterms s. {} ⊢c s' ∨ s' ∈ Sec)" "s ∈ Sec" "P s"
  shows "homogeneouslst s 𝒜 Sec"
using assms by (auto simp add: heterogeneouslst_def proj_specific_def)

private lemma GSMP_is_homogeneous:
  assumes 𝒜: "∀l l'. l ≠ l' ⟶ GSMP_disjoint (trms_projlst l 𝒜) (trms_projlst l' 𝒜) Sec"
  and t: "t ∈ GSMP (trmslst 𝒜)" "t ∉ Sec"
  shows "homogeneouslst t 𝒜 Sec"
proof -
  obtain n where n: "t ∈ GSMP (trms_projlst n 𝒜)" using in_GSMP_in_proj[OF t(1)] by atomize_elim auto
  show ?thesis using GSMP_proj_is_homogeneous[OF 𝒜 n t(2)] by metis
qed

private lemma GSMP_intersection_is_homogeneous:
  assumes 𝒜: "∀l l'. l ≠ l' ⟶ GSMP_disjoint (trms_projlst l 𝒜) (trms_projlst l' 𝒜) Sec"
    and t: "t ∈ GSMP (trms_projlst l 𝒜) ∩ GSMP (trms_projlst l' 𝒜)" "l ≠ l'"
  shows "homogeneouslst t 𝒜 Sec"
proof -
  define M where "M ≡ GSMP (trms_projlst l 𝒜)"
  define M' where "M' ≡ GSMP (trms_projlst l' 𝒜)"

  have t_in: "t ∈ M ∩ M'" "t ∈ GSMP (trmslst 𝒜)"
    using t(1) in_proj_in_GSMP[of t _ 𝒜]
    unfolding M_def M'_def by blast+

  have "M ∩ M' ⊆ Sec ∪ {m. {} ⊢c m}"
    using 𝒜 GSMP_disjointE[of l 𝒜 l' Sec] t(2)
    unfolding M_def M'_def by presburger
  moreover have "subtermsset (M ∩ M') = M ∩ M'"
    using GSMP_subterms unfolding M_def M'_def by blast
  ultimately have *: "subtermsset (M ∩ M') ⊆ Sec ∪ {m. {} ⊢c m}"
    by blast

  show ?thesis
  proof (cases "t ∈ Sec")
    case True thus ?thesis
      using * secrets_are_homogeneous[of Sec "λt. t ∈ M ∩ M'", OF _ _ t_in(1)]
      by fast
  qed (metis GSMP_is_homogeneous[OF 𝒜 t_in(2)])
qed

private lemma GSMP_is_homogeneous':
  assumes 𝒜: "∀l l'. l ≠ l' ⟶ GSMP_disjoint (trms_projlst l 𝒜) (trms_projlst l' 𝒜) Sec"
  and t: "t ∈ GSMP (trmslst 𝒜)"
         "t ∉ Sec - ⋃{GSMP (trms_projlst l1 𝒜) ∩ GSMP (trms_projlst l2 𝒜) | l1 l2. l1 ≠ l2}"
  shows "homogeneouslst t 𝒜 Sec"
using GSMP_is_homogeneous[OF 𝒜 t(1)] GSMP_intersection_is_homogeneous[OF 𝒜] t(2)
by blast

private lemma Ana_keys_homogeneous:
  assumes 𝒜: "∀l l'. l ≠ l' ⟶ GSMP_disjoint (trms_projlst l 𝒜) (trms_projlst l' 𝒜) Sec"
  and t: "t ∈ GSMP (trmslst 𝒜)"
  and k: "Ana t = (K,T)" "k ∈ set K"
         "k ∉ Sec - ⋃{GSMP (trms_projlst l1 𝒜) ∩ GSMP (trms_projlst l2 𝒜) | l1 l2. l1 ≠ l2}"
  shows "homogeneouslst k 𝒜 Sec"
proof (cases "k ∈ ⋃{GSMP (trms_projlst l1 𝒜) ∩ GSMP (trms_projlst l2 𝒜) | l1 l2. l1 ≠ l2}")
  case False
  hence "k ∉ Sec" using k(3) by fast
  moreover have "k ∈ GSMP (trmslst 𝒜)"
    using t SMP.Ana[OF _ k(1,2)] Ana_keys_fv[OF k(1)] k(2)
    unfolding GSMP_def by auto
  ultimately show ?thesis using GSMP_is_homogeneous[OF 𝒜, of k] by metis
qed (use GSMP_intersection_is_homogeneous[OF 𝒜] in blast)

end


subsection ‹Lemmata: Intruder Deduction Equivalences›
lemma deduct_if_hom_deduct: "⟨M;A⟩ ⊢GSMP m ⟹ M ⊢ m"
using deduct_if_restricted_deduct unfolding intruder_deduct_hom_def by blast

lemma hom_deduct_if_hom_ik:
  assumes "⟨M;A⟩ ⊢GSMP m" "∀m ∈ M. m ∈ GSMP (trmslst A)"
  shows "m ∈ GSMP (trmslst A)"
proof -
  let ?Q = "λm. m ∈ GSMP (trmslst A)"
  have "?Q t'" when "?Q t" "t' ⊑ t" for t t'
    using GSMP_subterm[OF _ that(2)] that(1)
    by blast
  thus ?thesis
    using assms(1) restricted_deduct_if_restricted_ik[OF _ assms(2)]
    unfolding intruder_deduct_hom_def
    by blast
qed

lemma deduct_hom_if_synth:
  assumes hom: "m ∈ GSMP (trmslst 𝒜)"
  and m: "M ⊢c m"
  shows "⟨M; 𝒜⟩ ⊢GSMP m"
proof -
  let ?Q = "λm. m ∈ GSMP (trmslst 𝒜)"
  have "?Q t'" when "?Q t" "t' ⊑ t" for t t'
    using GSMP_subterm[OF _ that(2)] that(1)
    by blast
  thus ?thesis
    using assms deduct_restricted_if_synth[of ?Q]
    unfolding intruder_deduct_hom_def
    by blast
qed

lemma hom_deduct_if_deduct:
  assumes M: "∀m ∈ M. m ∈ GSMP (trmslst 𝒜)"
    and m: "M ⊢ m" "m ∈ GSMP (trmslst 𝒜)"
  shows "⟨M; 𝒜⟩ ⊢GSMP m"
proof -
  let ?P = "λx. x ∈ GSMP (trmslst 𝒜)"

(*   have GSMP_hom: "homogeneouslst t 𝒜 Sec" when "t ∈ GSMP (trmslst 𝒜)" for t
    using 𝒜 GSMP_is_homogeneous[of 𝒜 Sec t]
          secrets_are_homogeneous[of Sec "λx. True" t 𝒜] that
    unfolding par_comp_def by blast *)

  have P_Ana: "?P k" when "?P t" "Ana t = (K, T)" "k ∈ set K" for t K T k
    using GSMP_Ana_key[OF _ that(2,3), of "trmslst 𝒜"] that (* GSMP_hom *)
    by presburger

  have P_subterm: "?P t'" when "?P t" "t' ⊑ t" for t t'
    using GSMP_subterm[of _ "trmslst 𝒜"] (* homogeneous_subterm[of _ 𝒜 Sec] *) that
    by blast

  have P_m: "?P m"
    using (* GSMP_hom[OF m(2)] *) m(2)
    by metis

  show ?thesis
    using restricted_deduct_if_deduct'[OF M _ _ m(1) P_m] P_Ana P_subterm
    unfolding intruder_deduct_hom_def
    by fast
qed


subsection ‹Lemmata: Deduction Reduction of Parallel Composable Constraints›
lemma par_comp_hom_deduct:
  assumes 𝒜: "par_comp 𝒜 Sec"
  and M: "∀l. M l ⊆ GSMP (trms_projlst l 𝒜)"
         "∀l. Discl ⊆ {s. M l ⊢ s}"
  and Sec: "∀l. ∀s ∈ Sec - Discl. ¬(⟨M l; 𝒜⟩ ⊢GSMP s)"
  and t: "⟨⋃l. M l; 𝒜⟩ ⊢GSMP t"
  shows "t ∉ Sec - Discl" (is ?A)
        "∀l. t ∈ GSMP (trms_projlst l 𝒜) ⟶ ⟨M l; 𝒜⟩ ⊢GSMP t" (is ?B)
proof -
  have M': "∀l. ∀m ∈ M l. m ∈ GSMP (trmslst 𝒜)"
  proof (intro allI ballI)
    fix l m show "m ∈ M l ⟹ m ∈ GSMP (trmslst 𝒜)" using M(1) in_proj_in_GSMP[of m l 𝒜] by blast
  qed

  have Discl_hom_deduct: "⟨M l; 𝒜⟩ ⊢GSMP u" when u: "u ∈ Discl" "u ∈ GSMP (trmslst 𝒜)" for l u
  proof-
    have "M l ⊢ u" using M(2) u by auto
    thus ?thesis using hom_deduct_if_deduct[of "M l" 𝒜 u] M(1) M' u by auto
  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 ∈ M lt" by atomize_elim auto
    show t_not_Sec: "t ∉ Sec - Discl"
    proof
      assume "t ∈ Sec - Discl"
      hence "∀l. ¬(⟨M l; 𝒜⟩ ⊢GSMP t)" using Sec by auto
      thus False using intruder_deduct_hom_AxiomH[OF t_in_proj_ik] by metis
    qed
    
    have 1: "∀l. t ∈ M l ⟶ t ∈ GSMP (trms_projlst l 𝒜)"
      using M(1,2) AxiomH by auto
  
    have 3: "{} ⊢c t ∨ t ∈ Discl"
      when "l1 ≠ l2" "t ∈ GSMP (trms_projlst l1 𝒜) ∩ GSMP (trms_projlst l2 𝒜)" for l1 l2
      using 𝒜 t_not_Sec that by (auto simp add: par_comp_def GSMP_disjoint_def)
  
    have 4: "t ∈ GSMP (trmslst 𝒜)" using M(1) M' t_in_proj_ik by auto
    
    show "∀l. t ∈ GSMP (trms_projlst l 𝒜) ⟶ ⟨M l; 𝒜⟩ ⊢GSMP t"
      by (metis (lifting) Int_iff empty_subsetI
            1 3 4 Discl_hom_deduct t_in_proj_ik
            intruder_deduct_hom_AxiomH[of t _ 𝒜]
            deduct_hom_if_synth[of t 𝒜 "{}"]
            ideduct_hom_mono[of "{}" 𝒜 t])
  next
    case (ComposeH T f)
    show "∀l. Fun f T ∈ GSMP (trms_projlst l 𝒜) ⟶ ⟨M l; 𝒜⟩ ⊢GSMP Fun f T"
    proof (intro allI impI)
      fix l
      assume "Fun f T ∈ GSMP (trms_projlst l 𝒜)"
      hence "t ∈ GSMP (trms_projlst l 𝒜)" when "t ∈ set T" for t
        using that GSMP_subterm[OF _ subtermeqI''] by auto
      thus "⟨M l; 𝒜⟩ ⊢GSMP Fun f T"
        using ComposeH.IH(2) intruder_deduct_hom_ComposeH[OF ComposeH.hyps(1,2) _ ComposeH.hyps(4)]
        by simp
    qed
    thus "Fun f T ∉ Sec - Discl"
      using Sec ComposeH.hyps(4) trmslst_union[of 𝒜] GSMP_Union[of 𝒜] by blast
  next
    case (DecomposeH t K T ti)
    have ti_subt: "ti ⊑ t" using Ana_subterm[OF DecomposeH.hyps(2)] ‹ti ∈ set T› by auto
    have t: "t ∈ GSMP (trmslst 𝒜)" using DecomposeH.hyps(1) hom_deduct_if_hom_ik M(1) M' by auto
    have ti: "ti ∈ GSMP (trmslst 𝒜)"
      using intruder_deduct_hom_DecomposeH[OF DecomposeH.hyps] hom_deduct_if_hom_ik M(1) M' by auto

    obtain l where l: "t ∈ GSMP (trms_projlst l 𝒜)"
      using in_GSMP_in_proj[of _ 𝒜] ti t by presburger

    have K_IH: "⟨M l; 𝒜⟩ ⊢GSMP k" when "k ∈ set K" for k
      using that GSMP_Ana_key[OF _ DecomposeH.hyps(2)] DecomposeH.IH(4) l by auto

    have ti_IH: "⟨M l; 𝒜⟩ ⊢GSMP ti"
      using K_IH DecomposeH.IH(2) l
            intruder_deduct_hom_DecomposeH[OF _ DecomposeH.hyps(2) _ ‹ti ∈ set T›]
      by blast
    thus ti_not_Sec: "ti ∉ Sec - Discl" using Sec by blast
    
    have "{} ⊢c ti ∨ ti ∈ Discl" when "ti ∈ GSMP (trms_projlst l' 𝒜)" "l' ≠ l" for l'
    proof - 
      have "GSMP_disjoint (trms_projlst l' 𝒜) (trms_projlst l 𝒜) Sec"
        using that(2) 𝒜 by (simp add: par_comp_def)
      thus ?thesis
        using ti_not_Sec GSMP_subterm[OF l ti_subt] that(1) by (auto simp add: GSMP_disjoint_def)
    qed
    hence "⟨M l'; 𝒜⟩ ⊢GSMP ti" when "ti ∈ GSMP (trms_projlst l' 𝒜)" "l' ≠ l" for l'
      using that Discl_hom_deduct[OF _ ti]
            deduct_hom_if_synth[OF ti, THEN ideduct_hom_mono[OF _ empty_subsetI]]
      by (cases "ti ∈ Discl") simp_all
    thus "∀l. ti ∈ GSMP (trms_projlst l 𝒜) ⟶ ⟨M l; 𝒜⟩ ⊢GSMP ti"
      using ti_IH by blast
  qed
qed

lemma par_comp_deduct_proj:
  assumes 𝒜: "par_comp 𝒜 Sec"
  and M: "∀l. M l ⊆ GSMP (trms_projlst l 𝒜)"
         "∀l. Discl ⊆ {s. M l ⊢ s}"
  and t: "(⋃l. M l) ⊢ t" "t ∈ GSMP (trms_projlst l 𝒜)"
  shows "M l ⊢ t ∨ (∃s ∈ Sec - Discl. ∃l. M l ⊢ s)"
using t
proof (induction t rule: intruder_deduct_induct)
  case (Axiom t)
  then obtain l' where t_in_ik_proj: "t ∈ M l'" by atomize_elim auto
  show ?case
  proof (cases "t ∈ Sec - Discl ∨ {} ⊢c t")
    case True thus ?thesis
      by (cases "t ∈ Sec - Discl")
         (metis intruder_deduct.Axiom[OF t_in_ik_proj],
          use ideduct_mono[of "{}" t "M l"] in blast)
  next
    case False
    hence "t ∉ Sec - Discl" "¬{} ⊢c t" "t ∈ GSMP (trms_projlst l 𝒜)" using Axiom by auto
    hence "(∀l'. l ≠ l' ⟶ t ∉ GSMP (trms_projlst l' 𝒜)) ∨ t ∈ Discl"
      using 𝒜 unfolding GSMP_disjoint_def par_comp_def by auto
    hence "(∀l'. l ≠ l' ⟶ t ∉ GSMP (trms_projlst l' 𝒜)) ∨ M l ⊢ t ∨ {} ⊢c t"
      using M by blast
    thus ?thesis
      by (cases "∃s ∈ M l. t ⊑ s ∧ {s} ⊢ t")
         (blast intro: ideduct_mono[of _ t "M l"],
          metis (no_types, lifting) False M(1) intruder_deduct.Axiom subsetCE t_in_ik_proj)
  qed
next
  case (Compose T f)
  hence "Fun f T ∈ GSMP (trms_projlst l 𝒜)" using Compose.prems by auto
  hence "t ∈ GSMP (trms_projlst l 𝒜)" when "t ∈ set T" for t using that unfolding GSMP_def by auto
  hence IH: "M l ⊢ t ∨ (∃s ∈ Sec - Discl. ∃l. M l ⊢ s)" when "t ∈ set T" for t
    using that Compose.IH by auto
  show ?case
    by (cases "∀t ∈ set T. M l ⊢ t")
       (metis intruder_deduct.Compose[OF Compose.hyps(1,2)], metis IH)
next
  case (Decompose t K T ti)
  have hom_ik: "m ∈ GSMP (trmslst 𝒜)" when m: "m ∈ M l" for m l
    using in_proj_in_GSMP[of m l 𝒜] M(1) m by blast

  have "⟨⋃l. M l; 𝒜⟩ ⊢GSMP ti"
    using intruder_deduct.Decompose[OF Decompose.hyps]
          hom_deduct_if_deduct[of "⋃l. M l"] hom_ik in_proj_in_GSMP[OF Decompose.prems(1)]
    by blast
  hence "(⟨M l; 𝒜⟩ ⊢GSMP ti) ∨ (∃s ∈ Sec-Discl. ∃l. ⟨M l; 𝒜⟩ ⊢GSMP s)"
    using par_comp_hom_deduct(2)[OF 𝒜 M] Decompose.prems(1)
    by blast
  thus ?case using deduct_if_hom_deduct[of _ 𝒜] by auto
qed


subsection ‹Theorem: Parallel Compositionality for Labeled Constraints›
lemma par_comp_prefix: assumes "par_comp (A@B) M" shows "par_comp A M"
proof -
  let ?L = "λl. trms_projlst l A ∪ trms_projlst l B"
  have "GSMP_disjoint (?L l1) (?L l2) M" when "l1 ≠ l2" for l1 l2
    using that assms unfolding par_comp_def
    by (metis trmsst_append proj_append(2) unlabel_append)
  hence "GSMP_disjoint (trms_projlst l1 A) (trms_projlst l2 A) M" when "l1 ≠ l2" for l1 l2
    using that SMP_union by (auto simp add: GSMP_def GSMP_disjoint_def)
  thus ?thesis using assms unfolding par_comp_def by blast
qed

theorem par_comp_constr_typed:
  assumes 𝒜: "par_comp 𝒜 Sec"
    and ℐ: "ℐ ⊨ ⟨unlabel 𝒜⟩" "interpretationsubst ℐ" "wtsubst ℐ" "wftrms (subst_range ℐ)"
  shows "(∀l. (ℐ ⊨ ⟨proj_unl l 𝒜⟩)) ∨
         (∃𝒜' l' t. prefix 𝒜' 𝒜 ∧ suffix [(l', receive⟨t⟩st)] 𝒜' ∧ (strand_leakslst 𝒜' Sec ℐ))"
proof -
  let ?sem = "λ𝒜. ⟦{}; 𝒜⟧d ℐ"
  let ?Q = "λ𝒜. ∀l. ?sem (proj_unl l 𝒜)"
  let ?L = "λ𝒜'. ∃t ∈ Sec - declassifiedlst 𝒜' ℐ. ∃l. ?sem (proj_unl l 𝒜'@[send⟨[t]⟩st])"
  let ?P = "λ𝒜 𝒜' l' ts. prefix (𝒜'@[(l',receive⟨ts⟩st)]) 𝒜 ∧ ?L (𝒜'@[(l',receive⟨ts⟩st)])"

  have "⟦{}; unlabel 𝒜⟧d ℐ" using ℐ by (simp add: constr_sem_d_def)
  with 𝒜 have aux: "?Q 𝒜 ∨ (∃𝒜'. prefix 𝒜' 𝒜 ∧ ?L 𝒜')"
  proof (induction "unlabel 𝒜" arbitrary: 𝒜 rule: List.rev_induct)
    case Nil
    hence "𝒜 = []" using unlabel_nil_only_if_nil by simp
    thus ?case by auto
  next
    case (snoc b B 𝒜)
    hence disj: "GSMP_disjoint (trms_projlst l1 𝒜) (trms_projlst l2 𝒜) Sec"
      when "l1 ≠ l2" for l1 l2
      using that by (auto simp add: par_comp_def)

    obtain a A n where a: "𝒜 = A@[a]" "a = (ln n, b) ∨ a = (⋆, b)"
      using unlabel_snoc_inv[OF snoc.hyps(2)[symmetric]] by atomize_elim auto
    hence A: "𝒜 = A@[(ln n, b)] ∨ 𝒜 = A@[(⋆, 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: "⟦{}; unlabel A⟧d ℐ" by (metis 1 snoc.prems(2) snoc.hyps(2) strand_sem_split(3))
    have IH: "(∀l. ⟦{}; proj_unl l A⟧d ℐ) ∨ (∃𝒜'. prefix 𝒜' A ∧ ?L 𝒜')"
      by (rule snoc.hyps(1)[OF 1 2 3])

    show ?case
    proof (cases "∀l. ⟦{}; proj_unl l A⟧d ℐ")
      case False
      then obtain 𝒜' where 𝒜': "prefix 𝒜' A" "?L 𝒜'" by (metis IH)
      hence "prefix 𝒜' (A@[a])" using a prefix_prefix[of _ A "[a]"] by simp
      thus ?thesis using 𝒜'(2) a by auto
    next
      case True
      note IH' = True
      show ?thesis
      proof (cases b)
        case (Send ts)
        hence "∀t ∈ set ts. ikst (unlabel A) ⋅set ℐ ⊢ t ⋅ ℐ"
          using a ‹⟦{}; unlabel 𝒜⟧d ℐ› strand_sem_split(2)[of "{}" "unlabel A" "unlabel [a]" ℐ]
                unlabel_append[of A "[a]"]
          by auto
        hence *: "∀t ∈ set ts. (⋃l. (ikst (proj_unl l A) ⋅set ℐ)) ⊢ t ⋅ ℐ"
          using proj_ik_union_is_unlabel_ik image_UN by metis

        have "ikst (proj_unl l 𝒜) = ikst (proj_unl l A)" for l
          using Send A 
          by (metis append_Nil2 ikst.simps(3) proj_unl_cons(3) proj_nil(2)
                    singleton_lst_proj(1,2) proj_ik_append)
        hence **: "ikst (proj_unl l A) ⋅set ℐ ⊆ GSMP (trms_projlst l 𝒜)" for l
          using ik_proj_subst_GSMP_subset[OF ℐ(3,4,2), of _ 𝒜]
          by auto

        note Discl =
          declassified_proj_ik_subset(1)[of A ℐ]

        have Sec: "ground Sec"
          using 𝒜 by (auto simp add: par_comp_def)

(*         have Sec_hom: "homogeneouslst s 𝒜 Sec" when "s ∈ Sec" for s
          using that secrets_are_homogeneous[of Sec "λ_. True" s 𝒜] snoc.prems(1)
          unfolding par_comp_def by auto *)

        have "∀m∈ikst (proj_unl l 𝒜) ⋅set ℐ. m ∈ GSMP (trmslst 𝒜)"
             "ikst (proj_unl l 𝒜) ⋅set ℐ ⊆ GSMP (trms_projlst l 𝒜)"
          for l
          using ik_proj_subst_GSMP_subset[OF ℐ(3,4,2), of _ 𝒜] GSMP_Union[of 𝒜] by auto
        moreover have "ikst (proj_unl l [a]) = {}" for l
          using Send proj_ikst_is_proj_rcv_set[of _ "[a]"] a(2) by auto
        ultimately have M: "∀l. ikst (proj_unl l A) ⋅set ℐ ⊆ GSMP (trms_projlst l 𝒜)"
          using a(1) proj_ik_append[of _ A "[a]"] by auto

        have prefix_A: "prefix A 𝒜" using A by auto

        have "s ⋅ ℐ = s"
          when "s ∈ Sec" for s
          using that Sec by auto
        hence leakage_case: "⟦{}; proj_unl l A@[Send1 s]⟧d ℐ"
          when "s ∈ Sec - declassifiedlst A ℐ" "ikst (proj_unl l A) ⋅set ℐ ⊢ s" for l s
          using that strand_sem_append(2) IH' by auto

        have proj_deduct_case_n:
            "∀m. m ≠ n ⟶ ⟦{}; proj_unl m (A@[a])⟧d ℐ"
            "∀t ∈ set ts. ikst (proj_unl n A) ⋅set ℐ ⊢ t ⋅ ℐ ⟹ ⟦{}; proj_unl n (A@[a])⟧d ℐ"
          when "a = (ln n, Send ts)"
          using that IH' proj_append(2)[of _ A] by auto

        have proj_deduct_case_star:
            "⟦{}; proj_unl l (A@[a])⟧d ℐ"
          when "a = (⋆, Send ts)" "∀t ∈ set ts. ikst (proj_unl l A) ⋅set ℐ ⊢ t ⋅ ℐ" for l
          using that IH' proj_append(2)[of _ A] by auto

        show ?thesis
        proof (cases "∃l. ∃m ∈ ikst (proj_unl l A) ⋅set ℐ. m ∈ Sec - declassifiedlst A ℐ")
          case True
          then obtain l s where ls: "s ∈ Sec - declassifiedlst A ℐ" "ikst (proj_unl l A) ⋅set ℐ ⊢ s"
            using intruder_deduct.Axiom by metis
          thus ?thesis using leakage_case prefix_A by blast
        next
          case False
          have A_decl_subset:
              "∀l. declassifiedlst A ℐ ⊆ {s. ikst (proj_unl l A) ⋅set ℐ ⊢ s}"
            using Discl unfolding a(1) by auto

          note deduct_proj_lemma = par_comp_deduct_proj[OF snoc.prems(1) M A_decl_subset]

          from a(2) show ?thesis
          proof
            assume "a = (ln n, b)"
            hence "a = (ln n, Send ts)" "∀t ∈ set ts. t ⋅ ℐ ∈ GSMP (trms_projlst n 𝒜)"
              using Send a(1) trms_projlst_append[of n A "[a]"]
                    GSMP_wt_substI[OF _ ℐ(3,4,2)]
              by (metis, force)
            hence
                "a = (ln n, Send ts)"
                "∀m. m ≠ n ⟶ ⟦{}; proj_unl m (A@[a])⟧d ℐ"
                "∀t ∈ set ts. ikst (proj_unl n A) ⋅set ℐ ⊢ t ⋅ ℐ ⟹ ⟦{}; proj_unl n (A@[a])⟧d ℐ"
                "∀t ∈ set ts. t ⋅ ℐ ∈ GSMP (trms_projlst n 𝒜)"
              using proj_deduct_case_n
              by auto
            hence "(∀l. ⟦{}; proj_unl l 𝒜⟧d ℐ) ∨
                   (∃s ∈ Sec-declassifiedlst A ℐ. ∃l. ikst (proj_unl l A) ⋅set ℐ ⊢ s)"
              using deduct_proj_lemma * unfolding a(1) list_all_iff by metis
            thus ?thesis using leakage_case prefix_A by metis
          next
            assume "a = (⋆, b)"
            hence ***: "a = (⋆, Send ts)" "list_all (λt. t ⋅ ℐ ∈ GSMP (trms_projlst l 𝒜)) ts" for l
              using Send a(1) GSMP_wt_substI[OF _ ℐ(3,4,2)] unfolding list_all_iff by (metis, force)
            hence "t ⋅ ℐ ∈ Sec - declassifiedlst A ℐ ∨
                   t ⋅ ℐ ∈ declassifiedlst A ℐ ∨
                   t ⋅ ℐ ∈ {m. {} ⊢c m}"
              when "t ∈ set ts" for t
              using that snoc.prems(1) a(1) at_least_2_labels
              unfolding par_comp_def GSMP_disjoint_def list_all_iff
              by blast
            hence "(∃t ∈ set ts. t ⋅ ℐ ∈ Sec - declassifiedlst A ℐ) ∨
                   (∀t ∈ set ts. t ⋅ ℐ ∈ declassifiedlst A ℐ ∨ t ⋅ ℐ ∈ {m. {} ⊢c m})"
              by blast
            thus ?thesis
            proof
              assume "∃t ∈ set ts. t ⋅ ℐ ∈ Sec - declassifiedlst A ℐ"
              then obtain t where t:
                  "t ∈ set ts" "t ⋅ ℐ ∈ Sec - declassifiedlst A ℐ"
                  "(⋃l. ikst (proj_unl l A) ⋅set ℐ) ⊢ t ⋅ ℐ"
                using * unfolding list_all_iff by blast
              have "∃s ∈ Sec - declassifiedlst A ℐ. ∃l. ikst (proj_unl l A) ⋅set ℐ ⊢ s"
                using t(1,2) deduct_proj_lemma[OF t(3)] ***(2) A a Discl
                unfolding list_all_iff by blast
              thus ?thesis using prefix_A leakage_case by blast
            next
              assume t: "∀t ∈ set ts. t ⋅ ℐ ∈ declassifiedlst A ℐ ∨ t ⋅ ℐ ∈ {m. {} ⊢c m}"
              moreover {
                fix t l assume "t ∈ set ts" "t ⋅ ℐ ∈ declassifiedlst A ℐ"
                hence "ikst (proj_unl l A) ⋅set ℐ ⊢ t ⋅ ℐ"
                  using intruder_deduct.Axiom Discl(1)[of l] 
                        ideduct_mono[of _ "t ⋅ ℐ" "ikst (proj_unl l A) ⋅set ℐ"]
                  by blast
              } moreover {
                fix t l assume "t ∈ set ts" "t ⋅ ℐ ∈ {m. {} ⊢c m}"
                hence "ikst (proj_unl l A) ⋅set ℐ ⊢ t ⋅ ℐ"
                  using ideduct_mono[OF deduct_if_synth] by blast
              } ultimately have "∀t ∈ set ts. ikst (proj_unl l A) ⋅set ℐ ⊢ t ⋅ ℐ" for l
                  by blast
              thus ?thesis using proj_deduct_case_star[OF ***(1)] a(1) by fast
            qed
          qed
        qed
      next
        case (Receive t)
        hence "⟦{}; proj_unl l 𝒜⟧d ℐ" for l
          using IH' a proj_append(2)[of l A "[a]"]
          unfolding unlabel_def proj_def by auto
        thus ?thesis by metis
      next
        case (Equality ac t t')
        hence *: "⟦M; [Equality ac t t']⟧d ℐ" for M
          using a ‹⟦{}; unlabel 𝒜⟧d ℐ› unlabel_append[of A "[a]"]
          by auto
        show ?thesis
          using a proj_append(2)[of _ A "[a]"] Equality
                strand_sem_append(2)[OF _ *] IH'
          unfolding unlabel_def proj_def by auto
      next
        case (Inequality X F)
        hence *: "⟦M; [Inequality X F]⟧d ℐ" for M
          using a ‹⟦{}; unlabel 𝒜⟧d ℐ› unlabel_append[of A "[a]"]
          by auto
        show ?thesis
          using a proj_append(2)[of _ A "[a]"] Inequality
                strand_sem_append(2)[OF _ *] IH'
          unfolding unlabel_def proj_def by auto
      qed
    qed
  qed
  
  from aux have "?Q 𝒜 ∨ (∃𝒜' l' t. ?P 𝒜 𝒜' l' t)"
  proof
    assume "∃𝒜'. prefix 𝒜' 𝒜 ∧ ?L 𝒜'"
    then obtain 𝒜' t l where 𝒜':
        "prefix 𝒜' 𝒜" "t ∈ Sec - declassifiedlst 𝒜' ℐ" "?sem (proj_unl l 𝒜'@[send⟨[t]⟩st])"
      by blast

    have *: "ikst (proj_unl l 𝒜') ⋅set ℐ ⊢ t ⋅ ℐ" "¬{} ⊢c t ⋅ ℐ"
      using 𝒜'(2) 𝒜 subst_ground_ident[of t ℐ] strand_sem_split(4)[OF 𝒜'(3)]
      unfolding par_comp_def by (simp, fastforce)

    obtain B k s where B:
        "k = ⋆ ∨ k = ln l" "prefix (B@[(k, receive⟨s⟩st)]) 𝒜'"
        "declassifiedlst (B@[(k, receive⟨s⟩st)]) ℐ = declassifiedlst 𝒜' ℐ"
        "ikst (proj_unl l (B@[(k, receive⟨s⟩st)])) = ikst (proj_unl l 𝒜')"
      using deduct_proj_priv_term_prefix_ex[OF *] by force
    
    have "prefix (B@[(k, receive⟨s⟩st)]) 𝒜" using B(2) 𝒜'(1) unfolding prefix_def by force
    moreover have "t ∈ Sec - declassifiedlst (B@[(k, receive⟨s⟩st)]) ℐ" using B(3) 𝒜'(2) by blast
    moreover have "?sem (proj_unl l (B@[(k, receive⟨s⟩st)])@[send⟨[t]⟩st])"
      using *(1)[unfolded B(4)[symmetric]]
            prefix_proj(2)[OF B(2), of l, unfolded prefix_def]
            strand_sem_split(3)[OF 𝒜'(3)]
            strand_sem_append(2)[
              of _ _ ℐ  "[send⟨[t]⟩st]",
              OF strand_sem_split(3)[of "{}" "proj_unl l (B@[(k, receive⟨s⟩st)])"]]
      by force
    ultimately show ?thesis by blast
  qed simp
  thus ?thesis
    using ℐ(1) unfolding strand_leakslst_def suffix_def constr_sem_d_def by blast
qed

end

locale labeled_typing =
  labeled_typed_model arity public Ana Γ label_witness1 label_witness2
+ typing_result arity public Ana Γ
  for arity::"'fun ⇒ nat"
    and public::"'fun ⇒ bool"
    and Ana::"('fun,'var) term ⇒ (('fun,'var) term list × ('fun,'var) term list)"
    and Γ::"('fun,'var) term ⇒ ('fun,'atom::finite) term_type"
    and label_witness1::"'lbl"
    and label_witness2::"'lbl"
begin

theorem par_comp_constr:
  assumes 𝒜: "par_comp 𝒜 Sec" "typing_cond (unlabel 𝒜)"
  and ℐ: "ℐ ⊨ ⟨unlabel 𝒜⟩" "interpretationsubst ℐ"
  shows "∃ℐτ. interpretationsubst ℐτ ∧ wtsubst ℐτ ∧ wftrms (subst_range ℐτ) ∧ (ℐτ ⊨ ⟨unlabel 𝒜⟩) ∧
              ((∀l. (ℐτ ⊨ ⟨proj_unl l 𝒜⟩)) ∨
               (∃𝒜' l' t. prefix 𝒜' 𝒜 ∧ suffix [(l', receive⟨t⟩st)] 𝒜' ∧
                          (strand_leakslst 𝒜' Sec ℐτ)))"
proof -
  from 𝒜(2) have *:
      "wfst {} (unlabel 𝒜)"
      "fvst (unlabel 𝒜) ∩ bvarsst (unlabel 𝒜) = {}"
      "tfrst (unlabel 𝒜)"
      "wftrms (trmsst (unlabel 𝒜))"
      "Ana_invar_subst (ikst (unlabel 𝒜) ∪ assignment_rhsst (unlabel 𝒜))"
    unfolding typing_cond_def tfrst_def by metis+

  obtain ℐτ where ℐτ: "ℐτ ⊨ ⟨unlabel 𝒜⟩" "interpretationsubst ℐτ" "wtsubst ℐτ" "wftrms (subst_range ℐτ)"
    using wt_attack_if_tfr_attack_d[OF * ℐ(2,1)] by metis

  show ?thesis using par_comp_constr_typed[OF 𝒜(1) ℐτ] ℐτ by auto
qed

end


subsection ‹Automated GSMP Disjointness›
locale labeled_typed_model' = typed_model' arity public Ana Γ +
  labeled_typed_model arity public Ana Γ label_witness1 label_witness2
  for arity::"'fun ⇒ nat"
    and public::"'fun ⇒ bool"
    and Ana::"('fun,(('fun,'atom::finite) term_type × nat)) term
              ⇒ (('fun,(('fun,'atom) term_type × nat)) term list
                 × ('fun,(('fun,'atom) term_type × nat)) term list)"
    and Γ::"('fun,(('fun,'atom) term_type × nat)) term ⇒ ('fun,'atom) term_type"
    and label_witness1 label_witness2::'lbl
begin

lemma GSMP_disjointI:
  fixes A' A B B'::"('fun, ('fun, 'atom) term × nat) terms"
  defines "f ≡ λM. {t ⋅ δ | t δ. t ∈ M ∧ wtsubst δ ∧ wftrms (subst_range δ) ∧ fv (t ⋅ δ) = {}}"
    and "δ ≡ var_rename (max_var_set (fvset A))"
  assumes A'_wf: "wftrms' arity A'"
    and B'_wf: "wftrms' arity B'"
    and A_inst: "has_all_wt_instances_of Γ A' A"
    and B_inst: "has_all_wt_instances_of Γ B' (B ⋅set δ)"
    and A_SMP_repr: "finite_SMP_representation arity Ana Γ A"
    and B_SMP_repr: "finite_SMP_representation arity Ana Γ (B ⋅set δ)"
    and AB_trms_disj:
      "∀t ∈ A. ∀s ∈ B ⋅set δ. Γ t = Γ s ∧ mgu t s ≠ None ⟶
        (intruder_synth' public arity {} t) ∨ ((∃u ∈ Sec. is_wt_instance_of_cond Γ t u))"
    and Sec_wf: "wftrms Sec"
  shows "GSMP_disjoint A' B' ((f Sec) - {m. {} ⊢c m})"
proof -
  have A_wf: "wftrms A" and B_wf: "wftrms (B ⋅set δ)"
    and A'_wf': "wftrms A'" and B'_wf': "wftrms B'"
    and A_finite: "finite A" and B_finite: "finite (B ⋅set δ)"
    using finite_SMP_representationD[OF A_SMP_repr]
          finite_SMP_representationD[OF B_SMP_repr]
          A'_wf B'_wf
    unfolding wftrms_code[symmetric] wftrm_code[symmetric] list_all_iff by blast+

  have AB_fv_disj: "fvset A ∩ fvset (B ⋅set δ) = {}"
    using var_rename_fv_set_disjoint'[of A B, unfolded δ_def[symmetric]] A_finite by simp

  have "GSMP_disjoint A (B ⋅set δ) ((f Sec) - {m. {} ⊢c m})"
    using ground_SMP_disjointI[OF AB_fv_disj A_SMP_repr B_SMP_repr Sec_wf AB_trms_disj]
    unfolding GSMP_def GSMP_disjoint_def f_def by blast
  moreover have "SMP A' ⊆ SMP A" "SMP B' ⊆ SMP (B ⋅set δ)"
    using SMP_I'[OF A'_wf' A_wf A_inst] SMP_SMP_subset[of A' A]
          SMP_I'[OF B'_wf' B_wf B_inst] SMP_SMP_subset[of B' "B ⋅set δ"]
    by (blast, blast)
  ultimately show ?thesis unfolding GSMP_def GSMP_disjoint_def by auto
qed

end

end