Theory Intruder_Deduction

(*  Title:      Intruder_Deduction.thy
    Author:     Andreas Viktor Hess, DTU
    SPDX-License-Identifier: BSD-3-Clause
*)

section ‹Dolev-Yao Intruder Model›
theory Intruder_Deduction
imports Messages More_Unification
begin

subsection ‹Syntax for the Intruder Deduction Relations›
consts INTRUDER_SYNTH::"('f,'v) terms ⇒ ('f,'v) term ⇒ bool" (infix ‹⊢c› 50)
consts INTRUDER_DEDUCT::"('f,'v) terms ⇒ ('f,'v) term ⇒ bool" (infix ‹⊢› 50)


subsection ‹Intruder Model Locale›
text ‹
  The intruder model is parameterized over arbitrary function symbols (e.g, cryptographic operators)
  and variables. It requires three functions:
  - ‹arity› that assigns an arity to each function symbol.
  - ‹public› that partitions the function symbols into those that will be available to the intruder
    and those that will not.
  - ‹Ana›, the analysis interface, that defines how messages can be decomposed (e.g., decryption).
›
locale intruder_model =
  fixes arity :: "'fun ⇒ nat"
    and public :: "'fun ⇒ bool"
    and Ana :: "('fun,'var) term ⇒ (('fun,'var) term list × ('fun,'var) term list)"
  assumes Ana_keys_fv: "⋀t K R. Ana t = (K,R) ⟹ fvset (set K) ⊆ fv t"
    and Ana_keys_wf: "⋀t k K R f T.
      Ana t = (K,R) ⟹ (⋀g S. Fun g S ⊑ t ⟹ length S = arity g)
                    ⟹ k ∈ set K ⟹ Fun f T ⊑ k ⟹ length T = arity f"
    and Ana_var[simp]: "⋀x. Ana (Var x) = ([],[])"
    and Ana_fun_subterm: "⋀f T K R. Ana (Fun f T) = (K,R) ⟹ set R ⊆ set T"
    and Ana_subst: "⋀t δ K R. ⟦Ana t = (K,R); K ≠ [] ∨ R ≠ []⟧ ⟹ Ana (t ⋅ δ) = (K ⋅list δ,R ⋅list δ)"
begin

lemma Ana_subterm: assumes "Ana t = (K,T)" shows "set T ⊂ subterms t"
using assms
by (cases t)
   (simp add: psubsetI,
    metis Ana_fun_subterm Fun_gt_params UN_I term.order_refl
          params_subterms psubsetI subset_antisym subset_trans)

lemma Ana_subterm': "s ∈ set (snd (Ana t)) ⟹ s ⊑ t"
using Ana_subterm by (cases "Ana t") auto

lemma Ana_vars: assumes "Ana t = (K,M)" shows "fvset (set K) ⊆ fv t" "fvset (set M) ⊆ fv t"
by (rule Ana_keys_fv[OF assms]) (use Ana_subterm[OF assms] subtermeq_vars_subset in auto)

abbreviation 𝒱 where "𝒱 ≡ UNIV::'var set"
abbreviation Σn (‹Σ⇧_›) where "Σ⇧n ≡ {f::'fun. arity f = n}"
abbreviation Σnpub (‹Σpub⇧_›) where "Σpub⇧n ≡ {f. public f} ∩ Σ⇧n"
abbreviation Σnpriv (‹Σpriv⇧_›) where "Σpriv⇧n ≡ {f. ¬public f} ∩ Σ⇧n"
abbreviation Σpub where "Σpub ≡ (⋃n. Σpub⇧n)"
abbreviation Σpriv where "Σpriv ≡ (⋃n. Σpriv⇧n)"
abbreviation Σ where "Σ ≡ (⋃n. Σ⇧n)"
abbreviation 𝒞 where "𝒞 ≡ Σ⇧0"
abbreviation 𝒞pub where "𝒞pub ≡ {f. public f} ∩ 𝒞"
abbreviation 𝒞priv where "𝒞priv ≡ {f. ¬public f} ∩ 𝒞"
abbreviation Σf where "Σf ≡ Σ - 𝒞"
abbreviation Σfpub where "Σfpub ≡ Σf ∩ Σpub"
abbreviation Σfpriv where "Σfpriv ≡ Σf ∩ Σpriv"

lemma disjoint_fun_syms: "Σf ∩ 𝒞 = {}" by auto
lemma id_union_univ: "Σf ∪ 𝒞 = UNIV" "Σ = UNIV" by auto
lemma const_arity_eq_zero[dest]: "c ∈ 𝒞 ⟹ arity c = 0" by simp
lemma const_pub_arity_eq_zero[dest]: "c ∈ 𝒞pub ⟹ arity c = 0 ∧ public c" by simp
lemma const_priv_arity_eq_zero[dest]: "c ∈ 𝒞priv ⟹ arity c = 0 ∧ ¬public c" by simp
lemma fun_arity_gt_zero[dest]: "f ∈ Σf ⟹ arity f > 0" by fastforce
lemma pub_fun_public[dest]: "f ∈ Σfpub ⟹ public f" by fastforce
lemma pub_fun_arity_gt_zero[dest]: "f ∈ Σfpub ⟹ arity f > 0" by fastforce

lemma Σf_unfold: "Σf = {f::'fun. arity f > 0}" by auto
lemma 𝒞_unfold: "𝒞 = {f::'fun. arity f = 0}" by auto
lemma 𝒞pub_unfold: "𝒞pub = {f::'fun. arity f = 0 ∧ public f}" by auto
lemma 𝒞priv_unfold: "𝒞priv = {f::'fun. arity f = 0 ∧ ¬public f}" by auto
lemma Σnpub_unfold: "(Σpub⇧n) = {f::'fun. arity f = n ∧ public f}" by auto
lemma Σnpriv_unfold: "(Σpriv⇧n) = {f::'fun. arity f = n ∧ ¬public f}" by auto
lemma Σfpub_unfold: "Σfpub = {f::'fun. arity f > 0 ∧ public f}" by auto
lemma Σfpriv_unfold: "Σfpriv = {f::'fun. arity f > 0 ∧ ¬public f}" by auto
lemma Σn_m_eq: "⟦(Σ⇧n) ≠ {}; (Σ⇧n) = (Σ⇧m)⟧ ⟹ n = m" by auto


subsection ‹Term Well-formedness›
definition "wftrm t ≡ ∀f T. Fun f T ⊑ t ⟶ length T = arity f"

abbreviation "wftrms T ≡ ∀t ∈ T. wftrm t"

lemma Ana_keys_wf': "Ana t = (K,T) ⟹ wftrm t ⟹ k ∈ set K ⟹ wftrm k"
using Ana_keys_wf unfolding wftrm_def by metis

lemma wf_trm_Var[simp]: "wftrm (Var x)" unfolding wftrm_def by simp

lemma wf_trm_subst_range_Var[simp]: "wftrms (subst_range Var)" by simp

lemma wf_trm_subst_range_iff: "(∀x. wftrm (θ x)) ⟷ wftrms (subst_range θ)"
by force

lemma wf_trm_subst_rangeD: "wftrms (subst_range θ) ⟹ wftrm (θ x)"
by (metis wf_trm_subst_range_iff)

lemma wf_trm_subst_rangeI[intro]:
  "(⋀x. wftrm (δ x)) ⟹ wftrms (subst_range δ)"
by (metis wf_trm_subst_range_iff)

lemma wf_trmI[intro]:
  assumes "⋀t. t ∈ set T ⟹ wftrm t" "length T = arity f"
  shows "wftrm (Fun f T)"
using assms unfolding wftrm_def by auto

lemma wf_trm_subterm: "⟦wftrm t; s ⊏ t⟧ ⟹ wftrm s"
unfolding wftrm_def by (induct t) auto

lemma wf_trm_subtermeq:
  assumes "wftrm t" "s ⊑ t"
  shows "wftrm s"
proof (cases "s = t")
  case False thus "wftrm s" using assms(2) wf_trm_subterm[OF assms(1)] by simp
qed (metis assms(1))

lemma wf_trm_param:
  assumes "wftrm (Fun f T)" "t ∈ set T"
  shows "wftrm t"
by (meson assms subtermeqI'' wf_trm_subtermeq)

lemma wf_trm_param_idx:
  assumes "wftrm (Fun f T)"
    and "i < length T"
  shows "wftrm (T ! i)"
