(* 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) ⟹ 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) (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 "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 qed (simp add: wf_trm_subst_rangeD[OF assms]) 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 (simp add: assms) 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 (simp add: wf⇩_{t}⇩_{r}⇩_{m}_def) 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)" 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 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 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 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 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 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 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