1201 lines
64 KiB
Plaintext
1201 lines
64 KiB
Plaintext
(*
|
|
(C) Copyright Andreas Viktor Hess, DTU, 2015-2020
|
|
|
|
All Rights Reserved.
|
|
|
|
Redistribution and use in source and binary forms, with or without
|
|
modification, are permitted provided that the following conditions are
|
|
met:
|
|
|
|
- Redistributions of source code must retain the above copyright
|
|
notice, this list of conditions and the following disclaimer.
|
|
|
|
- Redistributions in binary form must reproduce the above copyright
|
|
notice, this list of conditions and the following disclaimer in the
|
|
documentation and/or other materials provided with the distribution.
|
|
|
|
- Neither the name of the copyright holder nor the names of its
|
|
contributors may be used to endorse or promote products
|
|
derived from this software without specific prior written
|
|
permission.
|
|
|
|
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
|
|
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
|
|
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
|
|
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
|
|
OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
|
|
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
|
|
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
|
|
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
|
|
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
|
|
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
|
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
|
*)
|
|
|
|
(* Title: Intruder_Deduction.thy
|
|
Author: Andreas Viktor Hess, DTU
|
|
*)
|
|
|
|
section \<open>Dolev-Yao Intruder Model\<close>
|
|
theory Intruder_Deduction
|
|
imports Messages More_Unification
|
|
begin
|
|
|
|
subsection \<open>Syntax for the Intruder Deduction Relations\<close>
|
|
consts INTRUDER_SYNTH::"('f,'v) terms \<Rightarrow> ('f,'v) term \<Rightarrow> bool" (infix "\<turnstile>\<^sub>c" 50)
|
|
consts INTRUDER_DEDUCT::"('f,'v) terms \<Rightarrow> ('f,'v) term \<Rightarrow> bool" (infix "\<turnstile>" 50)
|
|
|
|
|
|
subsection \<open>Intruder Model Locale\<close>
|
|
text \<open>
|
|
The intruder model is parameterized over arbitrary function symbols (e.g, cryptographic operators)
|
|
and variables. It requires three functions:
|
|
- \<open>arity\<close> that assigns an arity to each function symbol.
|
|
- \<open>public\<close> that partitions the function symbols into those that will be available to the intruder
|
|
and those that will not.
|
|
- \<open>Ana\<close>, the analysis interface, that defines how messages can be decomposed (e.g., decryption).
|
|
\<close>
|
|
locale intruder_model =
|
|
fixes arity :: "'fun \<Rightarrow> nat"
|
|
and public :: "'fun \<Rightarrow> bool"
|
|
and Ana :: "('fun,'var) term \<Rightarrow> (('fun,'var) term list \<times> ('fun,'var) term list)"
|
|
assumes Ana_keys_fv: "\<And>t K R. Ana t = (K,R) \<Longrightarrow> fv\<^sub>s\<^sub>e\<^sub>t (set K) \<subseteq> fv t"
|
|
and Ana_keys_wf: "\<And>t k K R f T.
|
|
Ana t = (K,R) \<Longrightarrow> (\<And>g S. Fun g S \<sqsubseteq> t \<Longrightarrow> length S = arity g)
|
|
\<Longrightarrow> k \<in> set K \<Longrightarrow> Fun f T \<sqsubseteq> k \<Longrightarrow> length T = arity f"
|
|
and Ana_var[simp]: "\<And>x. Ana (Var x) = ([],[])"
|
|
and Ana_fun_subterm: "\<And>f T K R. Ana (Fun f T) = (K,R) \<Longrightarrow> set R \<subseteq> set T"
|
|
and Ana_subst: "\<And>t \<delta> K R. \<lbrakk>Ana t = (K,R); K \<noteq> [] \<or> R \<noteq> []\<rbrakk> \<Longrightarrow> Ana (t \<cdot> \<delta>) = (K \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>,R \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>)"
|
|
begin
|
|
|
|
lemma Ana_subterm: assumes "Ana t = (K,T)" shows "set T \<subset> 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 \<in> set (snd (Ana t)) \<Longrightarrow> s \<sqsubseteq> t"
|
|
using Ana_subterm by (cases "Ana t") auto
|
|
|
|
lemma Ana_vars: assumes "Ana t = (K,M)" shows "fv\<^sub>s\<^sub>e\<^sub>t (set K) \<subseteq> fv t" "fv\<^sub>s\<^sub>e\<^sub>t (set M) \<subseteq> fv t"
|
|
by (rule Ana_keys_fv[OF assms]) (use Ana_subterm[OF assms] subtermeq_vars_subset in auto)
|
|
|
|
abbreviation \<V> where "\<V> \<equiv> UNIV::'var set"
|
|
abbreviation \<Sigma>n ("\<Sigma>\<^sup>_") where "\<Sigma>\<^sup>n \<equiv> {f::'fun. arity f = n}"
|
|
abbreviation \<Sigma>npub ("\<Sigma>\<^sub>p\<^sub>u\<^sub>b\<^sup>_") where "\<Sigma>\<^sub>p\<^sub>u\<^sub>b\<^sup>n \<equiv> {f. public f} \<inter> \<Sigma>\<^sup>n"
|
|
abbreviation \<Sigma>npriv ("\<Sigma>\<^sub>p\<^sub>r\<^sub>i\<^sub>v\<^sup>_") where "\<Sigma>\<^sub>p\<^sub>r\<^sub>i\<^sub>v\<^sup>n \<equiv> {f. \<not>public f} \<inter> \<Sigma>\<^sup>n"
|
|
abbreviation \<Sigma>\<^sub>p\<^sub>u\<^sub>b where "\<Sigma>\<^sub>p\<^sub>u\<^sub>b \<equiv> (\<Union>n. \<Sigma>\<^sub>p\<^sub>u\<^sub>b\<^sup>n)"
|
|
abbreviation \<Sigma>\<^sub>p\<^sub>r\<^sub>i\<^sub>v where "\<Sigma>\<^sub>p\<^sub>r\<^sub>i\<^sub>v \<equiv> (\<Union>n. \<Sigma>\<^sub>p\<^sub>r\<^sub>i\<^sub>v\<^sup>n)"
|
|
abbreviation \<Sigma> where "\<Sigma> \<equiv> (\<Union>n. \<Sigma>\<^sup>n)"
|
|
abbreviation \<C> where "\<C> \<equiv> \<Sigma>\<^sup>0"
|
|
abbreviation \<C>\<^sub>p\<^sub>u\<^sub>b where "\<C>\<^sub>p\<^sub>u\<^sub>b \<equiv> {f. public f} \<inter> \<C>"
|
|
abbreviation \<C>\<^sub>p\<^sub>r\<^sub>i\<^sub>v where "\<C>\<^sub>p\<^sub>r\<^sub>i\<^sub>v \<equiv> {f. \<not>public f} \<inter> \<C>"
|
|
abbreviation \<Sigma>\<^sub>f where "\<Sigma>\<^sub>f \<equiv> \<Sigma> - \<C>"
|
|
abbreviation \<Sigma>\<^sub>f\<^sub>p\<^sub>u\<^sub>b where "\<Sigma>\<^sub>f\<^sub>p\<^sub>u\<^sub>b \<equiv> \<Sigma>\<^sub>f \<inter> \<Sigma>\<^sub>p\<^sub>u\<^sub>b"
|
|
abbreviation \<Sigma>\<^sub>f\<^sub>p\<^sub>r\<^sub>i\<^sub>v where "\<Sigma>\<^sub>f\<^sub>p\<^sub>r\<^sub>i\<^sub>v \<equiv> \<Sigma>\<^sub>f \<inter> \<Sigma>\<^sub>p\<^sub>r\<^sub>i\<^sub>v"
|
|
|
|
lemma disjoint_fun_syms: "\<Sigma>\<^sub>f \<inter> \<C> = {}" by auto
|
|
lemma id_union_univ: "\<Sigma>\<^sub>f \<union> \<C> = UNIV" "\<Sigma> = UNIV" by auto
|
|
lemma const_arity_eq_zero[dest]: "c \<in> \<C> \<Longrightarrow> arity c = 0" by simp
|
|
lemma const_pub_arity_eq_zero[dest]: "c \<in> \<C>\<^sub>p\<^sub>u\<^sub>b \<Longrightarrow> arity c = 0 \<and> public c" by simp
|
|
lemma const_priv_arity_eq_zero[dest]: "c \<in> \<C>\<^sub>p\<^sub>r\<^sub>i\<^sub>v \<Longrightarrow> arity c = 0 \<and> \<not>public c" by simp
|
|
lemma fun_arity_gt_zero[dest]: "f \<in> \<Sigma>\<^sub>f \<Longrightarrow> arity f > 0" by fastforce
|
|
lemma pub_fun_public[dest]: "f \<in> \<Sigma>\<^sub>f\<^sub>p\<^sub>u\<^sub>b \<Longrightarrow> public f" by fastforce
|
|
lemma pub_fun_arity_gt_zero[dest]: "f \<in> \<Sigma>\<^sub>f\<^sub>p\<^sub>u\<^sub>b \<Longrightarrow> arity f > 0" by fastforce
|
|
|
|
lemma \<Sigma>\<^sub>f_unfold: "\<Sigma>\<^sub>f = {f::'fun. arity f > 0}" by auto
|
|
lemma \<C>_unfold: "\<C> = {f::'fun. arity f = 0}" by auto
|
|
lemma \<C>pub_unfold: "\<C>\<^sub>p\<^sub>u\<^sub>b = {f::'fun. arity f = 0 \<and> public f}" by auto
|
|
lemma \<C>priv_unfold: "\<C>\<^sub>p\<^sub>r\<^sub>i\<^sub>v = {f::'fun. arity f = 0 \<and> \<not>public f}" by auto
|
|
lemma \<Sigma>npub_unfold: "(\<Sigma>\<^sub>p\<^sub>u\<^sub>b\<^sup>n) = {f::'fun. arity f = n \<and> public f}" by auto
|
|
lemma \<Sigma>npriv_unfold: "(\<Sigma>\<^sub>p\<^sub>r\<^sub>i\<^sub>v\<^sup>n) = {f::'fun. arity f = n \<and> \<not>public f}" by auto
|
|
lemma \<Sigma>fpub_unfold: "\<Sigma>\<^sub>f\<^sub>p\<^sub>u\<^sub>b = {f::'fun. arity f > 0 \<and> public f}" by auto
|
|
lemma \<Sigma>fpriv_unfold: "\<Sigma>\<^sub>f\<^sub>p\<^sub>r\<^sub>i\<^sub>v = {f::'fun. arity f > 0 \<and> \<not>public f}" by auto
|
|
lemma \<Sigma>n_m_eq: "\<lbrakk>(\<Sigma>\<^sup>n) \<noteq> {}; (\<Sigma>\<^sup>n) = (\<Sigma>\<^sup>m)\<rbrakk> \<Longrightarrow> n = m" by auto
|
|
|
|
|
|
subsection \<open>Term Well-formedness\<close>
|
|
definition "wf\<^sub>t\<^sub>r\<^sub>m t \<equiv> \<forall>f T. Fun f T \<sqsubseteq> t \<longrightarrow> length T = arity f"
|
|
|
|
abbreviation "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s T \<equiv> \<forall>t \<in> T. wf\<^sub>t\<^sub>r\<^sub>m t"
|
|
|
|
lemma Ana_keys_wf': "Ana t = (K,T) \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m t \<Longrightarrow> k \<in> set K \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m k"
|
|
using Ana_keys_wf unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by metis
|
|
|
|
lemma wf_trm_Var[simp]: "wf\<^sub>t\<^sub>r\<^sub>m (Var x)" unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by simp
|
|
|
|
lemma wf_trm_subst_range_Var[simp]: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range Var)" by simp
|
|
|
|
lemma wf_trm_subst_range_iff: "(\<forall>x. wf\<^sub>t\<^sub>r\<^sub>m (\<theta> x)) \<longleftrightarrow> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>)"
|
|
by force
|
|
|
|
lemma wf_trm_subst_rangeD: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>) \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m (\<theta> x)"
|
|
by (metis wf_trm_subst_range_iff)
|
|
|
|
lemma wf_trm_subst_rangeI[intro]:
|
|
"(\<And>x. wf\<^sub>t\<^sub>r\<^sub>m (\<delta> x)) \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)"
|
|
by (metis wf_trm_subst_range_iff)
|
|
|
|
lemma wf_trmI[intro]:
|
|
assumes "\<And>t. t \<in> set T \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m t" "length T = arity f"
|
|
shows "wf\<^sub>t\<^sub>r\<^sub>m (Fun f T)"
|
|
using assms unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto
|
|
|
|
lemma wf_trm_subterm: "\<lbrakk>wf\<^sub>t\<^sub>r\<^sub>m t; s \<sqsubset> t\<rbrakk> \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m s"
|
|
unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by (induct t) auto
|
|
|
|
lemma wf_trm_subtermeq:
|
|
assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "s \<sqsubseteq> t"
|
|
shows "wf\<^sub>t\<^sub>r\<^sub>m s"
|
|
proof (cases "s = t")
|
|
case False thus "wf\<^sub>t\<^sub>r\<^sub>m s" using assms(2) wf_trm_subterm[OF assms(1)] by simp
|
|
qed (metis assms(1))
|
|
|
|
lemma wf_trm_param:
|
|
assumes "wf\<^sub>t\<^sub>r\<^sub>m (Fun f T)" "t \<in> set T"
|
|
shows "wf\<^sub>t\<^sub>r\<^sub>m t"
|
|
by (meson assms subtermeqI'' wf_trm_subtermeq)
|
|
|
|
lemma wf_trm_param_idx:
|
|
assumes "wf\<^sub>t\<^sub>r\<^sub>m (Fun f T)"
|
|
and "i < length T"
|
|
shows "wf\<^sub>t\<^sub>r\<^sub>m (T ! i)"
|
|
using wf_trm_param[OF assms(1), of "T ! i"] assms(2)
|
|
by fastforce
|
|
|
|
lemma wf_trm_subst:
|
|
assumes "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)"
|
|
shows "wf\<^sub>t\<^sub>r\<^sub>m t = wf\<^sub>t\<^sub>r\<^sub>m (t \<cdot> \<delta>)"
|
|
proof
|
|
show "wf\<^sub>t\<^sub>r\<^sub>m t \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m (t \<cdot> \<delta>)"
|
|
proof (induction t)
|
|
case (Fun f T)
|
|
hence "\<And>t. t \<in> set T \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m t"
|
|
by (meson wf\<^sub>t\<^sub>r\<^sub>m_def Fun_param_is_subterm term.order_trans)
|
|
hence "\<And>t. t \<in> set T \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m (t \<cdot> \<delta>)" using Fun.IH by auto
|
|
moreover have "length (map (\<lambda>t. t \<cdot> \<delta>) T) = arity f"
|
|
using Fun.prems unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto
|
|
ultimately show ?case by fastforce
|
|
qed (simp add: wf_trm_subst_rangeD[OF assms])
|
|
|
|
show "wf\<^sub>t\<^sub>r\<^sub>m (t \<cdot> \<delta>) \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m t"
|
|
proof (induction t)
|
|
case (Fun f T)
|
|
hence "wf\<^sub>t\<^sub>r\<^sub>m t" when "t \<in> set (map (\<lambda>s. s \<cdot> \<delta>) T)" for t
|
|
by (metis that wf\<^sub>t\<^sub>r\<^sub>m_def Fun_param_is_subterm term.order_trans subst_apply_term.simps(2))
|
|
hence "wf\<^sub>t\<^sub>r\<^sub>m t" when "t \<in> set T" for t using that Fun.IH by auto
|
|
moreover have "length (map (\<lambda>t. t \<cdot> \<delta>) T) = arity f"
|
|
using Fun.prems unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto
|
|
ultimately show ?case by fastforce
|
|
qed (simp add: assms)
|
|
qed
|
|
|
|
lemma wf_trm_subst_singleton:
|
|
assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "wf\<^sub>t\<^sub>r\<^sub>m t'" shows "wf\<^sub>t\<^sub>r\<^sub>m (t \<cdot> Var(v := t'))"
|
|
proof -
|
|
have "wf\<^sub>t\<^sub>r\<^sub>m ((Var(v := t')) w)" for w using assms(2) unfolding wf\<^sub>t\<^sub>r\<^sub>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\<^sub>t\<^sub>r\<^sub>m (t \<cdot> \<delta>)"
|
|
shows "wf\<^sub>t\<^sub>r\<^sub>m (t \<cdot> rm_vars X \<delta>)"
|
|
using assms
|
|
proof (induction t)
|
|
case (Fun f T)
|
|
have "wf\<^sub>t\<^sub>r\<^sub>m (t \<cdot> \<delta>)" when "t \<in> set T" for t
|
|
using that wf_trm_param[of f "map (\<lambda>t. t \<cdot> \<delta>) T"] Fun.prems
|
|
by auto
|
|
hence "wf\<^sub>t\<^sub>r\<^sub>m (t \<cdot> rm_vars X \<delta>)" when "t \<in> set T" for t using that Fun.IH by simp
|
|
moreover have "length T = arity f" using Fun.prems unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto
|
|
ultimately show ?case unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto
|
|
qed simp
|
|
|
|
lemma wf_trm_subst_rm_vars': "wf\<^sub>t\<^sub>r\<^sub>m (\<delta> v) \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m (rm_vars X \<delta> v)"
|
|
by auto
|
|
|
|
lemma wf_trms_subst:
|
|
assumes "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s M"
|
|
shows "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta>)"
|
|
by (metis (no_types, lifting) assms imageE wf_trm_subst)
|
|
|
|
lemma wf_trms_subst_rm_vars:
|
|
assumes "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta>)"
|
|
shows "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (M \<cdot>\<^sub>s\<^sub>e\<^sub>t rm_vars X \<delta>)"
|
|
using assms wf_trm_subst_rm_vars by blast
|
|
|
|
lemma wf_trms_subst_rm_vars':
|
|
assumes "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)"
|
|
shows "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range (rm_vars X \<delta>))"
|
|
using assms by force
|
|
|
|
lemma wf_trms_subst_compose:
|
|
assumes "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>)" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)"
|
|
shows "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range (\<theta> \<circ>\<^sub>s \<delta>))"
|
|
using assms subst_img_comp_subset' wf_trm_subst by blast
|
|
|
|
lemma wf_trm_subst_compose:
|
|
fixes \<delta>::"('fun, 'v) subst"
|
|
assumes "wf\<^sub>t\<^sub>r\<^sub>m (\<theta> x)" "\<And>x. wf\<^sub>t\<^sub>r\<^sub>m (\<delta> x)"
|
|
shows "wf\<^sub>t\<^sub>r\<^sub>m ((\<theta> \<circ>\<^sub>s \<delta>) x)"
|
|
using wf_trm_subst[of \<delta> "\<theta> x", OF wf_trm_subst_rangeI[OF assms(2)]] assms(1)
|
|
subst_subst_compose[of "Var x" \<theta> \<delta>]
|
|
subst_apply_term.simps(1)[of x \<theta>]
|
|
subst_apply_term.simps(1)[of x "\<theta> \<circ>\<^sub>s \<delta>"]
|
|
by argo
|
|
|
|
lemma wf_trms_Var_range:
|
|
assumes "subst_range \<delta> \<subseteq> range Var"
|
|
shows "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)"
|
|
using assms by fastforce
|
|
|
|
lemma wf_trms_subst_compose_Var_range:
|
|
assumes "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>)"
|
|
and "subst_range \<delta> \<subseteq> range Var"
|
|
shows "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range (\<delta> \<circ>\<^sub>s \<theta>))"
|
|
and "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range (\<theta> \<circ>\<^sub>s \<delta>))"
|
|
using assms wf_trms_subst_compose wf_trms_Var_range by metis+
|
|
|
|
lemma wf_trm_subst_inv: "wf\<^sub>t\<^sub>r\<^sub>m (t \<cdot> \<delta>) \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m t"
|
|
unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by (induct t) auto
|
|
|
|
lemma wf_trms_subst_inv: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta>) \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s M"
|
|
using wf_trm_subst_inv by fast
|
|
|
|
lemma wf_trm_subterms: "wf\<^sub>t\<^sub>r\<^sub>m t \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subterms t)"
|
|
using wf_trm_subterm by blast
|
|
|
|
lemma wf_trms_subterms: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s M \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subterms\<^sub>s\<^sub>e\<^sub>t M)"
|
|
using wf_trm_subterms by blast
|
|
|
|
lemma wf_trm_arity: "wf\<^sub>t\<^sub>r\<^sub>m (Fun f T) \<Longrightarrow> length T = arity f"
|
|
unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by blast
|
|
|
|
lemma wf_trm_subterm_arity: "wf\<^sub>t\<^sub>r\<^sub>m t \<Longrightarrow> Fun f T \<sqsubseteq> t \<Longrightarrow> length T = arity f"
|
|
unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by blast
|
|
|
|
lemma unify_list_wf_trm:
|
|
assumes "Unification.unify E B = Some U" "\<forall>(s,t) \<in> set E. wf\<^sub>t\<^sub>r\<^sub>m s \<and> wf\<^sub>t\<^sub>r\<^sub>m t"
|
|
and "\<forall>(v,t) \<in> set B. wf\<^sub>t\<^sub>r\<^sub>m t"
|
|
shows "\<forall>(v,t) \<in> set U. wf\<^sub>t\<^sub>r\<^sub>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\<^sub>t\<^sub>r\<^sub>m (Fun f T)" "wf\<^sub>t\<^sub>r\<^sub>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 \<sqsubset> Fun f T" "t' \<sqsubset> Fun g S" when "(t,t') \<in> set E'" for t t'
|
|
using that by (metis zip_arg_subterm(1), metis zip_arg_subterm(2))
|
|
hence "wf\<^sub>t\<^sub>r\<^sub>m t" "wf\<^sub>t\<^sub>r\<^sub>m t'" when "(t,t') \<in> set E'" for t t'
|
|
using wf_trm_subterm wf_fun \<open>f = g\<close> 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 *: "\<forall>(w,x) \<in> set ((v, t) # B). wf\<^sub>t\<^sub>r\<^sub>m x"
|
|
and **: "\<forall>(s,t) \<in> set E. wf\<^sub>t\<^sub>r\<^sub>m s \<and> wf\<^sub>t\<^sub>r\<^sub>m t" "wf\<^sub>t\<^sub>r\<^sub>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 \<notin> fv t" using "3.prems"(1) by auto
|
|
hence "Unification.unify (subst_list (subst v t) E) ((v, t)#B) = Some U"
|
|
using \<open>t \<noteq> Var v\<close> "3.prems"(1) by auto
|
|
moreover have "\<forall>(s, t) \<in> set (subst_list (subst v t) E). wf\<^sub>t\<^sub>r\<^sub>m s \<and> wf\<^sub>t\<^sub>r\<^sub>m t"
|
|
using wf_trm_subst_singleton[OF _ \<open>wf\<^sub>t\<^sub>r\<^sub>m t\<close>] "3.prems"(2)
|
|
unfolding subst_list_def subst_def by auto
|
|
ultimately show ?thesis using "3.IH"(2)[OF \<open>t \<noteq> Var v\<close> \<open>v \<notin> fv t\<close> _ _ *] by metis
|
|
qed
|
|
next
|
|
case (4 f T v E B U)
|
|
hence *: "\<forall>(w,x) \<in> set ((v, Fun f T) # B). wf\<^sub>t\<^sub>r\<^sub>m x"
|
|
and **: "\<forall>(s,t) \<in> set E. wf\<^sub>t\<^sub>r\<^sub>m s \<and> wf\<^sub>t\<^sub>r\<^sub>m t" "wf\<^sub>t\<^sub>r\<^sub>m (Fun f T)"
|
|
by auto
|
|
|
|
have "v \<notin> 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 "\<forall>(s, t) \<in> set (subst_list (subst v (Fun f T)) E). wf\<^sub>t\<^sub>r\<^sub>m s \<and> wf\<^sub>t\<^sub>r\<^sub>m t"
|
|
using wf_trm_subst_singleton[OF _ \<open>wf\<^sub>t\<^sub>r\<^sub>m (Fun f T)\<close>] "4.prems"(2)
|
|
unfolding subst_list_def subst_def by auto
|
|
ultimately show ?case using "4.IH"[OF \<open>v \<notin> fv (Fun f T)\<close> _ _ *] by metis
|
|
qed
|
|
|
|
lemma mgu_wf_trm:
|
|
assumes "mgu s t = Some \<sigma>" "wf\<^sub>t\<^sub>r\<^sub>m s" "wf\<^sub>t\<^sub>r\<^sub>m t"
|
|
shows "wf\<^sub>t\<^sub>r\<^sub>m (\<sigma> v)"
|
|
proof -
|
|
from assms obtain \<sigma>' where "subst_of \<sigma>' = \<sigma>" "\<forall>(v,t) \<in> set \<sigma>'. wf\<^sub>t\<^sub>r\<^sub>m t"
|
|
using unify_list_wf_trm[of "[(s,t)]" "[]"] by (auto split: option.splits)
|
|
thus ?thesis
|
|
proof (induction \<sigma>' arbitrary: \<sigma> v rule: List.rev_induct)
|
|
case (snoc x \<sigma>' \<sigma> v)
|
|
define \<theta> where "\<theta> = subst_of \<sigma>'"
|
|
hence "wf\<^sub>t\<^sub>r\<^sub>m (\<theta> v)" for v using snoc.prems(2) snoc.IH[of \<theta>] by fastforce
|
|
moreover obtain w t where x: "x = (w,t)" by (metis surj_pair)
|
|
hence \<sigma>: "\<sigma> = Var(w := t) \<circ>\<^sub>s \<theta>" using snoc.prems(1) by (simp add: subst_def \<theta>_def)
|
|
moreover have "wf\<^sub>t\<^sub>r\<^sub>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\<^sub>t\<^sub>r\<^sub>m_def)
|
|
qed
|
|
|
|
lemma mgu_wf_trms:
|
|
assumes "mgu s t = Some \<sigma>" "wf\<^sub>t\<^sub>r\<^sub>m s" "wf\<^sub>t\<^sub>r\<^sub>m t"
|
|
shows "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<sigma>)"
|
|
using mgu_wf_trm[OF assms] by simp
|
|
|
|
subsection \<open>Definitions: Intruder Deduction Relations\<close>
|
|
text \<open>
|
|
A standard Dolev-Yao intruder.
|
|
\<close>
|
|
inductive intruder_deduct::"('fun,'var) terms \<Rightarrow> ('fun,'var) term \<Rightarrow> bool"
|
|
where
|
|
Axiom[simp]: "t \<in> M \<Longrightarrow> intruder_deduct M t"
|
|
| Compose[simp]: "\<lbrakk>length T = arity f; public f; \<And>t. t \<in> set T \<Longrightarrow> intruder_deduct M t\<rbrakk>
|
|
\<Longrightarrow> intruder_deduct M (Fun f T)"
|
|
| Decompose: "\<lbrakk>intruder_deduct M t; Ana t = (K, T); \<And>k. k \<in> set K \<Longrightarrow> intruder_deduct M k;
|
|
t\<^sub>i \<in> set T\<rbrakk>
|
|
\<Longrightarrow> intruder_deduct M t\<^sub>i"
|
|
|
|
text \<open>
|
|
A variant of the intruder relation which limits the intruder to composition only.
|
|
\<close>
|
|
inductive intruder_synth::"('fun,'var) terms \<Rightarrow> ('fun,'var) term \<Rightarrow> bool"
|
|
where
|
|
AxiomC[simp]: "t \<in> M \<Longrightarrow> intruder_synth M t"
|
|
| ComposeC[simp]: "\<lbrakk>length T = arity f; public f; \<And>t. t \<in> set T \<Longrightarrow> intruder_synth M t\<rbrakk>
|
|
\<Longrightarrow> 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 \<turnstile> t" "\<And>t. t \<in> M \<Longrightarrow> P M t"
|
|
"\<And>T f. \<lbrakk>length T = arity f; public f;
|
|
\<And>t. t \<in> set T \<Longrightarrow> M \<turnstile> t;
|
|
\<And>t. t \<in> set T \<Longrightarrow> P M t\<rbrakk> \<Longrightarrow> P M (Fun f T)"
|
|
"\<And>t K T t\<^sub>i. \<lbrakk>M \<turnstile> t; P M t; Ana t = (K, T); \<And>k. k \<in> set K \<Longrightarrow> M \<turnstile> k;
|
|
\<And>k. k \<in> set K \<Longrightarrow> P M k; t\<^sub>i \<in> set T\<rbrakk> \<Longrightarrow> P M t\<^sub>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 \<turnstile>\<^sub>c t" "\<And>t. t \<in> M \<Longrightarrow> P M t"
|
|
"\<And>T f. \<lbrakk>length T = arity f; public f;
|
|
\<And>t. t \<in> set T \<Longrightarrow> M \<turnstile>\<^sub>c t;
|
|
\<And>t. t \<in> set T \<Longrightarrow> P M t\<rbrakk> \<Longrightarrow> P M (Fun f T)"
|
|
shows "P M t"
|
|
using assms by (induct rule: intruder_synth.induct) auto
|
|
|
|
|
|
subsection \<open>Definitions: Analyzed Knowledge and Public Ground Well-formed Terms (PGWTs)\<close>
|
|
definition analyzed::"('fun,'var) terms \<Rightarrow> bool" where
|
|
"analyzed M \<equiv> \<forall>t. M \<turnstile> t \<longleftrightarrow> M \<turnstile>\<^sub>c t"
|
|
|
|
definition analyzed_in where
|
|
"analyzed_in t M \<equiv> \<forall>K R. (Ana t = (K,R) \<and> (\<forall>k \<in> set K. M \<turnstile>\<^sub>c k)) \<longrightarrow> (\<forall>r \<in> set R. M \<turnstile>\<^sub>c r)"
|
|
|
|
definition decomp_closure::"('fun,'var) terms \<Rightarrow> ('fun,'var) terms \<Rightarrow> bool" where
|
|
"decomp_closure M M' \<equiv> \<forall>t. M \<turnstile> t \<and> (\<exists>t' \<in> M. t \<sqsubseteq> t') \<longleftrightarrow> t \<in> M'"
|
|
|
|
inductive public_ground_wf_term::"('fun,'var) term \<Rightarrow> bool" where
|
|
PGWT[simp]: "\<lbrakk>public f; arity f = length T;
|
|
\<And>t. t \<in> set T \<Longrightarrow> public_ground_wf_term t\<rbrakk>
|
|
\<Longrightarrow> public_ground_wf_term (Fun f T)"
|
|
|
|
abbreviation "public_ground_wf_terms \<equiv> {t. public_ground_wf_term t}"
|
|
|
|
lemma public_const_deduct:
|
|
assumes "c \<in> \<C>\<^sub>p\<^sub>u\<^sub>b"
|
|
shows "M \<turnstile> Fun c []" "M \<turnstile>\<^sub>c Fun c []"
|
|
proof -
|
|
have "arity c = 0" "public c" using const_arity_eq_zero \<open>c \<in> \<C>\<^sub>p\<^sub>u\<^sub>b\<close> by auto
|
|
thus "M \<turnstile> Fun c []" "M \<turnstile>\<^sub>c Fun c []"
|
|
using intruder_synth.ComposeC[OF _ \<open>public c\<close>, of "[]"]
|
|
intruder_deduct.Compose[OF _ \<open>public c\<close>, of "[]"]
|
|
by auto
|
|
qed
|
|
|
|
lemma public_const_deduct'[simp]:
|
|
assumes "arity c = 0" "public c"
|
|
shows "M \<turnstile> Fun c []" "M \<turnstile>\<^sub>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 \<turnstile> t" "Fun f T \<in> subterms t"
|
|
and f: "\<not>public f"
|
|
shows "Fun f T \<in> subterms\<^sub>s\<^sub>e\<^sub>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 \<turnstile> Fun f T"
|
|
and f: "\<not>public f"
|
|
and M: "Fun f T \<in> subterms\<^sub>s\<^sub>e\<^sub>t M \<Longrightarrow> Fun f T \<in> M"
|
|
shows "Fun f T \<in> M"
|
|
by (rule M[OF private_fun_deduct_in_ik[OF t term.order_refl f]])
|
|
|
|
lemma pgwt_public: "\<lbrakk>public_ground_wf_term t; Fun f T \<sqsubseteq> t\<rbrakk> \<Longrightarrow> public f"
|
|
by (induct t rule: public_ground_wf_term.induct) auto
|
|
|
|
lemma pgwt_ground: "public_ground_wf_term t \<Longrightarrow> fv t = {}"
|
|
by (induct t rule: public_ground_wf_term.induct) auto
|
|
|
|
lemma pgwt_fun: "public_ground_wf_term t \<Longrightarrow> \<exists>f T. t = Fun f T"
|
|
using pgwt_ground[of t] by (cases t) auto
|
|
|
|
lemma pgwt_arity: "\<lbrakk>public_ground_wf_term t; Fun f T \<sqsubseteq> t\<rbrakk> \<Longrightarrow> arity f = length T"
|
|
by (induct t rule: public_ground_wf_term.induct) auto
|
|
|
|
lemma pgwt_wellformed: "public_ground_wf_term t \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m t"
|
|
by (induct t rule: public_ground_wf_term.induct) auto
|
|
|
|
lemma pgwt_deducible: "public_ground_wf_term t \<Longrightarrow> M \<turnstile>\<^sub>c t"
|
|
by (induct t rule: public_ground_wf_term.induct) auto
|
|
|
|
lemma pgwt_is_empty_synth: "public_ground_wf_term t \<longleftrightarrow> {} \<turnstile>\<^sub>c t"
|
|
proof -
|
|
{ fix M::"('fun,'var) term set" assume "M \<turnstile>\<^sub>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 "{} \<turnstile>\<^sub>c t" "\<And>v. M \<turnstile>\<^sub>c \<theta> v"
|
|
shows "M \<turnstile>\<^sub>c t \<cdot> \<theta>"
|
|
proof -
|
|
{ fix M'::"('fun,'var) term set" assume "M' \<turnstile>\<^sub>c t" "M' = {}" hence "M \<turnstile>\<^sub>c t \<cdot> \<theta>"
|
|
proof (induction t rule: intruder_synth.induct)
|
|
case (ComposeC T f M')
|
|
hence "length (map (\<lambda>t. t \<cdot> \<theta>) T) = arity f" "\<And>x. x \<in> set (map (\<lambda>t. t \<cdot> \<theta>) T) \<Longrightarrow> M \<turnstile>\<^sub>c x"
|
|
by auto
|
|
thus ?case using intruder_synth.ComposeC[of "map (\<lambda>t. t \<cdot> \<theta>) T" f M] \<open>public f\<close> by fastforce
|
|
qed simp
|
|
}
|
|
thus ?thesis using assms by metis
|
|
qed
|
|
|
|
|
|
subsection \<open>Lemmata: Monotonicity, deduction private constants, etc.\<close>
|
|
context
|
|
begin
|
|
lemma ideduct_mono:
|
|
"\<lbrakk>M \<turnstile> t; M \<subseteq> M'\<rbrakk> \<Longrightarrow> M' \<turnstile> t"
|
|
proof (induction rule: intruder_deduct.induct)
|
|
case (Decompose M t K T t\<^sub>i)
|
|
have "\<forall>k. k \<in> set K \<longrightarrow> M' \<turnstile> k" using Decompose.IH \<open>M \<subseteq> M'\<close> by simp
|
|
moreover have "M' \<turnstile> t" using Decompose.IH \<open>M \<subseteq> M'\<close> 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 "\<lbrakk>M \<turnstile>\<^sub>c t; M \<subseteq> M'\<rbrakk> \<Longrightarrow> M' \<turnstile>\<^sub>c t"
|
|
by (induct rule: intruder_synth.induct) auto
|
|
|
|
lemma ideduct_reduce:
|
|
"\<lbrakk>M \<union> M' \<turnstile> t; \<And>t'. t' \<in> M' \<Longrightarrow> M \<turnstile> t'\<rbrakk> \<Longrightarrow> M \<turnstile> 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 "\<lbrakk>M \<union> M' \<turnstile>\<^sub>c t; \<And>t'. t' \<in> M' \<Longrightarrow> M \<turnstile>\<^sub>c t'\<rbrakk> \<Longrightarrow> M \<turnstile>\<^sub>c t"
|
|
by (induct rule: intruder_synth_induct) auto
|
|
|
|
lemma ideduct_mono_eq:
|
|
assumes "\<forall>t. M \<turnstile> t \<longleftrightarrow> M' \<turnstile> t" shows "M \<union> N \<turnstile> t \<longleftrightarrow> M' \<union> N \<turnstile> t"
|
|
proof
|
|
show "M \<union> N \<turnstile> t \<Longrightarrow> M' \<union> N \<turnstile> t"
|
|
proof (induction t rule: intruder_deduct_induct)
|
|
case (Axiom t) thus ?case
|
|
proof (cases "t \<in> M")
|
|
case True
|
|
hence "M \<turnstile> t" using intruder_deduct.Axiom by metis
|
|
thus ?thesis using assms ideduct_mono[of M' t "M' \<union> 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\<^sub>i) thus ?case using intruder_deduct.Decompose[of "M' \<union> N" t K T] by auto
|
|
qed
|
|
|
|
show "M' \<union> N \<turnstile> t \<Longrightarrow> M \<union> N \<turnstile> t"
|
|
proof (induction t rule: intruder_deduct_induct)
|
|
case (Axiom t) thus ?case
|
|
proof (cases "t \<in> M'")
|
|
case True
|
|
hence "M' \<turnstile> t" using intruder_deduct.Axiom by metis
|
|
thus ?thesis using assms ideduct_mono[of M t "M \<union> 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\<^sub>i) thus ?case using intruder_deduct.Decompose[of "M \<union> N" t K T] by auto
|
|
qed
|
|
qed
|
|
|
|
lemma deduct_synth_subterm:
|
|
fixes M::"('fun,'var) terms" and t::"('fun,'var) term"
|
|
assumes "M \<turnstile>\<^sub>c t" "s \<in> subterms t" "\<forall>m \<in> M. \<forall>s \<in> subterms m. M \<turnstile>\<^sub>c s"
|
|
shows "M \<turnstile>\<^sub>c s"
|
|
using assms by (induct t rule: intruder_synth.induct) auto
|
|
|
|
lemma deduct_if_synth[intro, dest]: "M \<turnstile>\<^sub>c t \<Longrightarrow> M \<turnstile> t"
|
|
by (induct rule: intruder_synth.induct) auto
|
|
|
|
private lemma ideduct_ik_eq: assumes "\<forall>t \<in> M. M' \<turnstile> t" shows "M' \<turnstile> t \<longleftrightarrow> M' \<union> M \<turnstile> t"
|
|
by (meson assms ideduct_mono ideduct_reduce sup_ge1)
|
|
|
|
private lemma synth_if_deduct_empty: "{} \<turnstile> t \<Longrightarrow> {} \<turnstile>\<^sub>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 \<in> 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 "\<forall>t. M \<turnstile> t \<longleftrightarrow> M' \<turnstile>\<^sub>c t" "M \<subseteq> M'"
|
|
and "\<forall>t. M' \<union> N \<turnstile> t \<longleftrightarrow> M' \<union> N \<union> D \<turnstile>\<^sub>c t"
|
|
shows "M \<union> N \<turnstile> t \<longleftrightarrow> M' \<union> N \<union> D \<turnstile>\<^sub>c t"
|
|
proof -
|
|
have "\<forall>m \<in> M'. M \<turnstile> m" using assms(1) by auto
|
|
hence "\<forall>t. M \<turnstile> t \<longleftrightarrow> M' \<turnstile> t" by (metis assms(1,2) deduct_if_synth ideduct_reduce sup.absorb2)
|
|
hence "\<forall>t. M' \<union> N \<turnstile> t \<longleftrightarrow> M \<union> N \<turnstile> t" by (meson ideduct_mono_eq)
|
|
thus ?thesis by (meson assms(3))
|
|
qed
|
|
|
|
lemma ideduct_subst: "M \<turnstile> t \<Longrightarrow> M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta> \<turnstile> t \<cdot> \<delta>"
|
|
proof (induction t rule: intruder_deduct_induct)
|
|
case (Compose T f)
|
|
hence "length (map (\<lambda>t. t \<cdot> \<delta>) T) = arity f" "\<And>t. t \<in> set T \<Longrightarrow> M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta> \<turnstile> t \<cdot> \<delta>" by auto
|
|
thus ?case using intruder_deduct.Compose[OF _ Compose.hyps(2), of "map (\<lambda>t. t \<cdot> \<delta>) T"] by auto
|
|
next
|
|
case (Decompose t K M' m')
|
|
hence "Ana (t \<cdot> \<delta>) = (K \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>, M' \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>)"
|
|
"\<And>k. k \<in> set (K \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>) \<Longrightarrow> M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta> \<turnstile> k"
|
|
"m' \<cdot> \<delta> \<in> set (M' \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>)"
|
|
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 \<delta>::"('fun,'var) subst"
|
|
shows "M \<turnstile>\<^sub>c t \<Longrightarrow> M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta> \<turnstile>\<^sub>c t \<cdot> \<delta>"
|
|
proof (induction t rule: intruder_synth_induct)
|
|
case (ComposeC T f)
|
|
hence "length (map (\<lambda>t. t \<cdot> \<delta>) T) = arity f" "\<And>t. t \<in> set T \<Longrightarrow> M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta> \<turnstile>\<^sub>c t \<cdot> \<delta>" by auto
|
|
thus ?case using intruder_synth.ComposeC[OF _ ComposeC.hyps(2), of "map (\<lambda>t. t \<cdot> \<delta>) T"] by auto
|
|
qed simp
|
|
|
|
lemma ideduct_vars:
|
|
assumes "M \<turnstile> t"
|
|
shows "fv t \<subseteq> fv\<^sub>s\<^sub>e\<^sub>t M"
|
|
using assms
|
|
proof (induction t rule: intruder_deduct_induct)
|
|
case (Decompose t K T t\<^sub>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 \<turnstile>\<^sub>c t"
|
|
shows "fv t \<subseteq> fv\<^sub>s\<^sub>e\<^sub>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 \<turnstile>\<^sub>c t" "f \<in> funs_term t" "\<not>public f"
|
|
shows "f \<in> \<Union>(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 \<turnstile>\<^sub>c Fun c []" "\<not>public c"
|
|
shows "Fun c [] \<in> 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 "\<forall>t \<in> M. N \<turnstile>\<^sub>c t"
|
|
and "M \<turnstile>\<^sub>c t"
|
|
shows "N \<turnstile>\<^sub>c t"
|
|
using assms(2,1) by (induct t rule: intruder_synth.induct) auto
|
|
end
|
|
|
|
subsection \<open>Lemmata: Analyzed Intruder Knowledge Closure\<close>
|
|
lemma deducts_eq_if_analyzed: "analyzed M \<Longrightarrow> M \<turnstile> t \<longleftrightarrow> M \<turnstile>\<^sub>c t"
|
|
unfolding analyzed_def by auto
|
|
|
|
lemma closure_is_superset: "decomp_closure M M' \<Longrightarrow> M \<subseteq> M'"
|
|
unfolding decomp_closure_def by force
|
|
|
|
lemma deduct_if_closure_deduct: "\<lbrakk>M' \<turnstile> t; decomp_closure M M'\<rbrakk> \<Longrightarrow> M \<turnstile> t"
|
|
proof (induction t rule: intruder_deduct.induct)
|
|
case (Decompose M' t K T t\<^sub>i)
|
|
thus ?case using intruder_deduct.Decompose[OF _ \<open>Ana t = (K,T)\<close> _ \<open>t\<^sub>i \<in> set T\<close>] by simp
|
|
qed (auto simp add: decomp_closure_def)
|
|
|
|
lemma deduct_if_closure_synth: "\<lbrakk>decomp_closure M M'; M' \<turnstile>\<^sub>c t\<rbrakk> \<Longrightarrow> M \<turnstile> t"
|
|
using deduct_if_closure_deduct by blast
|
|
|
|
lemma decomp_closure_subterms_composable:
|
|
assumes "decomp_closure M M'"
|
|
and "M' \<turnstile>\<^sub>c t'" "M' \<turnstile> t" "t \<sqsubseteq> t'"
|
|
shows "M' \<turnstile>\<^sub>c t"
|
|
using \<open>M' \<turnstile>\<^sub>c t'\<close> assms
|
|
proof (induction t' rule: intruder_synth.induct)
|
|
case (AxiomC t' M')
|
|
have "M \<turnstile> t" using \<open>M' \<turnstile> t\<close> deduct_if_closure_deduct AxiomC.prems(1) by blast
|
|
moreover
|
|
{ have "\<exists>s \<in> M. t' \<sqsubseteq> s" using \<open>t' \<in> M'\<close> AxiomC.prems(1) unfolding decomp_closure_def by blast
|
|
hence "\<exists>s \<in> M. t \<sqsubseteq> s" using \<open>t \<sqsubseteq> t'\<close> term.order_trans by auto
|
|
}
|
|
ultimately have "t \<in> 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' \<turnstile>\<^sub>c t" using \<open>M' \<turnstile>\<^sub>c ?t'\<close> \<open>t = ?t'\<close> by simp }
|
|
moreover
|
|
{ assume "t \<noteq> ?t'"
|
|
have "\<exists>x \<in> set T. t \<sqsubseteq> x" using \<open>t \<sqsubseteq> ?t'\<close> \<open>t \<noteq> ?t'\<close> by simp
|
|
hence "M' \<turnstile>\<^sub>c t" using ComposeC.IH ComposeC.prems(1,3) ComposeC.hyps(3) by blast
|
|
}
|
|
ultimately show ?case using cases_simp[of "t = ?t'" "M' \<turnstile>\<^sub>c t"] by simp
|
|
qed
|
|
|
|
lemma decomp_closure_analyzed:
|
|
assumes "decomp_closure M M'"
|
|
shows "analyzed M'"
|
|
proof -
|
|
{ fix t assume "M' \<turnstile> t" have "M' \<turnstile>\<^sub>c t" using \<open>M' \<turnstile> t\<close> assms
|
|
proof (induction t rule: intruder_deduct.induct)
|
|
case (Decompose M' t K T t\<^sub>i)
|
|
hence "M' \<turnstile> t\<^sub>i" using Decompose.hyps intruder_deduct.Decompose by blast
|
|
moreover have "t\<^sub>i \<sqsubseteq> t"
|
|
using Decompose.hyps(4) Ana_subterm[OF Decompose.hyps(2)] by blast
|
|
moreover have "M' \<turnstile>\<^sub>c t" using Decompose.IH(1) Decompose.prems by blast
|
|
ultimately show "M' \<turnstile>\<^sub>c t\<^sub>i" using decomp_closure_subterms_composable Decompose.prems by blast
|
|
qed auto
|
|
}
|
|
moreover have "\<forall>t. M \<turnstile>\<^sub>c t \<longrightarrow> M \<turnstile> t" by auto
|
|
ultimately show ?thesis by (auto simp add: decomp_closure_def analyzed_def)
|
|
qed
|
|
|
|
lemma analyzed_if_all_analyzed_in:
|
|
assumes M: "\<forall>t \<in> M. analyzed_in t M"
|
|
shows "analyzed M"
|
|
proof (unfold analyzed_def, intro allI iffI)
|
|
fix t
|
|
assume t: "M \<turnstile> t"
|
|
thus "M \<turnstile>\<^sub>c t"
|
|
proof (induction t rule: intruder_deduct_induct)
|
|
case (Decompose t K T t\<^sub>i)
|
|
{ assume "t \<in> 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" "\<And>s. s \<in> set S \<Longrightarrow> M \<turnstile>\<^sub>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:
|
|
"(\<forall>t \<in> M. analyzed_in t M) \<longleftrightarrow> analyzed M"
|
|
proof
|
|
show "analyzed M \<Longrightarrow> \<forall>t \<in> 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 "\<exists>M'. (\<forall>t. M \<turnstile> t \<longleftrightarrow> M' \<turnstile>\<^sub>c t) \<and> decomp_closure M M' \<and> (finite M \<longrightarrow> finite M')"
|
|
proof -
|
|
let ?M' = "{t. M \<turnstile> t \<and> (\<exists>t' \<in> M. t \<sqsubseteq> t')}"
|
|
|
|
have M'_closes: "decomp_closure M ?M'" unfolding decomp_closure_def by simp
|
|
hence "M \<subseteq> ?M'" using closure_is_superset by simp
|
|
|
|
have "\<forall>t. ?M' \<turnstile>\<^sub>c t \<longrightarrow> M \<turnstile> t" using deduct_if_closure_synth[OF M'_closes] by blast
|
|
moreover have "\<forall>t. M \<turnstile> t \<longrightarrow> ?M' \<turnstile> t" using ideduct_mono[OF _ \<open>M \<subseteq> ?M'\<close>] by simp
|
|
moreover have "analyzed ?M'" using decomp_closure_analyzed[OF M'_closes] .
|
|
ultimately have "\<forall>t. M \<turnstile> t \<longleftrightarrow> ?M' \<turnstile>\<^sub>c t" unfolding analyzed_def by blast
|
|
moreover have "finite M \<longrightarrow> finite ?M'" by auto
|
|
ultimately show ?thesis using M'_closes by blast
|
|
qed
|
|
|
|
|
|
subsection \<open>Intruder Variants: Numbered and Composition-Restricted Intruder Deduction Relations\<close>
|
|
text \<open>
|
|
A variant of the intruder relation which restricts composition to only those terms that satisfy
|
|
a given predicate Q.
|
|
\<close>
|
|
inductive intruder_deduct_restricted::
|
|
"('fun,'var) terms \<Rightarrow> (('fun,'var) term \<Rightarrow> bool) \<Rightarrow> ('fun,'var) term \<Rightarrow> bool"
|
|
("\<langle>_;_\<rangle> \<turnstile>\<^sub>r _" 50)
|
|
where
|
|
AxiomR[simp]: "t \<in> M \<Longrightarrow> \<langle>M; Q\<rangle> \<turnstile>\<^sub>r t"
|
|
| ComposeR[simp]: "\<lbrakk>length T = arity f; public f; \<And>t. t \<in> set T \<Longrightarrow> \<langle>M; Q\<rangle> \<turnstile>\<^sub>r t; Q (Fun f T)\<rbrakk>
|
|
\<Longrightarrow> \<langle>M; Q\<rangle> \<turnstile>\<^sub>r Fun f T"
|
|
| DecomposeR: "\<lbrakk>\<langle>M; Q\<rangle> \<turnstile>\<^sub>r t; Ana t = (K, T); \<And>k. k \<in> set K \<Longrightarrow> \<langle>M; Q\<rangle> \<turnstile>\<^sub>r k; t\<^sub>i \<in> set T\<rbrakk>
|
|
\<Longrightarrow> \<langle>M; Q\<rangle> \<turnstile>\<^sub>r t\<^sub>i"
|
|
|
|
text \<open>
|
|
A variant of the intruder relation equipped with a number representing the heigth of the
|
|
derivation tree (i.e., \<open>\<langle>M; k\<rangle> \<turnstile>\<^sub>n t\<close> iff k is the maximum number of applications of the compose
|
|
an decompose rules in any path of the derivation tree for \<open>M \<turnstile> t\<close>).
|
|
\<close>
|
|
inductive intruder_deduct_num::
|
|
"('fun,'var) terms \<Rightarrow> nat \<Rightarrow> ('fun,'var) term \<Rightarrow> bool"
|
|
("\<langle>_; _\<rangle> \<turnstile>\<^sub>n _" 50)
|
|
where
|
|
AxiomN[simp]: "t \<in> M \<Longrightarrow> \<langle>M; 0\<rangle> \<turnstile>\<^sub>n t"
|
|
| ComposeN[simp]: "\<lbrakk>length T = arity f; public f; \<And>t. t \<in> set T \<Longrightarrow> \<langle>M; steps t\<rangle> \<turnstile>\<^sub>n t\<rbrakk>
|
|
\<Longrightarrow> \<langle>M; Suc (Max (insert 0 (steps ` set T)))\<rangle> \<turnstile>\<^sub>n Fun f T"
|
|
| DecomposeN: "\<lbrakk>\<langle>M; n\<rangle> \<turnstile>\<^sub>n t; Ana t = (K, T); \<And>k. k \<in> set K \<Longrightarrow> \<langle>M; steps k\<rangle> \<turnstile>\<^sub>n k; t\<^sub>i \<in> set T\<rbrakk>
|
|
\<Longrightarrow> \<langle>M; Suc (Max (insert n (steps ` set K)))\<rangle> \<turnstile>\<^sub>n t\<^sub>i"
|
|
|
|
lemma intruder_deduct_restricted_induct[consumes 1, case_names AxiomR ComposeR DecomposeR]:
|
|
assumes "\<langle>M; Q\<rangle> \<turnstile>\<^sub>r t" "\<And>t. t \<in> M \<Longrightarrow> P M Q t"
|
|
"\<And>T f. \<lbrakk>length T = arity f; public f;
|
|
\<And>t. t \<in> set T \<Longrightarrow> \<langle>M; Q\<rangle> \<turnstile>\<^sub>r t;
|
|
\<And>t. t \<in> set T \<Longrightarrow> P M Q t; Q (Fun f T)
|
|
\<rbrakk> \<Longrightarrow> P M Q (Fun f T)"
|
|
"\<And>t K T t\<^sub>i. \<lbrakk>\<langle>M; Q\<rangle> \<turnstile>\<^sub>r t; P M Q t; Ana t = (K, T); \<And>k. k \<in> set K \<Longrightarrow> \<langle>M; Q\<rangle> \<turnstile>\<^sub>r k;
|
|
\<And>k. k \<in> set K \<Longrightarrow> P M Q k; t\<^sub>i \<in> set T\<rbrakk> \<Longrightarrow> P M Q t\<^sub>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 "\<langle>M; n\<rangle> \<turnstile>\<^sub>n t" "\<And>t. t \<in> M \<Longrightarrow> P M 0 t"
|
|
"\<And>T f steps.
|
|
\<lbrakk>length T = arity f; public f;
|
|
\<And>t. t \<in> set T \<Longrightarrow> \<langle>M; steps t\<rangle> \<turnstile>\<^sub>n t;
|
|
\<And>t. t \<in> set T \<Longrightarrow> P M (steps t) t\<rbrakk>
|
|
\<Longrightarrow> P M (Suc (Max (insert 0 (steps ` set T)))) (Fun f T)"
|
|
"\<And>t K T t\<^sub>i steps n.
|
|
\<lbrakk>\<langle>M; n\<rangle> \<turnstile>\<^sub>n t; P M n t; Ana t = (K, T);
|
|
\<And>k. k \<in> set K \<Longrightarrow> \<langle>M; steps k\<rangle> \<turnstile>\<^sub>n k;
|
|
t\<^sub>i \<in> set T; \<And>k. k \<in> set K \<Longrightarrow> P M (steps k) k\<rbrakk>
|
|
\<Longrightarrow> P M (Suc (Max (insert n (steps ` set K)))) t\<^sub>i"
|
|
shows "P M n t"
|
|
using assms by (induct rule: intruder_deduct_num.induct) blast+
|
|
|
|
lemma ideduct_restricted_mono:
|
|
"\<lbrakk>\<langle>M; P\<rangle> \<turnstile>\<^sub>r t; M \<subseteq> M'\<rbrakk> \<Longrightarrow> \<langle>M'; P\<rangle> \<turnstile>\<^sub>r t"
|
|
proof (induction rule: intruder_deduct_restricted_induct)
|
|
case (DecomposeR t K T t\<^sub>i)
|
|
have "\<forall>k. k \<in> set K \<longrightarrow> \<langle>M'; P\<rangle> \<turnstile>\<^sub>r k" using DecomposeR.IH \<open>M \<subseteq> M'\<close> by simp
|
|
moreover have "\<langle>M'; P\<rangle> \<turnstile>\<^sub>r t" using DecomposeR.IH \<open>M \<subseteq> M'\<close> by simp
|
|
ultimately show ?case
|
|
using DecomposeR
|
|
intruder_deduct_restricted.DecomposeR[OF _ DecomposeR.hyps(2) _ DecomposeR.hyps(4)]
|
|
by blast
|
|
qed auto
|
|
|
|
|
|
subsection \<open>Lemmata: Intruder Deduction Equivalences\<close>
|
|
lemma deduct_if_restricted_deduct: "\<langle>M;P\<rangle> \<turnstile>\<^sub>r m \<Longrightarrow> M \<turnstile> m"
|
|
proof (induction m rule: intruder_deduct_restricted_induct)
|
|
case (DecomposeR t K T t\<^sub>i) thus ?case using intruder_deduct.Decompose by blast
|
|
qed simp_all
|
|
|
|
lemma restricted_deduct_if_restricted_ik:
|
|
assumes "\<langle>M;P\<rangle> \<turnstile>\<^sub>r m" "\<forall>m \<in> M. P m"
|
|
and P: "\<forall>t t'. P t \<longrightarrow> t' \<sqsubseteq> t \<longrightarrow> P t'"
|
|
shows "P m"
|
|
using assms(1)
|
|
proof (induction m rule: intruder_deduct_restricted_induct)
|
|
case (DecomposeR t K T t\<^sub>i)
|
|
obtain f S where "t = Fun f S" using Ana_var \<open>t\<^sub>i \<in> set T\<close> \<open>Ana t = (K, T)\<close> 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" "\<forall>t t'. P t \<longrightarrow> t' \<sqsubseteq> t \<longrightarrow> P t'"
|
|
and m: "M \<turnstile>\<^sub>c m"
|
|
shows "\<langle>M; P\<rangle> \<turnstile>\<^sub>r m"
|
|
using m P(1)
|
|
proof (induction m rule: intruder_synth_induct)
|
|
case (ComposeC T f)
|
|
hence "\<langle>M; P\<rangle> \<turnstile>\<^sub>r t" when t: "t \<in> 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 "\<langle>M; 0\<rangle> \<turnstile>\<^sub>n t" shows "t \<in> M"
|
|
proof -
|
|
{ fix k assume "\<langle>M; k\<rangle> \<turnstile>\<^sub>n t" hence "k > 0 \<or> t \<in> M" by (induct t) auto
|
|
} thus ?thesis using assms by auto
|
|
qed
|
|
|
|
lemma deduct_if_deduct_num: "\<langle>M; k\<rangle> \<turnstile>\<^sub>n t \<Longrightarrow> M \<turnstile> 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 \<turnstile> t \<Longrightarrow> \<exists>k. \<langle>M; k\<rangle> \<turnstile>\<^sub>n t"
|
|
proof (induction t rule: intruder_deduct_induct)
|
|
case (Compose T f)
|
|
then obtain steps where *: "\<forall>t \<in> set T. \<langle>M; steps t\<rangle> \<turnstile>\<^sub>n t" by moura
|
|
then obtain n where "\<forall>t \<in> set T. steps t \<le> 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\<^sub>i)
|
|
hence "\<And>u. u \<in> insert t (set K) \<Longrightarrow> \<exists>k. \<langle>M; k\<rangle> \<turnstile>\<^sub>n u" by auto
|
|
then obtain steps where *: "\<langle>M; steps t\<rangle> \<turnstile>\<^sub>n t" "\<forall>t \<in> set K. \<langle>M; steps t\<rangle> \<turnstile>\<^sub>n t" by moura
|
|
then obtain n where "steps t \<le> n" "\<forall>t \<in> set K. steps t \<le> 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: "\<forall>m \<in> M. \<forall>f T. Fun f T \<sqsubseteq> m \<longrightarrow> P f T"
|
|
and t: "\<langle>M; k\<rangle> \<turnstile>\<^sub>n t" "Fun f T \<sqsubseteq> t" "\<not>P f T"
|
|
shows "\<exists>l \<le> k. (\<langle>M; l\<rangle> \<turnstile>\<^sub>n Fun f T) \<and> (\<forall>t \<in> set T. \<exists>j < l. \<langle>M; j\<rangle> \<turnstile>\<^sub>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 "\<langle>M; Suc (Max (insert 0 (steps ` set T')))\<rangle> \<turnstile>\<^sub>n Fun f T" "T = T'"
|
|
using intruder_deduct_num.ComposeN[OF ComposeN.hyps] by auto
|
|
moreover have "\<And>t. t \<in> set T \<Longrightarrow> \<langle>M; steps t\<rangle> \<turnstile>\<^sub>n t"
|
|
using True ComposeN.hyps(3) by auto
|
|
moreover have "\<And>t. t \<in> set T \<Longrightarrow> 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' \<in> set T'" "Fun f T \<sqsubseteq> t'" using ComposeN by auto
|
|
hence "\<exists>l \<le> steps t'. (\<langle>M; l\<rangle> \<turnstile>\<^sub>n Fun f T) \<and> (\<forall>t \<in> set T. \<exists>j < l. \<langle>M; j\<rangle> \<turnstile>\<^sub>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\<^sub>i steps n)
|
|
hence *: "Fun f T \<sqsubseteq> t"
|
|
using term.order_trans[of "Fun f T" t\<^sub>i t] Ana_subterm[of t K T']
|
|
by blast
|
|
have "\<exists>l \<le> n. (\<langle>M; l\<rangle> \<turnstile>\<^sub>n Fun f T) \<and> (\<forall>t' \<in> set T. \<exists>j < l. \<langle>M; j\<rangle> \<turnstile>\<^sub>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 "\<langle>M; n\<rangle> \<turnstile>\<^sub>n t"
|
|
shows "t \<in> M \<or>
|
|
(\<exists>f T. t = Fun f T \<and> public f \<and> length T = arity f \<and> (\<forall>t \<in> set T. \<exists>l < n. \<langle>M; l\<rangle> \<turnstile>\<^sub>n t)) \<or>
|
|
(\<exists>m \<in> subterms\<^sub>s\<^sub>e\<^sub>t M.
|
|
(\<exists>l < n. \<langle>M; l\<rangle> \<turnstile>\<^sub>n m) \<and> (\<forall>k \<in> set (fst (Ana m)). \<exists>l < n. \<langle>M; l\<rangle> \<turnstile>\<^sub>n k) \<and>
|
|
t \<in> set (snd (Ana m)))"
|
|
(is "?P t n \<or> ?Q t n \<or> ?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 \<in> M" using deduct_zero_in_ik "1.prems"(1) by metis
|
|
thus ?thesis by auto
|
|
next
|
|
case (Suc n')
|
|
hence "\<langle>M; Suc n'\<rangle> \<turnstile>\<^sub>n t"
|
|
"\<forall>m < Suc n'. \<forall>x. (\<langle>M; m\<rangle> \<turnstile>\<^sub>n x) \<longrightarrow> ?P x m \<or> ?Q x m \<or> ?R x m"
|
|
using "1.prems" "1.IH" by blast+
|
|
hence "?P t (Suc n') \<or> ?Q t (Suc n') \<or> ?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 "\<And>t. t \<in> set T \<Longrightarrow> 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\<^sub>i steps n)
|
|
have 0: "n < Suc (Max (insert n (steps ` set K)))"
|
|
"\<And>k. k \<in> set K \<Longrightarrow> 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 \<or> ?Q t j \<or> ?R t j" when jt: "j < n" "\<langle>M; j\<rangle> \<turnstile>\<^sub>n t" for j t
|
|
using jt DecomposeN.prems(1) 0(1)
|
|
by simp
|
|
|
|
have IH2: "?P t n \<or> ?Q t n \<or> ?R t n"
|
|
using DecomposeN.IH(1) IH1
|
|
by simp
|
|
|
|
have 1: "\<forall>k \<in> set (fst (Ana t)). \<exists>l < Suc (Max (insert n (steps ` set K))). \<langle>M; l\<rangle> \<turnstile>\<^sub>n k"
|
|
using DecomposeN.hyps(1,2,3) 0(2)
|
|
by auto
|
|
|
|
have 2: "t\<^sub>i \<in> set (snd (Ana t))"
|
|
using DecomposeN.hyps(2,4)
|
|
by fastforce
|
|
|
|
have 3: "t \<in> subterms\<^sub>s\<^sub>e\<^sub>t M" when "t \<in> set (snd (Ana m))" "m \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>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\<^sub>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\<^sub>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" "\<forall>t \<in> set S. \<exists>l < n. \<langle>M; l\<rangle> \<turnstile>\<^sub>n t"
|
|
using * by moura
|
|
then obtain l where l: "l < n" "\<langle>M; l\<rangle> \<turnstile>\<^sub>n t\<^sub>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 restricted_deduct_if_deduct:
|
|
assumes M: "\<forall>m \<in> M. \<forall>f T. Fun f T \<sqsubseteq> m \<longrightarrow> P (Fun f T)"
|
|
and P_subterm: "\<forall>f T t. M \<turnstile> Fun f T \<longrightarrow> P (Fun f T) \<longrightarrow> t \<in> set T \<longrightarrow> P t"
|
|
and P_Ana_key: "\<forall>t K T k. M \<turnstile> t \<longrightarrow> P t \<longrightarrow> Ana t = (K, T) \<longrightarrow> M \<turnstile> k \<longrightarrow> k \<in> set K \<longrightarrow> P k"
|
|
and m: "M \<turnstile> m" "P m"
|
|
shows "\<langle>M; P\<rangle> \<turnstile>\<^sub>r m"
|
|
proof -
|
|
{ fix k assume "\<langle>M; k\<rangle> \<turnstile>\<^sub>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 \<in> M" using deduct_zero_in_ik "1.prems"(1) by metis
|
|
thus ?thesis by auto
|
|
next
|
|
case (Suc n')
|
|
hence "\<langle>M; Suc n'\<rangle> \<turnstile>\<^sub>n m"
|
|
"\<forall>m < Suc n'. \<forall>x. (\<langle>M; m\<rangle> \<turnstile>\<^sub>n x) \<longrightarrow> P x \<longrightarrow> \<langle>M;P\<rangle> \<turnstile>\<^sub>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 \<in> set T" for t
|
|
using Max_less_iff[of "insert 0 (steps ` set T)"] that
|
|
by blast
|
|
|
|
have **: "P t" when "t \<in> 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 "\<langle>M; P\<rangle> \<turnstile>\<^sub>r t" when "t \<in> 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\<^sub>i steps l)
|
|
show ?case
|
|
proof (cases "P t")
|
|
case True
|
|
hence "\<And>k. k \<in> set K \<Longrightarrow> P k"
|
|
using P_Ana_key DecomposeN.hyps(1,2,3) deduct_if_deduct_num
|
|
by blast
|
|
moreover have
|
|
"\<And>k m x. k \<in> set K \<Longrightarrow> m < steps k \<Longrightarrow> \<langle>M; m\<rangle> \<turnstile>\<^sub>n x \<Longrightarrow> P x \<Longrightarrow> \<langle>M;P\<rangle> \<turnstile>\<^sub>r x"
|
|
proof -
|
|
fix k m x assume *: "k \<in> set K" "m < steps k" "\<langle>M; m\<rangle> \<turnstile>\<^sub>n x" "P x"
|
|
have "steps k \<in> 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 "\<langle>M;P\<rangle> \<turnstile>\<^sub>r x" using DecomposeN.prems(1) *(3,4) by simp
|
|
qed
|
|
ultimately have "\<And>k. k \<in> set K \<Longrightarrow> \<langle>M; P\<rangle> \<turnstile>\<^sub>r k"
|
|
using DecomposeN.IH(2) by auto
|
|
moreover have "\<langle>M; P\<rangle> \<turnstile>\<^sub>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 \<sqsubseteq> t" "\<not>P (Fun g S)" using False by force+
|
|
have "\<exists>j<l. \<langle>M; j\<rangle> \<turnstile>\<^sub>n t\<^sub>i"
|
|
using gS DecomposeN.hyps(2,4) Ana_fun_subterm[of g S K T]
|
|
deduct_normalize[of M "\<lambda>f T. P (Fun f T)", OF M DecomposeN.hyps(1) *]
|
|
by force
|
|
hence "\<exists>j<Suc (Max (insert l (steps ` set K))). \<langle>M; j\<rangle> \<turnstile>\<^sub>n t\<^sub>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 "\<forall>m \<in> M. P m"
|
|
and "\<forall>t t'. P t \<longrightarrow> t' \<sqsubseteq> t \<longrightarrow> P t'"
|
|
and "\<forall>t K T k. P t \<longrightarrow> Ana t = (K, T) \<longrightarrow> k \<in> set K \<longrightarrow> P k"
|
|
and "M \<turnstile> m" "P m"
|
|
shows "\<langle>M; P\<rangle> \<turnstile>\<^sub>r m"
|
|
using restricted_deduct_if_deduct[of M P m] assms
|
|
by blast
|
|
|
|
lemma private_const_deduct:
|
|
assumes c: "\<not>public c" "M \<turnstile> (Fun c []::('fun,'var) term)"
|
|
shows "Fun c [] \<in> M \<or>
|
|
(\<exists>m \<in> subterms\<^sub>s\<^sub>e\<^sub>t M. M \<turnstile> m \<and> (\<forall>k \<in> set (fst (Ana m)). M \<turnstile> m) \<and>
|
|
Fun c [] \<in> set (snd (Ana m)))"
|
|
proof -
|
|
obtain n where "\<langle>M; n\<rangle> \<turnstile>\<^sub>n Fun c []"
|
|
using c(2) deduct_num_if_deduct by moura
|
|
hence "Fun c [] \<in> M \<or>
|
|
(\<exists>m \<in> subterms\<^sub>s\<^sub>e\<^sub>t M.
|
|
(\<exists>l < n. \<langle>M; l\<rangle> \<turnstile>\<^sub>n m) \<and>
|
|
(\<forall>k \<in> set (fst (Ana m)). \<exists>l < n. \<langle>M; l\<rangle> \<turnstile>\<^sub>n k) \<and> Fun c [] \<in> 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 \<turnstile> Fun f T" "Fun c [] \<in> set T" "\<forall>m \<in> subterms\<^sub>s\<^sub>e\<^sub>t M. Fun f T \<notin> set (snd (Ana m))"
|
|
and c: "\<not>public c" "Fun c [] \<notin> M" "\<forall>m \<in> subterms\<^sub>s\<^sub>e\<^sub>t M. Fun c [] \<notin> set (snd (Ana m))"
|
|
shows "Fun f T \<in> M"
|
|
proof -
|
|
have *: "\<nexists>n. \<langle>M; n\<rangle> \<turnstile>\<^sub>n Fun c []"
|
|
using private_const_deduct[OF c(1)] c(2,3) deduct_if_deduct_num
|
|
by blast
|
|
|
|
obtain n where n: "\<langle>M; n\<rangle> \<turnstile>\<^sub>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 \<open>Executable Definitions for Code Generation\<close>
|
|
fun intruder_synth' where
|
|
"intruder_synth' pu ar M (Var x) = (Var x \<in> M)"
|
|
| "intruder_synth' pu ar M (Fun f T) = (
|
|
Fun f T \<in> M \<or> (pu f \<and> length T = ar f \<and> list_all (intruder_synth' pu ar M) T))"
|
|
|
|
definition "wf\<^sub>t\<^sub>r\<^sub>m' ar t \<equiv> (\<forall>s \<in> subterms t. is_Fun s \<longrightarrow> ar (the_Fun s) = length (args s))"
|
|
|
|
definition "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s' ar M \<equiv> (\<forall>t \<in> M. wf\<^sub>t\<^sub>r\<^sub>m' ar t)"
|
|
|
|
definition "analyzed_in' An pu ar t M \<equiv> (case An t of
|
|
(K,T) \<Rightarrow> (\<forall>k \<in> set K. intruder_synth' pu ar M k) \<longrightarrow> (\<forall>s \<in> 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"
|
|
"\<And>x. intruder_synth' public arity M (Var x) \<Longrightarrow> P (Var x)"
|
|
"\<And>f T. (\<And>z. z \<in> set T \<Longrightarrow> intruder_synth' public arity M z \<Longrightarrow> P z) \<Longrightarrow>
|
|
intruder_synth' public arity M (Fun f T) \<Longrightarrow> 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\<^sub>t\<^sub>r\<^sub>m_code[code_unfold]:
|
|
"wf\<^sub>t\<^sub>r\<^sub>m t = wf\<^sub>t\<^sub>r\<^sub>m' arity t"
|
|
unfolding wf\<^sub>t\<^sub>r\<^sub>m_def wf\<^sub>t\<^sub>r\<^sub>m'_def
|
|
by auto
|
|
|
|
lemma (in intruder_model) wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s_code[code_unfold]:
|
|
"wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s M = wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s' arity M"
|
|
using wf\<^sub>t\<^sub>r\<^sub>m_code
|
|
unfolding wf\<^sub>t\<^sub>r\<^sub>m\<^sub>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 \<longleftrightarrow> ?B")
|
|
proof
|
|
show "?A \<Longrightarrow> ?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 \<Longrightarrow> ?A"
|
|
proof (induction t rule: intruder_synth'_induct)
|
|
case (Fun f T) thus ?case
|
|
proof (cases "Fun f T \<in> 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
|