using wf_trm_param[OF assms(1), of "T ! i"] assms(2)
by fastforce

lemma wf_trm_subst:
  assumes "wftrms (subst_range δ)"
  shows "wftrm t = wftrm (t ⋅ δ)"
proof
  show "wftrm t ⟹ wftrm (t ⋅ δ)"
  proof (induction t)
    case (Fun f T)
    hence "⋀t. t ∈ set T ⟹ wftrm t"
      by (meson wftrm_def Fun_param_is_subterm term.order_trans)
    hence "⋀t. t ∈ set T ⟹ wftrm (t ⋅ δ)" using Fun.IH by auto
    moreover have "length (map (λt. t ⋅ δ) T) = arity f"
      using Fun.prems unfolding wftrm_def by auto
    ultimately show ?case by fastforce
  qed (simp add: wf_trm_subst_rangeD[OF assms])

  show "wftrm (t ⋅ δ) ⟹ wftrm t"
  proof (induction t)
    case (Fun f T)
    hence "wftrm t" when "t ∈ set (map (λs. s ⋅ δ) T)" for t
      by (metis that wftrm_def Fun_param_is_subterm term.order_trans eval_term.simps(2)) 
    hence "wftrm t" when "t ∈ set T" for t using that Fun.IH by auto
    moreover have "length (map (λt. t ⋅ δ) T) = arity f"
      using Fun.prems unfolding wftrm_def by auto
    ultimately show ?case by fastforce
  qed (simp add: assms)
qed

lemma wf_trm_subst_singleton:
  assumes "wftrm t" "wftrm t'" shows "wftrm (t ⋅ Var(v := t'))"
proof -
  have "wftrm ((Var(v := t')) w)" for w using assms(2) unfolding wftrm_def by simp
  thus ?thesis using assms(1) wf_trm_subst[of "Var(v := t')" t, OF wf_trm_subst_rangeI] by simp
qed

lemma wf_trm_subst_rm_vars:
  assumes "wftrm (t ⋅ δ)"
  shows "wftrm (t ⋅ rm_vars X δ)"
using assms
proof (induction t)
  case (Fun f T)
  have "wftrm (t ⋅ δ)" when "t ∈ set T" for t
    using that wf_trm_param[of f "map (λt. t ⋅ δ) T"] Fun.prems
    by auto
  hence "wftrm (t ⋅ rm_vars X δ)" when "t ∈ set T" for t using that Fun.IH by simp
  moreover have "length T = arity f" using Fun.prems unfolding wftrm_def by auto
  ultimately show ?case unfolding wftrm_def by auto
qed simp

lemma wf_trm_subst_rm_vars': "wftrm (δ v) ⟹ wftrm (rm_vars X δ v)"
by auto

lemma wf_trms_subst:
  assumes "wftrms (subst_range δ)" "wftrms M"
  shows "wftrms (M ⋅set δ)"
by (metis (no_types, lifting) assms imageE wf_trm_subst)

lemma wf_trms_subst_rm_vars:
  assumes "wftrms (M ⋅set δ)"
  shows "wftrms (M ⋅set rm_vars X δ)"
using assms wf_trm_subst_rm_vars by blast

lemma wf_trms_subst_rm_vars':
  assumes "wftrms (subst_range δ)"
  shows "wftrms (subst_range (rm_vars X δ))"
using assms by force  

lemma wf_trms_subst_compose:
  assumes "wftrms (subst_range θ)" "wftrms (subst_range δ)"
  shows "wftrms (subst_range (θ ∘s δ))"
using assms subst_img_comp_subset' wf_trm_subst by blast 

lemma wf_trm_subst_compose:
  fixes δ::"('fun, 'v) subst"
  assumes "wftrm (θ x)" "⋀x. wftrm (δ x)"
  shows "wftrm ((θ ∘s δ) x)"
using wf_trm_subst[of δ "θ x", OF wf_trm_subst_rangeI[OF assms(2)]] assms(1)
      subst_subst_compose[of "Var x" θ δ]
by auto

lemma wf_trms_Var_range:
  assumes "subst_range δ ⊆ range Var"
  shows "wftrms (subst_range δ)"
using assms by fastforce

lemma wf_trms_subst_compose_Var_range:
  assumes "wftrms (subst_range θ)"
    and "subst_range δ ⊆ range Var"
  shows "wftrms (subst_range (δ ∘s θ))"
    and "wftrms (subst_range (θ ∘s δ))"
using assms wf_trms_subst_compose wf_trms_Var_range by metis+

lemma wf_trm_subst_inv: "wftrm (t ⋅ δ) ⟹ wftrm t"
unfolding wftrm_def by (induct t) auto

lemma wf_trms_subst_inv: "wftrms (M ⋅set δ) ⟹ wftrms M"
using wf_trm_subst_inv by fast

lemma wf_trm_subterms: "wftrm t ⟹ wftrms (subterms t)"
using wf_trm_subterm by blast

lemma wf_trms_subterms: "wftrms M ⟹ wftrms (subtermsset M)"
using wf_trm_subterms by blast

lemma wf_trm_arity: "wftrm (Fun f T) ⟹ length T = arity f"
unfolding wftrm_def by blast

lemma wf_trm_subterm_arity: "wftrm t ⟹ Fun f T ⊑ t ⟹ length T = arity f"
unfolding wftrm_def by blast

lemma unify_list_wf_trm:
  assumes "Unification.unify E B = Some U" "∀(s,t) ∈ set E. wftrm s ∧ wftrm t"
  and "∀(v,t) ∈ set B. wftrm t"
  shows "∀(v,t) ∈ set U. wftrm t"
using assms
proof (induction E B arbitrary: U rule: Unification.unify.induct)
  case (1 B U) thus ?case by auto
next
  case (2 f T g S E B U)
  have wf_fun: "wftrm (Fun f T)" "wftrm (Fun g S)" using "2.prems"(2) by auto
  from "2.prems"(1) obtain E' where *: "decompose (Fun f T) (Fun g S) = Some E'"
    and [simp]: "f = g" "length T = length S" "E' = zip T S"
    and **: "Unification.unify (E'@E) B = Some U"
    by (auto split: option.splits)
  hence "t ⊏ Fun f T" "t' ⊏ Fun g S" when "(t,t') ∈ set E'" for t t'
    using that by (metis zip_arg_subterm(1), metis zip_arg_subterm(2))
  hence "wftrm t" "wftrm t'" when "(t,t') ∈ set E'" for t t'
    using wf_trm_subterm wf_fun ‹f = g› that by blast+
  thus ?case using "2.IH"[OF * ** _ "2.prems"(3)] "2.prems"(2) by fastforce
next
  case (3 v t E B)
  hence *: "∀(w,x) ∈ set ((v, t) # B). wftrm x"
      and **: "∀(s,t) ∈ set E. wftrm s ∧ wftrm t" "wftrm t"
    by auto

  show ?case
  proof (cases "t = Var v")
    case True thus ?thesis using "3.prems" "3.IH"(1) by auto
  next
    case False
    hence "v ∉ fv t" using "3.prems"(1) by auto
    hence "Unification.unify (subst_list (subst v t) E) ((v, t)#B) = Some U"
      using ‹t ≠ Var v› "3.prems"(1) by auto
    moreover have "∀(s, t) ∈ set (subst_list (subst v t) E). wftrm s ∧ wftrm t"
      using wf_trm_subst_singleton[OF _ ‹wftrm t›] "3.prems"(2)
      unfolding subst_list_def subst_def by auto
    ultimately show ?thesis using "3.IH"(2)[OF ‹t ≠ Var v› ‹v ∉ fv t› _ _ *] by metis
  qed
next
  case (4 f T v E B U)
  hence *: "∀(w,x) ∈ set ((v, Fun f T) # B). wftrm x"
      and **: "∀(s,t) ∈ set E. wftrm s ∧ wftrm t" "wftrm (Fun f T)"
    by auto

  have "v ∉ fv (Fun f T)" using "4.prems"(1) by force
  hence "Unification.unify (subst_list (subst v (Fun f T)) E) ((v, Fun f T)#B) = Some U"
    using "4.prems"(1) by auto
  moreover have "∀(s, t) ∈ set (subst_list (subst v (Fun f T)) E). wftrm s ∧ wftrm t"
    using wf_trm_subst_singleton[OF _ ‹wftrm (Fun f T)›] "4.prems"(2)
    unfolding subst_list_def subst_def by auto
  ultimately show ?case using "4.IH"[OF ‹v ∉ fv (Fun f T)› _ _ *] by metis
