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⟨tsst)  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⟨tsst) = 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⟨tsst)  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⟨tsst)  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⟨tsst)  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⟨tsst)  set A} set I" t 
              "{set ts |ts. (, receive⟨tsst)  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⟨tsst)  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⟨sst)]) A 
                 declassifiedlst ((B@[(k,receive⟨sst)])) I = declassifiedlst A I 
                 ikst (proj_unl l (B@[(k,receive⟨sst)])) = 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⟨tsst"

  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. s1subterms m. s2subterms 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⟨tst)] 𝒜'  (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⟨tsst)]) 𝒜  ?L (𝒜'@[(l',receive⟨tsst)])"

  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 Ad " by (metis 1 snoc.prems(2) snoc.hyps(2) strand_sem_split(3))
    have IH: "(l. {}; proj_unl l Ad )  (𝒜'. prefix 𝒜' A  ?L 𝒜')"
      by (rule snoc.hyps(1)[OF 1 2 3])

    show ?case
    proof (cases "l. {}; proj_unl l Ad ")
      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 "mikst (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⟨sst)]) 𝒜'"
        "declassifiedlst (B@[(k, receive⟨sst)])  = declassifiedlst 𝒜' "
        "ikst (proj_unl l (B@[(k, receive⟨sst)])) = ikst (proj_unl l 𝒜')"
      using deduct_proj_priv_term_prefix_ex[OF *] by force
    
    have "prefix (B@[(k, receive⟨sst)]) 𝒜" using B(2) 𝒜'(1) unfolding prefix_def by force
    moreover have "t  Sec - declassifiedlst (B@[(k, receive⟨sst)]) " using B(3) 𝒜'(2) by blast
    moreover have "?sem (proj_unl l (B@[(k, receive⟨sst)])@[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⟨sst)])"]]
      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⟨tst)] 𝒜' 
                          (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