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 "Σpubn  {f. public f}  Σ⇧n"
abbreviation Σnpriv ("Σpriv_") where "Σprivn  {f. ¬public f}  Σ⇧n"
abbreviation Σpub where "Σpub  (n. Σpubn)"
abbreviation Σpriv where "Σpriv  (n. Σprivn)"
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: "(Σpubn) = {f::'fun. arity f = n  public f}" by auto
lemma Σnpriv_unfold: "(Σprivn) = {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