# Theory Intruder_Deduction

```(*  Title:      Intruder_Deduction.thy
Author:     Andreas Viktor Hess, DTU
*)

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) ⟹ fv⇩s⇩e⇩t (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 ⋅⇩l⇩i⇩s⇩t δ,R ⋅⇩l⇩i⇩s⇩t δ)"
begin

lemma Ana_subterm: assumes "Ana t = (K,T)" shows "set T ⊂ subterms t"
using assms
by (cases t)
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 "fv⇩s⇩e⇩t (set K) ⊆ fv t" "fv⇩s⇩e⇩t (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 ("Σ⇩p⇩u⇩b⇧_") where "Σ⇩p⇩u⇩b⇧n ≡ {f. public f} ∩ Σ⇧n"
abbreviation Σnpriv ("Σ⇩p⇩r⇩i⇩v⇧_") where "Σ⇩p⇩r⇩i⇩v⇧n ≡ {f. ¬public f} ∩ Σ⇧n"
abbreviation Σ⇩p⇩u⇩b where "Σ⇩p⇩u⇩b ≡ (⋃n. Σ⇩p⇩u⇩b⇧n)"
abbreviation Σ⇩p⇩r⇩i⇩v where "Σ⇩p⇩r⇩i⇩v ≡ (⋃n. Σ⇩p⇩r⇩i⇩v⇧n)"
abbreviation Σ where "Σ ≡ (⋃n. Σ⇧n)"
abbreviation 𝒞 where "𝒞 ≡ Σ⇧0"
abbreviation 𝒞⇩p⇩u⇩b where "𝒞⇩p⇩u⇩b ≡ {f. public f} ∩ 𝒞"
abbreviation 𝒞⇩p⇩r⇩i⇩v where "𝒞⇩p⇩r⇩i⇩v ≡ {f. ¬public f} ∩ 𝒞"
abbreviation Σ⇩f where "Σ⇩f ≡ Σ - 𝒞"
abbreviation Σ⇩f⇩p⇩u⇩b where "Σ⇩f⇩p⇩u⇩b ≡ Σ⇩f ∩ Σ⇩p⇩u⇩b"
abbreviation Σ⇩f⇩p⇩r⇩i⇩v where "Σ⇩f⇩p⇩r⇩i⇩v ≡ Σ⇩f ∩ Σ⇩p⇩r⇩i⇩v"

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 ∈ 𝒞⇩p⇩u⇩b ⟹ arity c = 0 ∧ public c" by simp
lemma const_priv_arity_eq_zero[dest]: "c ∈ 𝒞⇩p⇩r⇩i⇩v ⟹ 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 ∈ Σ⇩f⇩p⇩u⇩b ⟹ public f" by fastforce
lemma pub_fun_arity_gt_zero[dest]: "f ∈ Σ⇩f⇩p⇩u⇩b ⟹ 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: "𝒞⇩p⇩u⇩b = {f::'fun. arity f = 0 ∧ public f}" by auto
lemma 𝒞priv_unfold: "𝒞⇩p⇩r⇩i⇩v = {f::'fun. arity f = 0 ∧ ¬public f}" by auto
lemma Σnpub_unfold: "(Σ⇩p⇩u⇩b⇧n) = {f::'fun. arity f = n ∧ public f}" by auto
lemma Σnpriv_unfold: "(Σ⇩p⇩r⇩i⇩v⇧n) = {f::'fun. arity f = n ∧ ¬public f}" by auto
lemma Σfpub_unfold: "Σ⇩f⇩p⇩u⇩b = {f::'fun. arity f > 0 ∧ public f}" by auto
lemma Σfpriv_unfold: "Σ⇩f⇩p⇩r⇩i⇩v = {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 "wf⇩t⇩r⇩m t ≡ ∀f T. Fun f T ⊑ t ⟶ length T = arity f"

abbreviation "wf⇩t⇩r⇩m⇩s T ≡ ∀t ∈ T. wf⇩t⇩r⇩m t"

lemma Ana_keys_wf': "Ana t = (K,T) ⟹ wf⇩t⇩r⇩m t ⟹ k ∈ set K ⟹ wf⇩t⇩r⇩m k"
using Ana_keys_wf unfolding wf⇩t⇩r⇩m_def by metis

lemma wf_trm_Var[simp]: "wf⇩t⇩r⇩m (Var x)" unfolding wf⇩t⇩r⇩m_def by simp

lemma wf_trm_subst_range_Var[simp]: "wf⇩t⇩r⇩m⇩s (subst_range Var)" by simp

lemma wf_trm_subst_range_iff: "(∀x. wf⇩t⇩r⇩m (θ x)) ⟷ wf⇩t⇩r⇩m⇩s (subst_range θ)"
by force

lemma wf_trm_subst_rangeD: "wf⇩t⇩r⇩m⇩s (subst_range θ) ⟹ wf⇩t⇩r⇩m (θ x)"
by (metis wf_trm_subst_range_iff)

lemma wf_trm_subst_rangeI[intro]:
"(⋀x. wf⇩t⇩r⇩m (δ x)) ⟹ wf⇩t⇩r⇩m⇩s (subst_range δ)"
by (metis wf_trm_subst_range_iff)

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

lemma wf_trm_subterm: "⟦wf⇩t⇩r⇩m t; s ⊏ t⟧ ⟹ wf⇩t⇩r⇩m s"
unfolding wf⇩t⇩r⇩m_def by (induct t) auto

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

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

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

lemma wf_trm_subst:
assumes "wf⇩t⇩r⇩m⇩s (subst_range δ)"
shows "wf⇩t⇩r⇩m t = wf⇩t⇩r⇩m (t ⋅ δ)"
proof
show "wf⇩t⇩r⇩m t ⟹ wf⇩t⇩r⇩m (t ⋅ δ)"
proof (induction t)
case (Fun f T)
hence "⋀t. t ∈ set T ⟹ wf⇩t⇩r⇩m t"
by (meson wf⇩t⇩r⇩m_def Fun_param_is_subterm term.order_trans)
hence "⋀t. t ∈ set T ⟹ wf⇩t⇩r⇩m (t ⋅ δ)" using Fun.IH by auto
moreover have "length (map (λt. t ⋅ δ) T) = arity f"
using Fun.prems unfolding wf⇩t⇩r⇩m_def by auto
ultimately show ?case by fastforce

show "wf⇩t⇩r⇩m (t ⋅ δ) ⟹ wf⇩t⇩r⇩m t"
proof (induction t)
case (Fun f T)
hence "wf⇩t⇩r⇩m t" when "t ∈ set (map (λs. s ⋅ δ) T)" for t
by (metis that wf⇩t⇩r⇩m_def Fun_param_is_subterm term.order_trans subst_apply_term.simps(2))
hence "wf⇩t⇩r⇩m 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 wf⇩t⇩r⇩m_def by auto
ultimately show ?case by fastforce
qed

lemma wf_trm_subst_singleton:
assumes "wf⇩t⇩r⇩m t" "wf⇩t⇩r⇩m t'" shows "wf⇩t⇩r⇩m (t ⋅ Var(v := t'))"
proof -
have "wf⇩t⇩r⇩m ((Var(v := t')) w)" for w using assms(2) unfolding wf⇩t⇩r⇩m_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 "wf⇩t⇩r⇩m (t ⋅ δ)"
shows "wf⇩t⇩r⇩m (t ⋅ rm_vars X δ)"
using assms
proof (induction t)
case (Fun f T)
have "wf⇩t⇩r⇩m (t ⋅ δ)" when "t ∈ set T" for t
using that wf_trm_param[of f "map (λt. t ⋅ δ) T"] Fun.prems
by auto
hence "wf⇩t⇩r⇩m (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 wf⇩t⇩r⇩m_def by auto
ultimately show ?case unfolding wf⇩t⇩r⇩m_def by auto
qed simp

lemma wf_trm_subst_rm_vars': "wf⇩t⇩r⇩m (δ v) ⟹ wf⇩t⇩r⇩m (rm_vars X δ v)"
by auto

lemma wf_trms_subst:
assumes "wf⇩t⇩r⇩m⇩s (subst_range δ)" "wf⇩t⇩r⇩m⇩s M"
shows "wf⇩t⇩r⇩m⇩s (M ⋅⇩s⇩e⇩t δ)"
by (metis (no_types, lifting) assms imageE wf_trm_subst)

lemma wf_trms_subst_rm_vars:
assumes "wf⇩t⇩r⇩m⇩s (M ⋅⇩s⇩e⇩t δ)"
shows "wf⇩t⇩r⇩m⇩s (M ⋅⇩s⇩e⇩t rm_vars X δ)"
using assms wf_trm_subst_rm_vars by blast

lemma wf_trms_subst_rm_vars':
assumes "wf⇩t⇩r⇩m⇩s (subst_range δ)"
shows "wf⇩t⇩r⇩m⇩s (subst_range (rm_vars X δ))"
using assms by force

lemma wf_trms_subst_compose:
assumes "wf⇩t⇩r⇩m⇩s (subst_range θ)" "wf⇩t⇩r⇩m⇩s (subst_range δ)"
shows "wf⇩t⇩r⇩m⇩s (subst_range (θ ∘⇩s δ))"
using assms subst_img_comp_subset' wf_trm_subst by blast

lemma wf_trm_subst_compose:
fixes δ::"('fun, 'v) subst"
assumes "wf⇩t⇩r⇩m (θ x)" "⋀x. wf⇩t⇩r⇩m (δ x)"
shows "wf⇩t⇩r⇩m ((θ ∘⇩s δ) x)"
using wf_trm_subst[of δ "θ x", OF wf_trm_subst_rangeI[OF assms(2)]] assms(1)
subst_subst_compose[of "Var x" θ δ]
subst_apply_term.simps(1)[of x θ]
subst_apply_term.simps(1)[of x "θ ∘⇩s δ"]
by argo

lemma wf_trms_Var_range:
assumes "subst_range δ ⊆ range Var"
shows "wf⇩t⇩r⇩m⇩s (subst_range δ)"
using assms by fastforce

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

lemma wf_trm_subst_inv: "wf⇩t⇩r⇩m (t ⋅ δ) ⟹ wf⇩t⇩r⇩m t"
unfolding wf⇩t⇩r⇩m_def by (induct t) auto

lemma wf_trms_subst_inv: "wf⇩t⇩r⇩m⇩s (M ⋅⇩s⇩e⇩t δ) ⟹ wf⇩t⇩r⇩m⇩s M"
using wf_trm_subst_inv by fast

lemma wf_trm_subterms: "wf⇩t⇩r⇩m t ⟹ wf⇩t⇩r⇩m⇩s (subterms t)"
using wf_trm_subterm by blast

lemma wf_trms_subterms: "wf⇩t⇩r⇩m⇩s M ⟹ wf⇩t⇩r⇩m⇩s (subterms⇩s⇩e⇩t M)"
using wf_trm_subterms by blast

lemma wf_trm_arity: "wf⇩t⇩r⇩m (Fun f T) ⟹ length T = arity f"
unfolding wf⇩t⇩r⇩m_def by blast

lemma wf_trm_subterm_arity: "wf⇩t⇩r⇩m t ⟹ Fun f T ⊑ t ⟹ length T = arity f"
unfolding wf⇩t⇩r⇩m_def by blast

lemma unify_list_wf_trm:
assumes "Unification.unify E B = Some U" "∀(s,t) ∈ set E. wf⇩t⇩r⇩m s ∧ wf⇩t⇩r⇩m t"
and "∀(v,t) ∈ set B. wf⇩t⇩r⇩m t"
shows "∀(v,t) ∈ set U. wf⇩t⇩r⇩m 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: "wf⇩t⇩r⇩m (Fun f T)" "wf⇩t⇩r⇩m (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 "wf⇩t⇩r⇩m t" "wf⇩t⇩r⇩m 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). wf⇩t⇩r⇩m x"
and **: "∀(s,t) ∈ set E. wf⇩t⇩r⇩m s ∧ wf⇩t⇩r⇩m t" "wf⇩t⇩r⇩m 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). wf⇩t⇩r⇩m s ∧ wf⇩t⇩r⇩m t"
using wf_trm_subst_singleton[OF _ ‹wf⇩t⇩r⇩m 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). wf⇩t⇩r⇩m x"
and **: "∀(s,t) ∈ set E. wf⇩t⇩r⇩m s ∧ wf⇩t⇩r⇩m t" "wf⇩t⇩r⇩m (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). wf⇩t⇩r⇩m s ∧ wf⇩t⇩r⇩m t"
using wf_trm_subst_singleton[OF _ ‹wf⇩t⇩r⇩m (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 σ" "wf⇩t⇩r⇩m s" "wf⇩t⇩r⇩m t"
shows "wf⇩t⇩r⇩m (σ v)"
proof -
from assms obtain σ' where "subst_of σ' = σ" "∀(v,t) ∈ set σ'. wf⇩t⇩r⇩m 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 "wf⇩t⇩r⇩m (θ 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 "wf⇩t⇩r⇩m t" using snoc.prems(2) x by auto
ultimately show ?case using wf_trm_subst[of _ t] unfolding subst_compose_def by auto
qed

lemma mgu_wf_trms:
assumes "mgu s t = Some σ" "wf⇩t⇩r⇩m s" "wf⇩t⇩r⇩m t"
shows "wf⇩t⇩r⇩m⇩s (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;
t⇩i ∈ set T⟧
⟹ intruder_deduct M t⇩i"

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)"

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 t⇩i. ⟦M ⊢ t; P M t; Ana t = (K, T); ⋀k. k ∈ set K ⟹ M ⊢ k;
⋀k. k ∈ set K ⟹ P M k; t⇩i ∈ set T⟧ ⟹ P M t⇩i"
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 ∈ 𝒞⇩p⇩u⇩b"
shows "M ⊢ Fun c []" "M ⊢⇩c Fun c []"
proof -
have "arity c = 0" "public c" using const_arity_eq_zero ‹c ∈ 𝒞⇩p⇩u⇩b› 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 ∈ subterms⇩s⇩e⇩t 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 ∈ subterms⇩s⇩e⇩t 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 ⟹ wf⇩t⇩r⇩m 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 t⇩i)
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 t⇩i) 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 t⇩i) 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 ⋅⇩s⇩e⇩t δ ⊢ 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 ⋅⇩s⇩e⇩t δ ⊢ 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 ⋅⇩l⇩i⇩s⇩t δ, M' ⋅⇩l⇩i⇩s⇩t δ)"
"⋀k. k ∈ set (K ⋅⇩l⇩i⇩s⇩t δ) ⟹ M ⋅⇩s⇩e⇩t δ ⊢ k"
"m' ⋅ δ ∈ set (M' ⋅⇩l⇩i⇩s⇩t δ)"
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 ⋅⇩s⇩e⇩t δ ⊢⇩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 ⋅⇩s⇩e⇩t δ ⊢⇩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 ⊆ fv⇩s⇩e⇩t M"
using assms
proof (induction t rule: intruder_deduct_induct)
case (Decompose t K T t⇩i) 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 ⊆ fv⇩s⇩e⇩t 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 t⇩i)
thus ?case using intruder_deduct.Decompose[OF _ ‹Ana t = (K,T)› _ ‹t⇩i ∈ set T›] by simp

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 t⇩i)
hence "M' ⊢ t⇩i" using Decompose.hyps intruder_deduct.Decompose by blast
moreover have "t⇩i ⊑ 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 t⇩i" 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 t⇩i)
{ 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; t⇩i ∈ set T⟧
⟹ ⟨M; Q⟩ ⊢⇩r t⇩i"

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; t⇩i ∈ set T⟧
⟹ ⟨M; Suc (Max (insert n (steps ` set K)))⟩ ⊢⇩n t⇩i"

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 t⇩i. ⟦⟨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; t⇩i ∈ set T⟧ ⟹ P M Q t⇩i"
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 t⇩i steps n.
⟦⟨M; n⟩ ⊢⇩n t; P M n t; Ana t = (K, T);
⋀k. k ∈ set K ⟹ ⟨M; steps k⟩ ⊢⇩n k;
t⇩i ∈ set T; ⋀k. k ∈ set K ⟹ P M (steps k) k⟧
⟹ P M (Suc (Max (insert n (steps ` set K)))) t⇩i"
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 t⇩i)
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 t⇩i) 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 t⇩i)
obtain f S where "t = Fun f S" using Ana_var ‹t⇩i ∈ set T› ‹Ana t = (K, T)› by (cases t) auto
thus ?case using DecomposeR assms(2) P Ana_subterm by blast

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 moura
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 t⇩i)
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 moura
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' t⇩i steps n)
hence *: "Fun f T ⊑ t"
using term.order_trans[of "Fun f T" t⇩i 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 ∈ subterms⇩s⇩e⇩t 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 t⇩i 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: "t⇩i ∈ set (snd (Ana t))"
using DecomposeN.hyps(2,4)
by fastforce

have 3: "t ∈ subterms⇩s⇩e⇩t M" when "t ∈ set (snd (Ana m))" "m ⊑⇩s⇩e⇩t 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 t⇩i (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 t⇩i (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 moura
then obtain l where l: "l < n" "⟨M; l⟩ ⊢⇩n t⇩i"
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 ⊑⇩s⇩e⇩t 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 ⊑⇩s⇩e⇩t 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 t⇩i 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) moura+
hence *: "Fun g S ⊑ t" "¬P (Fun g S)" using False by force+
have "∃j<l. ⟨M; j⟩ ⊢⇩n t⇩i"
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 t⇩i"
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 ∈ subterms⇩s⇩e⇩t 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 moura
hence "Fun c [] ∈ M ∨
(∃m ∈ subterms⇩s⇩e⇩t 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 ∈ subterms⇩s⇩e⇩t M. Fun f T ∉ set (snd (Ana m))"
and c: "¬public c" "Fun c [] ∉ M" "∀m ∈ subterms⇩s⇩e⇩t 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 "wf⇩t⇩r⇩m' ar t ≡ (∀s ∈ subterms t. is_Fun s ⟶ ar (the_Fun s) = length (args s))"

definition "wf⇩t⇩r⇩m⇩s' ar M ≡ (∀t ∈ M. wf⇩t⇩r⇩m' 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) wf⇩t⇩r⇩m_code[code_unfold]:
"wf⇩t⇩r⇩m t = wf⇩t⇩r⇩m' arity t"
unfolding wf⇩t⇩r⇩m_def wf⇩t⇩r⇩m'_def
by auto

lemma (in intruder_model) wf⇩t⇩r⇩m⇩s_code[code_unfold]:
"wf⇩t⇩r⇩m⇩s M = wf⇩t⇩r⇩m⇩s' arity M"
using wf⇩t⇩r⇩m_code
unfolding wf⇩t⇩r⇩m⇩s'_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

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
```