qed

lemma mgu_wf_trm:
  assumes "mgu s t = Some σ" "wftrm s" "wftrm t"
  shows "wftrm (σ v)"
proof -
  from assms obtain σ' where "subst_of σ' = σ" "∀(v,t) ∈ set σ'. wftrm t"
    using unify_list_wf_trm[of "[(s,t)]" "[]"] by (auto simp: mgu_def split: option.splits)
  thus ?thesis
  proof (induction σ' arbitrary: σ v rule: List.rev_induct)
    case (snoc x σ' σ v)
    define θ where "θ = subst_of σ'"
    hence "wftrm (θ v)" for v using snoc.prems(2) snoc.IH[of θ] by fastforce 
    moreover obtain w t where x: "x = (w,t)" by (metis surj_pair) 
    hence σ: "σ = Var(w := t) ∘s θ" using snoc.prems(1) by (simp add: subst_def θ_def)
    moreover have "wftrm t" using snoc.prems(2) x by auto
    ultimately show ?case using wf_trm_subst[of _ t] unfolding subst_compose_def by auto
  qed (simp add: wftrm_def)
qed

lemma mgu_wf_trms:
  assumes "mgu s t = Some σ" "wftrm s" "wftrm t"
  shows "wftrms (subst_range σ)"
using mgu_wf_trm[OF assms] by simp

subsection ‹Definitions: Intruder Deduction Relations›
text ‹
  A standard Dolev-Yao intruder.
›
inductive intruder_deduct::"('fun,'var) terms ⇒ ('fun,'var) term ⇒ bool"
where
  Axiom[simp]:   "t ∈ M ⟹ intruder_deduct M t"
| Compose[simp]: "⟦length T = arity f; public f; ⋀t. t ∈ set T ⟹ intruder_deduct M t⟧
                  ⟹ intruder_deduct M (Fun f T)"
| Decompose:     "⟦intruder_deduct M t; Ana t = (K, T); ⋀k. k ∈ set K ⟹ intruder_deduct M k;
                   ti ∈ set T⟧
                  ⟹ intruder_deduct M ti"

text ‹
  A variant of the intruder relation which limits the intruder to composition only.
›
inductive intruder_synth::"('fun,'var) terms ⇒ ('fun,'var) term ⇒ bool"
where
  AxiomC[simp]:   "t ∈ M ⟹ intruder_synth M t"
| ComposeC[simp]: "⟦length T = arity f; public f; ⋀t. t ∈ set T ⟹ intruder_synth M t⟧
                    ⟹ intruder_synth M (Fun f T)"

adhoc_overloading INTRUDER_DEDUCT intruder_deduct
adhoc_overloading INTRUDER_SYNTH intruder_synth

lemma intruder_deduct_induct[consumes 1, case_names Axiom Compose Decompose]:
  assumes "M ⊢ t" "⋀t. t ∈ M ⟹ P M t"
          "⋀T f. ⟦length T = arity f; public f;
                  ⋀t. t ∈ set T ⟹ M ⊢ t;
                  ⋀t. t ∈ set T ⟹ P M t⟧ ⟹ P M (Fun f T)"
          "⋀t K T ti. ⟦M ⊢ t; P M t; Ana t = (K, T); ⋀k. k ∈ set K ⟹ M ⊢ k;
                       ⋀k. k ∈ set K ⟹ P M k; ti ∈ set T⟧ ⟹ P M ti"
  shows "P M t"
using assms by (induct rule: intruder_deduct.induct) blast+

lemma intruder_synth_induct[consumes 1, case_names AxiomC ComposeC]:
  fixes M::"('fun,'var) terms" and t::"('fun,'var) term"
  assumes "M ⊢c t" "⋀t. t ∈ M ⟹ P M t"
          "⋀T f. ⟦length T = arity f; public f;
                  ⋀t. t ∈ set T ⟹ M ⊢c t;
                  ⋀t. t ∈ set T ⟹ P M t⟧ ⟹ P M (Fun f T)"
  shows "P M t"
using assms by (induct rule: intruder_synth.induct) auto


subsection ‹Definitions: Analyzed Knowledge and Public Ground Well-formed Terms (PGWTs)›
definition analyzed::"('fun,'var) terms ⇒ bool" where
  "analyzed M ≡ ∀t. M ⊢ t ⟷ M ⊢c t"

definition analyzed_in where
  "analyzed_in t M ≡ ∀K R. (Ana t = (K,R) ∧ (∀k ∈ set K. M ⊢c k)) ⟶ (∀r ∈ set R. M ⊢c r)"

definition decomp_closure::"('fun,'var) terms ⇒ ('fun,'var) terms ⇒ bool" where
  "decomp_closure M M' ≡ ∀t. M ⊢ t ∧ (∃t' ∈ M. t ⊑ t') ⟷ t ∈ M'"

inductive public_ground_wf_term::"('fun,'var) term ⇒ bool" where
  PGWT[simp]: "⟦public f; arity f = length T;
                ⋀t. t ∈ set T ⟹ public_ground_wf_term t⟧
                  ⟹ public_ground_wf_term (Fun f T)"

abbreviation "public_ground_wf_terms ≡ {t. public_ground_wf_term t}"

lemma public_const_deduct:
  assumes "c ∈ 𝒞pub"
  shows "M ⊢ Fun c []" "M ⊢c Fun c []"
proof -
  have "arity c = 0" "public c" using const_arity_eq_zero ‹c ∈ 𝒞pub› by auto
  thus "M ⊢ Fun c []" "M ⊢c Fun c []"
    using intruder_synth.ComposeC[OF _ ‹public c›, of "[]"]
          intruder_deduct.Compose[OF _ ‹public c›, of "[]"]
    by auto
qed

lemma public_const_deduct'[simp]:
  assumes "arity c = 0" "public c"
  shows "M ⊢ Fun c []" "M ⊢c Fun c []"
using intruder_deduct.Compose[of "[]" c] intruder_synth.ComposeC[of "[]" c] assms by simp_all

lemma private_fun_deduct_in_ik:
  assumes t: "M ⊢ t" "Fun f T ∈ subterms t"
    and f: "¬public f"
  shows "Fun f T ∈ subtermsset M"
using t
proof (induction t rule: intruder_deduct.induct)
  case Decompose thus ?case by (meson Ana_subterm psubsetD term.order_trans)
qed (auto simp add: f in_subterms_Union)

lemma private_fun_deduct_in_ik':
  assumes t: "M ⊢ Fun f T"
    and f: "¬public f"
  shows "Fun f T ∈ subtermsset M"
by (rule private_fun_deduct_in_ik[OF t term.order_refl f])

lemma pgwt_public: "⟦public_ground_wf_term t; Fun f T ⊑ t⟧ ⟹ public f"
by (induct t rule: public_ground_wf_term.induct) auto

lemma pgwt_ground: "public_ground_wf_term t ⟹ fv t = {}"
by (induct t rule: public_ground_wf_term.induct) auto

lemma pgwt_fun: "public_ground_wf_term t ⟹ ∃f T. t = Fun f T"
using pgwt_ground[of t] by (cases t) auto

lemma pgwt_arity: "⟦public_ground_wf_term t; Fun f T ⊑ t⟧ ⟹ arity f = length T"
by (induct t rule: public_ground_wf_term.induct) auto

lemma pgwt_wellformed: "public_ground_wf_term t ⟹ wftrm t"
by (induct t rule: public_ground_wf_term.induct) auto

lemma pgwt_deducible: "public_ground_wf_term t ⟹ M ⊢c t"
by (induct t rule: public_ground_wf_term.induct) auto

lemma pgwt_is_empty_synth: "public_ground_wf_term t ⟷ {} ⊢c t"
proof -
  { fix M::"('fun,'var) term set" assume "M ⊢c t" "M = {}" hence "public_ground_wf_term t"
      by (induct t rule: intruder_synth.induct) auto
  }
  thus ?thesis using pgwt_deducible by auto
qed

lemma ideduct_synth_subst_apply:
  fixes M::"('fun,'var) terms" and t::"('fun,'var) term"
  assumes "{} ⊢c t" "⋀v. M ⊢c θ v"
  shows "M ⊢c t ⋅ θ"
proof -
  { fix M'::"('fun,'var) term set" assume "M' ⊢c t" "M' = {}" hence "M ⊢c t ⋅ θ"
    proof (induction t rule: intruder_synth.induct)
      case (ComposeC T f M')
      hence "length (map (λt. t ⋅ θ) T) = arity f" "⋀x. x ∈ set (map (λt. t ⋅ θ) T) ⟹ M ⊢c x"
        by auto
      thus ?case using intruder_synth.ComposeC[of "map (λt. t ⋅ θ) T" f M] ‹public f› by fastforce
    qed simp
  }
  thus ?thesis using assms by metis
qed
  

subsection ‹Lemmata: Monotonicity, Deduction of Private Constants, etc.›
context
begin
lemma ideduct_mono:
  "⟦M ⊢ t; M ⊆ M'⟧ ⟹ M' ⊢ t"
proof (induction rule: intruder_deduct.induct)
  case (Decompose M t K T ti)
  have "∀k. k ∈ set K ⟶ M' ⊢ k" using Decompose.IH ‹M ⊆ M'› by simp
  moreover have "M' ⊢ t" using Decompose.IH ‹M ⊆ M'› by simp
  ultimately show ?case using Decompose.hyps intruder_deduct.Decompose by blast
qed auto

lemma ideduct_synth_mono:
  fixes M::"('fun,'var) terms" and t::"('fun,'var) term"
  shows "⟦M ⊢c t; M ⊆ M'⟧ ⟹ M' ⊢c t"
by (induct rule: intruder_synth.induct) auto

context
begin

― ‹Used by ‹inductive_set››
private lemma ideduct_mono_set[mono_set]:
  "M ⊆ N ⟹ M ⊢ t ⟶ N ⊢ t"
  "M ⊆ N ⟹ M ⊢c t ⟶ N ⊢c t"
using ideduct_mono ideduct_synth_mono by (blast, blast)

end

lemma ideduct_reduce:
  "⟦M ∪ M' ⊢ t; ⋀t'. t' ∈ M' ⟹ M ⊢ t'⟧ ⟹ M ⊢ t"
proof (induction rule: intruder_deduct_induct)
  case Decompose thus ?case using intruder_deduct.Decompose by blast 
qed auto

lemma ideduct_synth_reduce:
  fixes M::"('fun,'var) terms" and t::"('fun,'var) term"
  shows "⟦M ∪ M' ⊢c t; ⋀t'. t' ∈ M' ⟹ M ⊢c t'⟧ ⟹ M ⊢c t"
by (induct rule: intruder_synth_induct) auto

lemma ideduct_mono_eq:
  assumes "∀t. M ⊢ t ⟷ M' ⊢ t" shows "M ∪ N ⊢ t ⟷ M' ∪ N ⊢ t"
proof
  show "M ∪ N ⊢ t ⟹ M' ∪ N ⊢ t"
  proof (induction t rule: intruder_deduct_induct)
    case (Axiom t) thus ?case
    proof (cases "t ∈ M")
      case True
      hence "M ⊢ t" using intruder_deduct.Axiom by metis
      thus ?thesis using assms ideduct_mono[of M' t "M' ∪ N"] by simp
    qed auto
  next
    case (Compose T f) thus ?case using intruder_deduct.Compose by auto
  next
    case (Decompose t K T ti) thus ?case using intruder_deduct.Decompose[of "M' ∪ N" t K T] by auto
  qed

  show "M' ∪ N ⊢ t ⟹ M ∪ N ⊢ t"
  proof (induction t rule: intruder_deduct_induct)
    case (Axiom t) thus ?case
    proof (cases "t ∈ M'")
      case True
      hence "M' ⊢ t" using intruder_deduct.Axiom by metis
      thus ?thesis using assms ideduct_mono[of M t "M ∪ N"] by simp
    qed auto
  next
    case (Compose T f) thus ?case using intruder_deduct.Compose by auto
  next
    case (Decompose t K T ti) thus ?case using intruder_deduct.Decompose[of "M ∪ N" t K T] by auto
  qed
qed

lemma deduct_synth_subterm:
  fixes M::"('fun,'var) terms" and t::"('fun,'var) term"
  assumes "M ⊢c t" "s ∈ subterms t" "∀m ∈ M. ∀s ∈ subterms m. M ⊢c s"
  shows "M ⊢c s"
using assms by (induct t rule: intruder_synth.induct) auto

lemma deduct_if_synth[intro, dest]: "M ⊢c t ⟹ M ⊢ t"
by (induct rule: intruder_synth.induct) auto

private lemma ideduct_ik_eq: assumes "∀t ∈ M. M' ⊢ t" shows "M' ⊢ t ⟷ M' ∪ M ⊢ t"
by (meson assms ideduct_mono ideduct_reduce sup_ge1)

private lemma synth_if_deduct_empty: "{} ⊢ t ⟹ {} ⊢c t"
proof (induction t rule: intruder_deduct_induct)
  case (Decompose t K M m)
  then obtain f T where "t = Fun f T" "m ∈ set T"
    using Ana_fun_subterm Ana_var by (cases t) fastforce+
  with Decompose.IH(1) show ?case by (induction rule: intruder_synth_induct) auto
qed auto

private lemma ideduct_deduct_synth_mono_eq:
  assumes "∀t. M ⊢ t ⟷ M' ⊢c t" "M ⊆ M'"
  and "∀t. M' ∪ N ⊢ t ⟷ M' ∪ N ∪ D ⊢c t"
  shows "M ∪ N ⊢ t ⟷ M' ∪ N ∪ D ⊢c t"
proof -
  have "∀m ∈ M'. M ⊢ m" using assms(1) by auto
  hence "∀t. M ⊢ t ⟷ M' ⊢ t" by (metis assms(1,2) deduct_if_synth ideduct_reduce sup.absorb2)
  hence "∀t. M' ∪ N ⊢ t ⟷ M ∪ N ⊢ t" by (meson ideduct_mono_eq)
  thus ?thesis by (meson assms(3))
qed

lemma ideduct_subst: "M ⊢ t ⟹ M ⋅set δ ⊢ t ⋅ δ"
proof (induction t rule: intruder_deduct_induct)
  case (Compose T f)
  hence "length (map (λt. t ⋅ δ) T) = arity f" "⋀t. t ∈ set T ⟹ M ⋅set δ ⊢ t ⋅ δ" by auto
  thus ?case using intruder_deduct.Compose[OF _ Compose.hyps(2), of "map (λt. t ⋅ δ) T"] by auto
next
  case (Decompose t K M' m')
  hence "Ana (t ⋅ δ) = (K ⋅list δ, M' ⋅list δ)"
        "⋀k. k ∈ set (K ⋅list δ) ⟹ M ⋅set δ ⊢ k"
        "m' ⋅ δ ∈ set (M' ⋅list δ)"
    using Ana_subst[OF Decompose.hyps(2)] by fastforce+
  thus ?case using intruder_deduct.Decompose[OF Decompose.IH(1)] by metis
qed simp

lemma ideduct_synth_subst:
  fixes M::"('fun,'var) terms" and t::"('fun,'var) term" and δ::"('fun,'var) subst"
  shows "M ⊢c t ⟹ M ⋅set δ ⊢c t ⋅ δ"
proof (induction t rule: intruder_synth_induct)
  case (ComposeC T f)
  hence "length (map (λt. t ⋅ δ) T) = arity f" "⋀t. t ∈ set T ⟹ M ⋅set δ ⊢c t ⋅ δ" by auto
  thus ?case using intruder_synth.ComposeC[OF _ ComposeC.hyps(2), of "map (λt. t ⋅ δ) T"] by auto
qed simp

lemma ideduct_vars:
  assumes "M ⊢ t"
  shows "fv t ⊆ fvset M"
using assms 
proof (induction t rule: intruder_deduct_induct)
  case (Decompose t K T ti) thus ?case
    using Ana_vars(2) fv_subset by blast 
qed auto

lemma ideduct_synth_vars:
  fixes M::"('fun,'var) terms" and t::"('fun,'var) term"
  assumes "M ⊢c t"
  shows "fv t ⊆ fvset M"
using assms by (induct t rule: intruder_synth_induct) auto

lemma ideduct_synth_priv_fun_in_ik:
  fixes M::"('fun,'var) terms" and t::"('fun,'var) term"
  assumes "M ⊢c t" "f ∈ funs_term t" "¬public f"
  shows "f ∈ ⋃(funs_term ` M)"
using assms by (induct t rule: intruder_synth_induct) auto

lemma ideduct_synth_priv_const_in_ik:
  fixes M::"('fun,'var) terms" and t::"('fun,'var) term"
  assumes "M ⊢c Fun c []" "¬public c"
  shows "Fun c [] ∈ M"
using intruder_synth.cases[OF assms(1)] assms(2) by fast

lemma ideduct_synth_ik_replace:
  fixes M::"('fun,'var) terms" and t::"('fun,'var) term"
  assumes "∀t ∈ M. N ⊢c t"
    and "M ⊢c t"
  shows "N ⊢c t"
using assms(2,1) by (induct t rule: intruder_synth.induct) auto
end

subsection ‹Lemmata: Analyzed Intruder Knowledge Closure›
lemma deducts_eq_if_analyzed: "analyzed M ⟹ M ⊢ t ⟷ M ⊢c t"
unfolding analyzed_def by auto

lemma closure_is_superset: "decomp_closure M M' ⟹ M ⊆ M'"
unfolding decomp_closure_def by force

lemma deduct_if_closure_deduct: "⟦M' ⊢ t; decomp_closure M M'⟧ ⟹ M ⊢ t"
proof (induction t rule: intruder_deduct.induct)
  case (Decompose M' t K T ti)
  thus ?case using intruder_deduct.Decompose[OF _ ‹Ana t = (K,T)› _ ‹ti ∈ set T›] by simp
qed (auto simp add: decomp_closure_def)

lemma deduct_if_closure_synth: "⟦decomp_closure M M'; M' ⊢c t⟧ ⟹ M ⊢ t"
using deduct_if_closure_deduct by blast

lemma decomp_closure_subterms_composable:
  assumes "decomp_closure M M'"
  and "M' ⊢c t'" "M' ⊢ t" "t ⊑ t'"
  shows "M' ⊢c t"
using ‹M' ⊢c t'› assms
proof (induction t' rule: intruder_synth.induct)
  case (AxiomC t' M')
  have "M ⊢ t" using ‹M' ⊢ t› deduct_if_closure_deduct AxiomC.prems(1) by blast
  moreover
  { have "∃s ∈ M. t' ⊑ s" using ‹t' ∈ M'› AxiomC.prems(1) unfolding decomp_closure_def by blast
    hence "∃s ∈ M. t ⊑ s" using ‹t ⊑ t'› term.order_trans by auto
  }
  ultimately have "t ∈ M'" using AxiomC.prems(1) unfolding decomp_closure_def by blast
  thus ?case by simp
next
  case (ComposeC T f M')
  let ?t' = "Fun f T"
  { assume "t = ?t'" have "M' ⊢c t" using ‹M' ⊢c ?t'› ‹t = ?t'› by simp }
  moreover
  { assume "t ≠ ?t'"
    have "∃x ∈ set T. t ⊑ x" using ‹t ⊑ ?t'› ‹t ≠ ?t'› by simp
    hence "M' ⊢c t" using ComposeC.IH ComposeC.prems(1,3) ComposeC.hyps(3) by blast
  }
  ultimately show ?case using cases_simp[of "t = ?t'" "M' ⊢c t"] by simp
qed

lemma decomp_closure_analyzed:
  assumes "decomp_closure M M'"
  shows "analyzed M'"
proof -
  { fix t assume "M' ⊢ t" have "M' ⊢c t" using ‹M' ⊢ t› assms
    proof (induction t rule: intruder_deduct.induct)
      case (Decompose M' t K T ti) 
      hence "M' ⊢ ti" using Decompose.hyps intruder_deduct.Decompose by blast
      moreover have "ti ⊑ t"
        using Decompose.hyps(4) Ana_subterm[OF Decompose.hyps(2)] by blast
      moreover have "M' ⊢c t" using Decompose.IH(1) Decompose.prems by blast
      ultimately show "M' ⊢c ti" using decomp_closure_subterms_composable Decompose.prems by blast
    qed auto
  }
  moreover have "∀t. M ⊢c t ⟶ M ⊢ t" by auto
  ultimately show ?thesis by (auto simp add: decomp_closure_def analyzed_def)
qed

lemma analyzed_if_all_analyzed_in:
  assumes M: "∀t ∈ M. analyzed_in t M"
  shows "analyzed M"
proof (unfold analyzed_def, intro allI iffI)
  fix t
  assume t: "M ⊢ t"
  thus "M ⊢c t"
  proof (induction t rule: intruder_deduct_induct)
    case (Decompose t K T ti)
    { assume "t ∈ M"
      hence ?case
        using M Decompose.IH(2) Decompose.hyps(2,4)
        unfolding analyzed_in_def by fastforce
    } moreover {
      fix f S assume "t = Fun f S" "⋀s. s ∈ set S ⟹ M ⊢c s"
      hence ?case using Ana_fun_subterm[of f S] Decompose.hyps(2,4) by blast
    } ultimately show ?case using intruder_synth.cases[OF Decompose.IH(1), of ?case] by blast
  qed simp_all
qed auto

lemma analyzed_is_all_analyzed_in:
  "(∀t ∈ M. analyzed_in t M) ⟷ analyzed M"
proof
  show "analyzed M ⟹ ∀t ∈ M. analyzed_in t M"
    unfolding analyzed_in_def analyzed_def
    by (auto intro: intruder_deduct.Decompose[OF intruder_deduct.Axiom])
qed (rule analyzed_if_all_analyzed_in)

lemma ik_has_synth_ik_closure:
  fixes M :: "('fun,'var) terms"
  shows "∃M'. (∀t. M ⊢ t ⟷ M' ⊢c t) ∧ decomp_closure M M' ∧ (finite M ⟶ finite M')"
proof -
  let ?M' = "{t. M ⊢ t ∧ (∃t' ∈ M. t ⊑ t')}"

  have M'_closes: "decomp_closure M ?M'" unfolding decomp_closure_def by simp
  hence "M ⊆ ?M'" using closure_is_superset by simp

  have "∀t. ?M' ⊢c t ⟶ M ⊢ t" using deduct_if_closure_synth[OF M'_closes] by blast 
  moreover have "∀t. M ⊢ t ⟶ ?M' ⊢ t" using ideduct_mono[OF _ ‹M ⊆ ?M'›] by simp
  moreover have "analyzed ?M'" using decomp_closure_analyzed[OF M'_closes] .
  ultimately have "∀t. M ⊢ t ⟷ ?M' ⊢c t" unfolding analyzed_def by blast
  moreover have "finite M ⟶ finite ?M'" by auto
  ultimately show ?thesis using M'_closes by blast
qed

lemma deducts_eq_if_empty_ik:
  "{} ⊢ t ⟷ {} ⊢c t"
using analyzed_is_all_analyzed_in[of "{}"] deducts_eq_if_analyzed[of "{}" t] by blast


subsection ‹Intruder Variants: Numbered and Composition-Restricted Intruder Deduction Relations›
text ‹
  A variant of the intruder relation which restricts composition to only those terms that satisfy
  a given predicate Q.
›
inductive intruder_deduct_restricted::
  "('fun,'var) terms ⇒ (('fun,'var) term ⇒ bool) ⇒ ('fun,'var) term ⇒ bool"
  (‹⟨_;_⟩ ⊢r _› 50)
where
  AxiomR[simp]:   "t ∈ M ⟹ ⟨M; Q⟩ ⊢r t"
| ComposeR[simp]: "⟦length T = arity f; public f; ⋀t. t ∈ set T ⟹ ⟨M; Q⟩ ⊢r t; Q (Fun f T)⟧
                    ⟹ ⟨M; Q⟩ ⊢r Fun f T"
| DecomposeR:     "⟦⟨M; Q⟩ ⊢r t; Ana t = (K, T); ⋀k. k ∈ set K ⟹ ⟨M; Q⟩ ⊢r k; ti ∈ set T⟧
                    ⟹ ⟨M; Q⟩ ⊢r ti"

text ‹
  A variant of the intruder relation equipped with a number representing the height of the
  derivation tree (i.e., ‹⟨M; k⟩ ⊢n t› iff k is the maximum number of applications of the compose
  and decompose rules in any path of the derivation tree for ‹M ⊢ t›).
›
inductive intruder_deduct_num::
  "('fun,'var) terms ⇒ nat ⇒ ('fun,'var) term ⇒ bool"
  (‹⟨_; _⟩ ⊢n _› 50)
where
  AxiomN[simp]:   "t ∈ M ⟹ ⟨M; 0⟩ ⊢n t"
| ComposeN[simp]: "⟦length T = arity f; public f; ⋀t. t ∈ set T ⟹ ⟨M; steps t⟩ ⊢n t⟧
                    ⟹ ⟨M; Suc (Max (insert 0 (steps ` set T)))⟩ ⊢n Fun f T"
| DecomposeN:     "⟦⟨M; n⟩ ⊢n t; Ana t = (K, T); ⋀k. k ∈ set K ⟹ ⟨M; steps k⟩ ⊢n k; ti ∈ set T⟧
                    ⟹ ⟨M; Suc (Max (insert n (steps ` set K)))⟩ ⊢n ti"

lemma intruder_deduct_restricted_induct[consumes 1, case_names AxiomR ComposeR DecomposeR]:
  assumes "⟨M; Q⟩ ⊢r t" "⋀t. t ∈ M ⟹ P M Q t"
          "⋀T f. ⟦length T = arity f; public f;
                  ⋀t. t ∈ set T ⟹ ⟨M; Q⟩ ⊢r t;
                  ⋀t. t ∈ set T ⟹ P M Q t; Q (Fun f T)
                  ⟧ ⟹ P M Q (Fun f T)"
          "⋀t K T ti. ⟦⟨M; Q⟩ ⊢r t; P M Q t; Ana t = (K, T); ⋀k. k ∈ set K ⟹ ⟨M; Q⟩ ⊢r k;
                       ⋀k. k ∈ set K ⟹ P M Q k; ti ∈ set T⟧ ⟹ P M Q ti"
  shows "P M Q t"
using assms by (induct t rule: intruder_deduct_restricted.induct) blast+

lemma intruder_deduct_num_induct[consumes 1, case_names AxiomN ComposeN DecomposeN]:
  assumes "⟨M; n⟩ ⊢n t" "⋀t. t ∈ M ⟹ P M 0 t"
          "⋀T f steps.
              ⟦length T = arity f; public f;
               ⋀t. t ∈ set T ⟹ ⟨M; steps t⟩ ⊢n t;
               ⋀t. t ∈ set T ⟹ P M (steps t) t⟧
              ⟹ P M (Suc (Max (insert 0 (steps ` set T)))) (Fun f T)"
          "⋀t K T ti steps n.
              ⟦⟨M; n⟩ ⊢n t; P M n t; Ana t = (K, T);
               ⋀k. k ∈ set K ⟹ ⟨M; steps k⟩ ⊢n k;
               ti ∈ set T; ⋀k. k ∈ set K ⟹ P M (steps k) k⟧
              ⟹ P M (Suc (Max (insert n (steps ` set K)))) ti"
  shows "P M n t"
using assms by (induct rule: intruder_deduct_num.induct) blast+

lemma ideduct_restricted_mono:
  "⟦⟨M; P⟩ ⊢r t; M ⊆ M'⟧ ⟹ ⟨M'; P⟩ ⊢r t"
proof (induction rule: intruder_deduct_restricted_induct)
  case (DecomposeR t K T ti)
  have "∀k. k ∈ set K ⟶ ⟨M'; P⟩ ⊢r k" using DecomposeR.IH ‹M ⊆ M'› by simp
  moreover have "⟨M'; P⟩ ⊢r t" using DecomposeR.IH ‹M ⊆ M'› by simp
  ultimately show ?case
    using DecomposeR
          intruder_deduct_restricted.DecomposeR[OF _ DecomposeR.hyps(2) _ DecomposeR.hyps(4)]
    by blast
qed auto


subsection ‹Lemmata: Intruder Deduction Equivalences›
lemma deduct_if_restricted_deduct: "⟨M;P⟩ ⊢r m ⟹ M ⊢ m"
proof (induction m rule: intruder_deduct_restricted_induct)
  case (DecomposeR t K T ti) thus ?case using intruder_deduct.Decompose by blast
qed simp_all

lemma restricted_deduct_if_restricted_ik:
  assumes "⟨M;P⟩ ⊢r m" "∀m ∈ M. P m"
  and P: "∀t t'. P t ⟶ t' ⊑ t ⟶ P t'"
  shows "P m"
using assms(1)
proof (induction m rule: intruder_deduct_restricted_induct)
  case (DecomposeR t K T ti)
  obtain f S where "t = Fun f S" using Ana_var ‹ti ∈ set T› ‹Ana t = (K, T)› by (cases t) auto
  thus ?case using DecomposeR assms(2) P Ana_subterm by blast
qed (simp_all add: assms(2))

lemma deduct_restricted_if_synth:
  assumes P: "P m" "∀t t'. P t ⟶ t' ⊑ t ⟶ P t'"
  and m: "M ⊢c m"
  shows "⟨M; P⟩ ⊢r m"
using m P(1)
proof (induction m rule: intruder_synth_induct)
  case (ComposeC T f)
  hence "⟨M; P⟩ ⊢r t" when t: "t ∈ set T" for t
    using t P(2) subtermeqI''[of _ T f]
    by fastforce
  thus ?case
    using intruder_deduct_restricted.ComposeR[OF ComposeC.hyps(1,2)] ComposeC.prems(1)
    by metis
qed simp

lemma deduct_zero_in_ik:
  assumes "⟨M; 0⟩ ⊢n t" shows "t ∈ M"
proof -
  { fix k assume "⟨M; k⟩ ⊢n t" hence "k > 0 ∨ t ∈ M" by (induct t) auto
  } thus ?thesis using assms by auto
qed

lemma deduct_if_deduct_num: "⟨M; k⟩ ⊢n t ⟹ M ⊢ t"
by (induct t rule: intruder_deduct_num.induct)
   (metis intruder_deduct.Axiom,
    metis intruder_deduct.Compose,
    metis intruder_deduct.Decompose)

lemma deduct_num_if_deduct: "M ⊢ t ⟹ ∃k. ⟨M; k⟩ ⊢n t"
proof (induction t rule: intruder_deduct_induct)
  case (Compose T f)
  then obtain steps where *: "∀t ∈ set T. ⟨M; steps t⟩ ⊢n t" by atomize_elim metis
  then obtain n where "∀t ∈ set T. steps t ≤ n"
    using finite_nat_set_iff_bounded_le[of "steps ` set T"]
    by auto
  thus ?case using ComposeN[OF Compose.hyps(1,2), of M steps] * by force
next
  case (Decompose t K T ti)
  hence "⋀u. u ∈ insert t (set K) ⟹ ∃k. ⟨M; k⟩ ⊢n u" by auto
  then obtain steps where *: "⟨M; steps t⟩ ⊢n t" "∀t ∈ set K. ⟨M; steps t⟩ ⊢n t" by (metis insert_iff)
  then obtain n where "steps t ≤ n" "∀t ∈ set K. steps t ≤ n"
    using finite_nat_set_iff_bounded_le[of "steps ` insert t (set K)"]
    by auto
  thus ?case using DecomposeN[OF _ Decompose.hyps(2) _ Decompose.hyps(4), of M _ steps] * by force
qed (metis AxiomN)

lemma deduct_normalize:
  assumes M: "∀m ∈ M. ∀f T. Fun f T ⊑ m ⟶ P f T"
  and t: "⟨M; k⟩ ⊢n t" "Fun f T ⊑ t" "¬P f T"
  shows "∃l ≤ k. (⟨M; l⟩ ⊢n Fun f T) ∧ (∀t ∈ set T. ∃j < l. ⟨M; j⟩ ⊢n t)"
using t
proof (induction t rule: intruder_deduct_num_induct)
  case (AxiomN t) thus ?case using M by auto
next
  case (ComposeN T' f' steps) thus ?case
  proof (cases "Fun f' T' = Fun f T")
    case True
    hence "⟨M; Suc (Max (insert 0 (steps ` set T')))⟩ ⊢n Fun f T" "T = T'"
      using intruder_deduct_num.ComposeN[OF ComposeN.hyps] by auto
    moreover have "⋀t. t ∈ set T ⟹ ⟨M; steps t⟩ ⊢n t"
      using True ComposeN.hyps(3) by auto
    moreover have "⋀t. t ∈ set T ⟹ steps t < Suc (Max (insert 0 (steps ` set T)))"
      using Max_less_iff[of "insert 0 (steps ` set T)" "Suc (Max (insert 0 (steps ` set T)))"]
      by auto
    ultimately show ?thesis by auto
  next
    case False
    then obtain t' where t': "t' ∈ set T'" "Fun f T ⊑ t'" using ComposeN by auto
    hence "∃l ≤ steps t'. (⟨M; l⟩ ⊢n Fun f T) ∧ (∀t ∈ set T. ∃j < l. ⟨M; j⟩ ⊢n t)"
      using ComposeN.IH[OF _ _ ComposeN.prems(2)] by auto
    moreover have "steps t' < Suc (Max (insert 0 (steps ` set T')))"
      using Max_less_iff[of "insert 0 (steps ` set T')" "Suc (Max (insert 0 (steps ` set T')))"]
      using t'(1) by auto
    ultimately show ?thesis using ComposeN.hyps(3)[OF t'(1)]
      by (meson Suc_le_eq le_Suc_eq le_trans)
  qed
next
  case (DecomposeN t K T' ti steps n)
  hence *: "Fun f T ⊑ t"
    using term.order_trans[of "Fun f T" ti t] Ana_subterm[of t K T']
    by blast
  have "∃l ≤ n. (⟨M; l⟩ ⊢n Fun f T) ∧ (∀t' ∈ set T. ∃j < l. ⟨M; j⟩ ⊢n t')"
    using DecomposeN.IH(1)[OF * DecomposeN.prems(2)] by auto
  moreover have "n < Suc (Max (insert n (steps ` set K)))"
      using Max_less_iff[of "insert n (steps ` set K)" "Suc (Max (insert n (steps ` set K)))"]
      by auto
  ultimately show ?case using DecomposeN.hyps(4) by (meson Suc_le_eq le_Suc_eq le_trans)
qed

lemma deduct_inv:
  assumes "⟨M; n⟩ ⊢n t"
  shows "t ∈ M ∨
         (∃f T. t = Fun f T ∧ public f ∧ length T = arity f ∧ (∀t ∈ set T. ∃l < n. ⟨M; l⟩ ⊢n t)) ∨
         (∃m ∈ subtermsset M.
            (∃l < n. ⟨M; l⟩ ⊢n m) ∧ (∀k ∈ set (fst (Ana m)). ∃l < n. ⟨M; l⟩ ⊢n k) ∧
            t ∈ set (snd (Ana m)))"
    (is "?P t n ∨ ?Q t n ∨ ?R t n")
using assms
proof (induction n arbitrary: t rule: nat_less_induct)
  case (1 n t) thus ?case
  proof (cases n)
    case 0
    hence "t ∈ M" using deduct_zero_in_ik "1.prems"(1) by metis
    thus ?thesis by auto
  next
    case (Suc n')
    hence "⟨M; Suc n'⟩ ⊢n t"
          "∀m < Suc n'. ∀x. (⟨M; m⟩ ⊢n x) ⟶ ?P x m ∨ ?Q x m ∨ ?R x m"
      using "1.prems" "1.IH" by blast+
    hence "?P t (Suc n') ∨ ?Q t (Suc n') ∨ ?R t (Suc n')"
    proof (induction t rule: intruder_deduct_num_induct)
      case (AxiomN t) thus ?case by simp
    next
      case (ComposeN T f steps)
      have "⋀t. t ∈ set T ⟹ steps t < Suc (Max (insert 0 (steps ` set T)))"
          using Max_less_iff[of "insert 0 (steps ` set T)" "Suc (Max (insert 0 (steps ` set T)))"]
          by auto
      thus ?case using ComposeN.hyps by metis
    next
      case (DecomposeN t K T ti steps n)
      have 0: "n < Suc (Max (insert n (steps ` set K)))"
              "⋀k. k ∈ set K ⟹ steps k < Suc (Max (insert n (steps ` set K)))"
        using Max_less_iff[of "insert n (steps ` set K)" "Suc (Max (insert n (steps ` set K)))"]
        by auto

      have IH1: "?P t j ∨ ?Q t j ∨ ?R t j" when jt: "j < n" "⟨M; j⟩ ⊢n t" for j t
        using jt DecomposeN.prems(1) 0(1)
        by simp

      have IH2: "?P t n ∨ ?Q t n ∨ ?R t n"
        using DecomposeN.IH(1) IH1
        by simp

      have 1: "∀k ∈ set (fst (Ana t)). ∃l < Suc (Max (insert n (steps ` set K))). ⟨M; l⟩ ⊢n k"
        using DecomposeN.hyps(1,2,3) 0(2)
        by auto
    
      have 2: "ti ∈ set (snd (Ana t))"
        using DecomposeN.hyps(2,4)
        by fastforce
    
      have 3: "t ∈ subtermsset M" when "t ∈ set (snd (Ana m))" "m ⊑set M" for m
        using that(1) Ana_subterm[of m _ "snd (Ana m)"] in_subterms_subset_Union[OF that(2)]
        by (metis (no_types, lifting) prod.collapse psubsetD subsetCE subsetD) 
    
      have 4: "?R ti (Suc (Max (insert n (steps ` set K))))" when "?R t n"
        using that 0(1) 1 2 3 DecomposeN.hyps(1)
        by (metis (no_types, lifting)) 
    
      have 5: "?R ti (Suc (Max (insert n (steps ` set K))))" when "?P t n"
        using that 0(1) 1 2 DecomposeN.hyps(1)
        by blast
    
      have 6: ?case when *: "?Q t n"
      proof -
        obtain g S where g:
            "t = Fun g S" "public g" "length S = arity g" "∀t ∈ set S. ∃l < n. ⟨M; l⟩ ⊢n t"
          using * by atomize_elim auto
        then obtain l where l: "l < n" "⟨M; l⟩ ⊢n ti"
          using 0(1) DecomposeN.hyps(2,4) Ana_fun_subterm[of g S K T] by blast
    
        have **: "l < Suc (Max (insert n (steps ` set K)))" using l(1) 0(1) by simp
    
        show ?thesis using IH1[OF l] less_trans[OF _ **] by fastforce
      qed

      show ?case using IH2 4 5 6 by argo
    qed
    thus ?thesis using Suc by fast
  qed
qed

lemma deduct_inv':
  assumes "M ⊢ Fun f ts"
  shows "Fun f ts ⊑set M ∨ (∀t ∈ set ts. M ⊢ t)"
proof -
  obtain k where k: "intruder_deduct_num M k (Fun f ts)"
    using deduct_num_if_deduct[OF assms] by fast

  have "Fun f ts ⊑set M ∨ (∀t ∈ set ts. ∃l. intruder_deduct_num M l t)"
    using deduct_inv[OF k] Ana_subterm'[of "Fun f ts"] in_subterms_subset_Union by blast
  thus ?thesis using deduct_if_deduct_num by blast
qed

lemma restricted_deduct_if_deduct:
  assumes M: "∀m ∈ M. ∀f T. Fun f T ⊑ m ⟶ P (Fun f T)"
  and P_subterm: "∀f T t. M ⊢ Fun f T ⟶ P (Fun f T) ⟶ t ∈ set T ⟶ P t"
  and P_Ana_key: "∀t K T k. M ⊢ t ⟶ P t ⟶ Ana t = (K, T) ⟶ M ⊢ k ⟶ k ∈ set K ⟶ P k"
  and m: "M ⊢ m" "P m"
  shows "⟨M; P⟩ ⊢r m"
proof -
  { fix k assume "⟨M; k⟩ ⊢n m"
    hence ?thesis using m(2)
    proof (induction k arbitrary: m rule: nat_less_induct)
      case (1 n m) thus ?case
      proof (cases n)
        case 0
        hence "m ∈ M" using deduct_zero_in_ik "1.prems"(1) by metis
        thus ?thesis by auto
      next
        case (Suc n')
        hence "⟨M; Suc n'⟩ ⊢n m"
              "∀m < Suc n'. ∀x. (⟨M; m⟩ ⊢n x) ⟶ P x ⟶ ⟨M;P⟩ ⊢r x"
          using "1.prems" "1.IH" by blast+
        thus ?thesis using "1.prems"(2)
        proof (induction m rule: intruder_deduct_num_induct)
          case (ComposeN T f steps)
          have *: "steps t < Suc (Max (insert 0 (steps ` set T)))" when "t ∈ set T" for t
            using Max_less_iff[of "insert 0 (steps ` set T)"] that
            by blast

          have **: "P t" when "t ∈ set T" for t
            using P_subterm ComposeN.prems(2) that
                  Fun_param_is_subterm[OF that]
                  intruder_deduct.Compose[OF ComposeN.hyps(1,2)]
                  deduct_if_deduct_num[OF ComposeN.hyps(3)]
            by blast

          have "⟨M; P⟩ ⊢r t" when "t ∈ set T" for t
            using ComposeN.prems(1) ComposeN.hyps(3)[OF that] *[OF that] **[OF that]
            by blast
          thus ?case
            by (metis intruder_deduct_restricted.ComposeR[OF ComposeN.hyps(1,2)] ComposeN.prems(2))
        next
          case (DecomposeN t K T ti steps l)
          show ?case
          proof (cases "P t")
            case True
            hence "⋀k. k ∈ set K ⟹ P k"
              using P_Ana_key DecomposeN.hyps(1,2,3) deduct_if_deduct_num
              by blast
            moreover have
                "⋀k m x. k ∈ set K ⟹ m < steps k ⟹ ⟨M; m⟩ ⊢n x ⟹ P x ⟹ ⟨M;P⟩ ⊢r x"
            proof -
              fix k m x assume *: "k ∈ set K" "m < steps k" "⟨M; m⟩ ⊢n x" "P x"
              have "steps k ∈ insert l (steps ` set K)" using *(1) by simp
              hence "m < Suc (Max (insert l (steps ` set K)))"
                using less_trans[OF *(2), of "Suc (Max (insert l (steps ` set K)))"]
                      Max_less_iff[of "insert l (steps ` set K)"
                                      "Suc (Max (insert l (steps ` set K)))"]
                by auto
              thus "⟨M;P⟩ ⊢r x" using DecomposeN.prems(1) *(3,4) by simp
            qed
            ultimately have "⋀k. k ∈ set K ⟹ ⟨M; P⟩ ⊢r k"
              using DecomposeN.IH(2) by auto
            moreover have "⟨M; P⟩ ⊢r t"
              using True DecomposeN.prems(1) DecomposeN.hyps(1) le_imp_less_Suc
                    Max_less_iff[of "insert l (steps ` set K)" "Suc (Max (insert l (steps ` set K)))"]
              by blast
            ultimately show ?thesis
              using intruder_deduct_restricted.DecomposeR[OF _ DecomposeN.hyps(2)
                                                             _ DecomposeN.hyps(4)]
              by metis
          next
            case False
            obtain g S where gS: "t = Fun g S" using DecomposeN.hyps(2,4) by (cases t) auto
            hence *: "Fun g S ⊑ t" "¬P (Fun g S)" using False by force+
            have "∃j<l. ⟨M; j⟩ ⊢n ti"
              using gS DecomposeN.hyps(2,4) Ana_fun_subterm[of g S K T]
                    deduct_normalize[of M "λf T. P (Fun f T)", OF M DecomposeN.hyps(1) *]
              by force
            hence "∃j<Suc (Max (insert l (steps ` set K))). ⟨M; j⟩ ⊢n ti"
              using Max_less_iff[of "insert l (steps ` set K)"
                                    "Suc (Max (insert l (steps ` set K)))"]
                    less_trans[of _ l "Suc (Max (insert l (steps ` set K)))"]
              by blast
            thus ?thesis using DecomposeN.prems(1,2) by meson
          qed
        qed auto
      qed
    qed
  } thus ?thesis using deduct_num_if_deduct m(1) by metis
qed

lemma restricted_deduct_if_deduct':
  assumes "∀m ∈ M. P m"
    and "∀t t'. P t ⟶ t' ⊑ t ⟶ P t'"
    and "∀t K T k. P t ⟶ Ana t = (K, T) ⟶ k ∈ set K ⟶ P k"
    and "M ⊢ m" "P m"
  shows "⟨M; P⟩ ⊢r m"
using restricted_deduct_if_deduct[of M P m] assms
by blast

lemma private_const_deduct:
  assumes c: "¬public c" "M ⊢ (Fun c []::('fun,'var) term)"
  shows "Fun c [] ∈ M ∨
         (∃m ∈ subtermsset M. M ⊢ m ∧ (∀k ∈ set (fst (Ana m)). M ⊢ m) ∧
                             Fun c [] ∈ set (snd (Ana m)))"
proof -
  obtain n where "⟨M; n⟩ ⊢n Fun c []"
    using c(2) deduct_num_if_deduct by atomize_elim auto
  hence "Fun c [] ∈ M ∨
         (∃m ∈ subtermsset M.
            (∃l < n. ⟨M; l⟩ ⊢n m) ∧
            (∀k ∈ set (fst (Ana m)). ∃l < n. ⟨M; l⟩ ⊢n k) ∧ Fun c [] ∈ set (snd (Ana m)))"
    using deduct_inv[of M n "Fun c []"] c(1) by fast
  thus ?thesis using deduct_if_deduct_num[of M] by blast
qed

lemma private_fun_deduct_in_ik'':
  assumes t: "M ⊢ Fun f T" "Fun c [] ∈ set T" "∀m ∈ subtermsset M. Fun f T ∉ set (snd (Ana m))"
    and c: "¬public c" "Fun c [] ∉ M" "∀m ∈ subtermsset M. Fun c [] ∉ set (snd (Ana m))"
  shows "Fun f T ∈ M"
proof -
  have *: "∄n. ⟨M; n⟩ ⊢n Fun c []"
    using private_const_deduct[OF c(1)] c(2,3) deduct_if_deduct_num
    by blast

  obtain n where n: "⟨M; n⟩ ⊢n Fun f T"
    using t(1) deduct_num_if_deduct
    by blast

  show ?thesis
    using deduct_inv[OF n] t(2,3) *
    by blast
qed

end

subsection ‹Executable Definitions for Code Generation›
fun intruder_synth' where
  "intruder_synth' pu ar M (Var x) = (Var x ∈ M)"
| "intruder_synth' pu ar M (Fun f T) = (
    Fun f T ∈ M ∨ (pu f ∧ length T = ar f ∧ list_all (intruder_synth' pu ar M) T))"

definition "wftrm' ar t ≡ (∀s ∈ subterms t. is_Fun s ⟶ ar (the_Fun s) = length (args s))"

definition "wftrms' ar M ≡ (∀t ∈ M. wftrm' ar t)"

definition "analyzed_in' An pu ar t M ≡ (case An t of
    (K,T) ⇒ (∀k ∈ set K. intruder_synth' pu ar M k) ⟶ (∀s ∈ set T. intruder_synth' pu ar M s))"

lemma (in intruder_model) intruder_synth'_induct[consumes 1, case_names Var Fun]:
  assumes "intruder_synth' public arity M t"
          "⋀x. intruder_synth' public arity M (Var x) ⟹ P (Var x)"
          "⋀f T. (⋀z. z ∈ set T ⟹ intruder_synth' public arity M z ⟹ P z) ⟹
                  intruder_synth' public arity M (Fun f T) ⟹ P (Fun f T) "
  shows "P t"
using assms by (induct public arity M t rule: intruder_synth'.induct) auto

lemma (in intruder_model) wftrm_code[code_unfold]:
  "wftrm t = wftrm' arity t"
unfolding wftrm_def wftrm'_def
by auto

lemma (in intruder_model) wftrms_code[code_unfold]:
  "wftrms M = wftrms' arity M"
using wftrm_code
unfolding wftrms'_def
by auto

lemma (in intruder_model) intruder_synth_code[code_unfold]:
  "intruder_synth M t = intruder_synth' public arity M t"
  (is "?A ⟷ ?B")
proof
  show "?A ⟹ ?B"
  proof (induction t rule: intruder_synth_induct)
    case (AxiomC t) thus ?case by (cases t) auto
  qed (fastforce simp add: list_all_iff)

  show "?B ⟹ ?A"
  proof (induction t rule: intruder_synth'_induct)
    case (Fun f T) thus ?case
    proof (cases "Fun f T ∈ M")
      case False
      hence "public f" "length T = arity f" "list_all (intruder_synth' public arity M) T"
        using Fun.hyps by fastforce+
      thus ?thesis
        using Fun.IH intruder_synth.ComposeC[of T f M] Ball_set[of T]
        by blast
    qed simp
  qed simp
qed

lemma (in intruder_model) analyzed_in_code[code_unfold]:
  "analyzed_in t M = analyzed_in' Ana public arity t M"
using intruder_synth_code[of M]
unfolding analyzed_in_def analyzed_in'_def
by fastforce

end