1180 lines
71 KiB
Plaintext
1180 lines
71 KiB
Plaintext
(*
|
|
(C) Copyright Andreas Viktor Hess, DTU, 2018-2020
|
|
(C) Copyright Sebastian A. Mödersheim, DTU, 2018-2020
|
|
(C) Copyright Achim D. Brucker, University of Sheffield, 2018-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: Parallel_Compositionality.thy
|
|
Author: Andreas Viktor Hess, DTU
|
|
Author: Sebastian A. Mödersheim, DTU
|
|
Author: Achim D. Brucker, The University of Sheffield
|
|
*)
|
|
|
|
section \<open>Parallel Compositionality of Security Protocols\<close>
|
|
text \<open>\label{sec:Parallel-Compositionality}\<close>
|
|
theory Parallel_Compositionality
|
|
imports Typing_Result Labeled_Strands
|
|
begin
|
|
|
|
|
|
subsection \<open>Definitions: Labeled Typed Model Locale\<close>
|
|
locale labeled_typed_model = typed_model arity public Ana \<Gamma>
|
|
for arity::"'fun \<Rightarrow> nat"
|
|
and public::"'fun \<Rightarrow> bool"
|
|
and Ana::"('fun,'var) term \<Rightarrow> (('fun,'var) term list \<times> ('fun,'var) term list)"
|
|
and \<Gamma>::"('fun,'var) term \<Rightarrow> ('fun,'atom::finite) term_type"
|
|
+
|
|
fixes label_witness1 and label_witness2::"'lbl"
|
|
assumes at_least_2_labels: "label_witness1 \<noteq> label_witness2"
|
|
begin
|
|
|
|
text \<open>The Ground Sub-Message Patterns (GSMP)\<close>
|
|
definition GSMP::"('fun,'var) terms \<Rightarrow> ('fun,'var) terms" where
|
|
"GSMP P \<equiv> {t \<in> SMP P. fv t = {}}"
|
|
|
|
definition typing_cond where
|
|
"typing_cond \<A> \<equiv>
|
|
wf\<^sub>s\<^sub>t {} \<A> \<and>
|
|
fv\<^sub>s\<^sub>t \<A> \<inter> bvars\<^sub>s\<^sub>t \<A> = {} \<and>
|
|
tfr\<^sub>s\<^sub>t \<A> \<and>
|
|
wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>s\<^sub>t \<A>) \<and>
|
|
Ana_invar_subst (ik\<^sub>s\<^sub>t \<A> \<union> assignment_rhs\<^sub>s\<^sub>t \<A>)"
|
|
|
|
|
|
subsection \<open>Definitions: GSMP Disjointedness and Parallel Composability\<close>
|
|
definition GSMP_disjoint where
|
|
"GSMP_disjoint P1 P2 Secrets \<equiv> GSMP P1 \<inter> GSMP P2 \<subseteq> Secrets \<union> {m. {} \<turnstile>\<^sub>c m}"
|
|
|
|
definition declassified\<^sub>l\<^sub>s\<^sub>t where
|
|
"declassified\<^sub>l\<^sub>s\<^sub>t (\<A>::('fun,'var,'lbl) labeled_strand) \<I> \<equiv> {t. (\<star>, Receive t) \<in> set \<A>} \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>"
|
|
|
|
definition par_comp where
|
|
"par_comp (\<A>::('fun,'var,'lbl) labeled_strand) (Secrets::('fun,'var) terms) \<equiv>
|
|
(\<forall>l1 l2. l1 \<noteq> l2 \<longrightarrow> GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t l1 \<A>) (trms_proj\<^sub>l\<^sub>s\<^sub>t l2 \<A>) Secrets) \<and>
|
|
(\<forall>s \<in> Secrets. \<forall>s' \<in> subterms s. {} \<turnstile>\<^sub>c s' \<or> s' \<in> Secrets) \<and>
|
|
ground Secrets"
|
|
|
|
definition strand_leaks\<^sub>l\<^sub>s\<^sub>t where
|
|
"strand_leaks\<^sub>l\<^sub>s\<^sub>t \<A> Sec \<I> \<equiv> (\<exists>t \<in> Sec - declassified\<^sub>l\<^sub>s\<^sub>t \<A> \<I>. \<exists>l. (\<I> \<Turnstile> \<langle>proj_unl l \<A>@[Send t]\<rangle>))"
|
|
|
|
subsection \<open>Definitions: Homogeneous and Numbered Intruder Deduction Variants\<close>
|
|
|
|
definition proj_specific where
|
|
"proj_specific n t \<A> Secrets \<equiv> t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t n \<A>) - (Secrets \<union> {m. {} \<turnstile>\<^sub>c m})"
|
|
|
|
definition heterogeneous\<^sub>l\<^sub>s\<^sub>t where
|
|
"heterogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Secrets \<equiv> (
|
|
(\<exists>l1 l2. \<exists>s1 \<in> subterms t. \<exists>s2 \<in> subterms t.
|
|
l1 \<noteq> l2 \<and> proj_specific l1 s1 \<A> Secrets \<and> proj_specific l2 s2 \<A> Secrets))"
|
|
|
|
abbreviation homogeneous\<^sub>l\<^sub>s\<^sub>t where
|
|
"homogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Secrets \<equiv> \<not>heterogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Secrets"
|
|
|
|
definition intruder_deduct_hom::
|
|
"('fun,'var) terms \<Rightarrow> ('fun,'var,'lbl) labeled_strand \<Rightarrow> ('fun,'var) terms \<Rightarrow> ('fun,'var) term
|
|
\<Rightarrow> bool" ("\<langle>_;_;_\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m _" 50)
|
|
where
|
|
"\<langle>M; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m t \<equiv> \<langle>M; \<lambda>t. homogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Sec \<and> t \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)\<rangle> \<turnstile>\<^sub>r t"
|
|
|
|
lemma intruder_deduct_hom_AxiomH[simp]:
|
|
assumes "t \<in> M"
|
|
shows "\<langle>M; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m t"
|
|
using intruder_deduct_restricted.AxiomR[of t M] assms
|
|
unfolding intruder_deduct_hom_def
|
|
by blast
|
|
|
|
lemma intruder_deduct_hom_ComposeH[simp]:
|
|
assumes "length X = arity f" "public f" "\<And>x. x \<in> set X \<Longrightarrow> \<langle>M; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m x"
|
|
and "homogeneous\<^sub>l\<^sub>s\<^sub>t (Fun f X) \<A> Sec" "Fun f X \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
|
|
shows "\<langle>M; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m Fun f X"
|
|
proof -
|
|
let ?Q = "\<lambda>t. homogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Sec \<and> t \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
|
|
show ?thesis
|
|
using intruder_deduct_restricted.ComposeR[of X f M ?Q] assms
|
|
unfolding intruder_deduct_hom_def
|
|
by blast
|
|
qed
|
|
|
|
lemma intruder_deduct_hom_DecomposeH:
|
|
assumes "\<langle>M; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m t" "Ana t = (K, T)" "\<And>k. k \<in> set K \<Longrightarrow> \<langle>M; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m k" "t\<^sub>i \<in> set T"
|
|
shows "\<langle>M; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m t\<^sub>i"
|
|
proof -
|
|
let ?Q = "\<lambda>t. homogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Sec \<and> t \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
|
|
show ?thesis
|
|
using intruder_deduct_restricted.DecomposeR[of M ?Q t] assms
|
|
unfolding intruder_deduct_hom_def
|
|
by blast
|
|
qed
|
|
|
|
lemma intruder_deduct_hom_induct[consumes 1, case_names AxiomH ComposeH DecomposeH]:
|
|
assumes "\<langle>M; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m t" "\<And>t. t \<in> M \<Longrightarrow> P M t"
|
|
"\<And>X f. \<lbrakk>length X = arity f; public f;
|
|
\<And>x. x \<in> set X \<Longrightarrow> \<langle>M; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m x;
|
|
\<And>x. x \<in> set X \<Longrightarrow> P M x;
|
|
homogeneous\<^sub>l\<^sub>s\<^sub>t (Fun f X) \<A> Sec;
|
|
Fun f X \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)
|
|
\<rbrakk> \<Longrightarrow> P M (Fun f X)"
|
|
"\<And>t K T t\<^sub>i. \<lbrakk>\<langle>M; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m t; P M t; Ana t = (K, T);
|
|
\<And>k. k \<in> set K \<Longrightarrow> \<langle>M; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m 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"
|
|
proof -
|
|
let ?Q = "\<lambda>t. homogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Sec \<and> t \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
|
|
show ?thesis
|
|
using intruder_deduct_restricted_induct[of M ?Q t "\<lambda>M Q t. P M t"] assms
|
|
unfolding intruder_deduct_hom_def
|
|
by blast
|
|
qed
|
|
|
|
lemma ideduct_hom_mono:
|
|
"\<lbrakk>\<langle>M; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m t; M \<subseteq> M'\<rbrakk> \<Longrightarrow> \<langle>M'; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m t"
|
|
using ideduct_restricted_mono[of M _ t M']
|
|
unfolding intruder_deduct_hom_def
|
|
by fast
|
|
|
|
subsection \<open>Lemmata: GSMP\<close>
|
|
lemma GSMP_disjoint_empty[simp]:
|
|
"GSMP_disjoint {} A Sec" "GSMP_disjoint A {} Sec"
|
|
unfolding GSMP_disjoint_def GSMP_def by fastforce+
|
|
|
|
lemma GSMP_mono:
|
|
assumes "N \<subseteq> M"
|
|
shows "GSMP N \<subseteq> GSMP M"
|
|
using SMP_mono[OF assms] unfolding GSMP_def by fast
|
|
|
|
lemma GSMP_SMP_mono:
|
|
assumes "SMP N \<subseteq> SMP M"
|
|
shows "GSMP N \<subseteq> GSMP M"
|
|
using assms unfolding GSMP_def by fast
|
|
|
|
lemma GSMP_subterm:
|
|
assumes "t \<in> GSMP M" "t' \<sqsubseteq> t"
|
|
shows "t' \<in> GSMP M"
|
|
using SMP.Subterm[of t M t'] ground_subterm[of t t'] assms unfolding GSMP_def by auto
|
|
|
|
lemma GSMP_subterms: "subterms\<^sub>s\<^sub>e\<^sub>t (GSMP M) = GSMP M"
|
|
using GSMP_subterm[of _ M] by blast
|
|
|
|
lemma GSMP_Ana_key:
|
|
assumes "t \<in> GSMP M" "Ana t = (K,T)" "k \<in> set K"
|
|
shows "k \<in> GSMP M"
|
|
using SMP.Ana[of t M K T k] Ana_keys_fv[of t K T] assms unfolding GSMP_def by auto
|
|
|
|
lemma GSMP_append[simp]: "GSMP (trms\<^sub>l\<^sub>s\<^sub>t (A@B)) = GSMP (trms\<^sub>l\<^sub>s\<^sub>t A) \<union> GSMP (trms\<^sub>l\<^sub>s\<^sub>t B)"
|
|
using SMP_union[of "trms\<^sub>l\<^sub>s\<^sub>t A" "trms\<^sub>l\<^sub>s\<^sub>t B"] trms\<^sub>l\<^sub>s\<^sub>t_append[of A B] unfolding GSMP_def by auto
|
|
|
|
lemma GSMP_union: "GSMP (A \<union> B) = GSMP A \<union> GSMP B"
|
|
using SMP_union[of A B] unfolding GSMP_def by auto
|
|
|
|
lemma GSMP_Union: "GSMP (trms\<^sub>l\<^sub>s\<^sub>t A) = (\<Union>l. GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l A))"
|
|
proof -
|
|
define P where "P \<equiv> (\<lambda>l. trms_proj\<^sub>l\<^sub>s\<^sub>t l A)"
|
|
define Q where "Q \<equiv> trms\<^sub>l\<^sub>s\<^sub>t A"
|
|
have "SMP (\<Union>l. P l) = (\<Union>l. SMP (P l))" "Q = (\<Union>l. P l)"
|
|
unfolding P_def Q_def by (metis SMP_Union, metis trms\<^sub>l\<^sub>s\<^sub>t_union)
|
|
hence "GSMP Q = (\<Union>l. GSMP (P l))" unfolding GSMP_def by auto
|
|
thus ?thesis unfolding P_def Q_def by metis
|
|
qed
|
|
|
|
lemma in_GSMP_in_proj: "t \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t A) \<Longrightarrow> \<exists>n. t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t n A)"
|
|
using GSMP_Union[of A] by blast
|
|
|
|
lemma in_proj_in_GSMP: "t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t n A) \<Longrightarrow> t \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t A)"
|
|
using GSMP_Union[of A] by blast
|
|
|
|
lemma GSMP_disjointE:
|
|
assumes A: "GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t n A) (trms_proj\<^sub>l\<^sub>s\<^sub>t m A) Sec"
|
|
shows "GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t n A) \<inter> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t m A) \<subseteq> Sec \<union> {m. {} \<turnstile>\<^sub>c m}"
|
|
using assms unfolding GSMP_disjoint_def by auto
|
|
|
|
lemma GSMP_disjoint_term:
|
|
assumes "GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>) (trms_proj\<^sub>l\<^sub>s\<^sub>t l' \<A>) Sec"
|
|
shows "t \<notin> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>) \<or> t \<notin> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l' \<A>) \<or> t \<in> Sec \<or> {} \<turnstile>\<^sub>c t"
|
|
using assms unfolding GSMP_disjoint_def by blast
|
|
|
|
lemma GSMP_wt_subst_subset:
|
|
assumes "t \<in> GSMP (M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>)" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<I>)"
|
|
shows "t \<in> GSMP M"
|
|
using SMP_wt_subst_subset[OF _ assms(2,3), of t M] assms(1) unfolding GSMP_def by simp
|
|
|
|
lemma GSMP_wt_substI:
|
|
assumes "t \<in> M" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t I" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range I)" "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t I"
|
|
shows "t \<cdot> I \<in> GSMP M"
|
|
proof -
|
|
have "t \<in> SMP M" using assms(1) by auto
|
|
hence *: "t \<cdot> I \<in> SMP M" using SMP.Substitution assms(2,3) wf_trm_subst_range_iff[of I] by simp
|
|
moreover have "fv (t \<cdot> I) = {}"
|
|
using assms(1) interpretation_grounds_all'[OF assms(4)]
|
|
by auto
|
|
ultimately show ?thesis unfolding GSMP_def by simp
|
|
qed
|
|
|
|
lemma GSMP_disjoint_subset:
|
|
assumes "GSMP_disjoint L R S" "L' \<subseteq> L" "R' \<subseteq> R"
|
|
shows "GSMP_disjoint L' R' S"
|
|
using assms(1) SMP_mono[OF assms(2)] SMP_mono[OF assms(3)]
|
|
by (auto simp add: GSMP_def GSMP_disjoint_def)
|
|
|
|
lemma GSMP_disjoint_fst_specific_not_snd_specific:
|
|
assumes "GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>) (trms_proj\<^sub>l\<^sub>s\<^sub>t l' \<A>) Sec" "l \<noteq> l'"
|
|
and "proj_specific l m \<A> Sec"
|
|
shows "\<not>proj_specific l' m \<A> Sec"
|
|
using assms by (fastforce simp add: GSMP_disjoint_def proj_specific_def)
|
|
|
|
lemma GSMP_disjoint_snd_specific_not_fst_specific:
|
|
assumes "GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>) (trms_proj\<^sub>l\<^sub>s\<^sub>t l' \<A>) Sec"
|
|
and "proj_specific l' m \<A> Sec"
|
|
shows "\<not>proj_specific l m \<A> Sec"
|
|
using assms by (auto simp add: GSMP_disjoint_def proj_specific_def)
|
|
|
|
lemma GSMP_disjoint_intersection_not_specific:
|
|
assumes "GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>) (trms_proj\<^sub>l\<^sub>s\<^sub>t l' \<A>) Sec"
|
|
and "t \<in> Sec \<or> {} \<turnstile>\<^sub>c t"
|
|
shows "\<not>proj_specific l t \<A> Sec" "\<not>proj_specific l t \<A> Sec"
|
|
using assms by (auto simp add: GSMP_disjoint_def proj_specific_def)
|
|
|
|
subsection \<open>Lemmata: Intruder Knowledge and Declassification\<close>
|
|
lemma ik_proj_subst_GSMP_subset:
|
|
assumes I: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t I" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range I)" "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t I"
|
|
shows "ik\<^sub>s\<^sub>t (proj_unl n A) \<cdot>\<^sub>s\<^sub>e\<^sub>t I \<subseteq> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t n A)"
|
|
proof
|
|
fix t assume "t \<in> ik\<^sub>s\<^sub>t (proj_unl n A) \<cdot>\<^sub>s\<^sub>e\<^sub>t I"
|
|
hence *: "t \<in> trms_proj\<^sub>l\<^sub>s\<^sub>t n A \<cdot>\<^sub>s\<^sub>e\<^sub>t I" by auto
|
|
then obtain s where "s \<in> trms_proj\<^sub>l\<^sub>s\<^sub>t n A" "t = s \<cdot> I" by auto
|
|
hence "t \<in> SMP (trms_proj\<^sub>l\<^sub>s\<^sub>t n A)" using SMP_I I(1,2) wf_trm_subst_range_iff[of I] by simp
|
|
moreover have "fv t = {}"
|
|
using * interpretation_grounds_all'[OF I(3)]
|
|
by auto
|
|
ultimately show "t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t n A)" unfolding GSMP_def by simp
|
|
qed
|
|
|
|
lemma declassified_proj_ik_subset: "declassified\<^sub>l\<^sub>s\<^sub>t A I \<subseteq> ik\<^sub>s\<^sub>t (proj_unl n A) \<cdot>\<^sub>s\<^sub>e\<^sub>t I"
|
|
proof (induction A)
|
|
case (Cons a A) thus ?case
|
|
using proj_ik_append[of n "[a]" A] by (auto simp add: declassified\<^sub>l\<^sub>s\<^sub>t_def)
|
|
qed (simp add: declassified\<^sub>l\<^sub>s\<^sub>t_def)
|
|
|
|
lemma declassified_proj_GSMP_subset:
|
|
assumes I: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t I" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range I)" "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t I"
|
|
shows "declassified\<^sub>l\<^sub>s\<^sub>t A I \<subseteq> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t n A)"
|
|
by (rule subset_trans[OF declassified_proj_ik_subset ik_proj_subst_GSMP_subset[OF I]])
|
|
|
|
lemma declassified_subterms_proj_GSMP_subset:
|
|
assumes I: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t I" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range I)" "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t I"
|
|
shows "subterms\<^sub>s\<^sub>e\<^sub>t (declassified\<^sub>l\<^sub>s\<^sub>t A I) \<subseteq> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t n A)"
|
|
proof
|
|
fix t assume t: "t \<in> subterms\<^sub>s\<^sub>e\<^sub>t (declassified\<^sub>l\<^sub>s\<^sub>t A I)"
|
|
then obtain t' where t': "t' \<in> declassified\<^sub>l\<^sub>s\<^sub>t A I" "t \<sqsubseteq> t'" by moura
|
|
hence "t' \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t n A)" using declassified_proj_GSMP_subset[OF assms] by blast
|
|
thus "t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t n A)"
|
|
using SMP.Subterm[of t' "trms_proj\<^sub>l\<^sub>s\<^sub>t n A" t] ground_subterm[OF _ t'(2)] t'(2)
|
|
unfolding GSMP_def by fast
|
|
qed
|
|
|
|
lemma declassified_secrets_subset:
|
|
assumes A: "\<forall>n m. n \<noteq> m \<longrightarrow> GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t n A) (trms_proj\<^sub>l\<^sub>s\<^sub>t m A) Sec"
|
|
and I: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t I" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range I)" "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t I"
|
|
shows "declassified\<^sub>l\<^sub>s\<^sub>t A I \<subseteq> Sec \<union> {m. {} \<turnstile>\<^sub>c m}"
|
|
using declassified_proj_GSMP_subset[OF I] A at_least_2_labels
|
|
unfolding GSMP_disjoint_def by blast
|
|
|
|
lemma declassified_subterms_secrets_subset:
|
|
assumes A: "\<forall>n m. n \<noteq> m \<longrightarrow> GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t n A) (trms_proj\<^sub>l\<^sub>s\<^sub>t m A) Sec"
|
|
and I: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t I" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range I)" "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t I"
|
|
shows "subterms\<^sub>s\<^sub>e\<^sub>t (declassified\<^sub>l\<^sub>s\<^sub>t A I) \<subseteq> Sec \<union> {m. {} \<turnstile>\<^sub>c m}"
|
|
using declassified_subterms_proj_GSMP_subset[OF I, of A label_witness1]
|
|
declassified_subterms_proj_GSMP_subset[OF I, of A label_witness2]
|
|
A at_least_2_labels
|
|
unfolding GSMP_disjoint_def by fast
|
|
|
|
lemma declassified_proj_eq: "declassified\<^sub>l\<^sub>s\<^sub>t A I = declassified\<^sub>l\<^sub>s\<^sub>t (proj n A) I"
|
|
unfolding declassified\<^sub>l\<^sub>s\<^sub>t_def proj_def by auto
|
|
|
|
lemma declassified_append: "declassified\<^sub>l\<^sub>s\<^sub>t (A@B) I = declassified\<^sub>l\<^sub>s\<^sub>t A I \<union> declassified\<^sub>l\<^sub>s\<^sub>t B I"
|
|
unfolding declassified\<^sub>l\<^sub>s\<^sub>t_def by auto
|
|
|
|
lemma declassified_prefix_subset: "prefix A B \<Longrightarrow> declassified\<^sub>l\<^sub>s\<^sub>t A I \<subseteq> declassified\<^sub>l\<^sub>s\<^sub>t B I"
|
|
using declassified_append unfolding prefix_def by auto
|
|
|
|
subsection \<open>Lemmata: Homogeneous and Heterogeneous Terms\<close>
|
|
lemma proj_specific_secrets_anti_mono:
|
|
assumes "proj_specific l t \<A> Sec" "Sec' \<subseteq> Sec"
|
|
shows "proj_specific l t \<A> Sec'"
|
|
using assms unfolding proj_specific_def by fast
|
|
|
|
lemma heterogeneous_secrets_anti_mono:
|
|
assumes "heterogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Sec" "Sec' \<subseteq> Sec"
|
|
shows "heterogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Sec'"
|
|
using assms proj_specific_secrets_anti_mono unfolding heterogeneous\<^sub>l\<^sub>s\<^sub>t_def by metis
|
|
|
|
lemma homogeneous_secrets_mono:
|
|
assumes "homogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Sec'" "Sec' \<subseteq> Sec"
|
|
shows "homogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Sec"
|
|
using assms heterogeneous_secrets_anti_mono by blast
|
|
|
|
lemma heterogeneous_supterm:
|
|
assumes "heterogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Sec" "t \<sqsubseteq> t'"
|
|
shows "heterogeneous\<^sub>l\<^sub>s\<^sub>t t' \<A> Sec"
|
|
proof -
|
|
obtain l1 l2 s1 s2 where *:
|
|
"l1 \<noteq> l2"
|
|
"s1 \<sqsubseteq> t" "proj_specific l1 s1 \<A> Sec"
|
|
"s2 \<sqsubseteq> t" "proj_specific l2 s2 \<A> Sec"
|
|
using assms(1) unfolding heterogeneous\<^sub>l\<^sub>s\<^sub>t_def by moura
|
|
thus ?thesis
|
|
using term.order_trans[OF *(2) assms(2)] term.order_trans[OF *(4) assms(2)]
|
|
by (auto simp add: heterogeneous\<^sub>l\<^sub>s\<^sub>t_def)
|
|
qed
|
|
|
|
lemma homogeneous_subterm:
|
|
assumes "homogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Sec" "t' \<sqsubseteq> t"
|
|
shows "homogeneous\<^sub>l\<^sub>s\<^sub>t t' \<A> Sec"
|
|
by (metis assms heterogeneous_supterm)
|
|
|
|
lemma proj_specific_subterm:
|
|
assumes "t \<sqsubseteq> t'" "proj_specific l t' \<A> Sec"
|
|
shows "proj_specific l t \<A> Sec \<or> t \<in> Sec \<or> {} \<turnstile>\<^sub>c t"
|
|
using GSMP_subterm[OF _ assms(1)] assms(2) by (auto simp add: proj_specific_def)
|
|
|
|
lemma heterogeneous_term_is_Fun:
|
|
assumes "heterogeneous\<^sub>l\<^sub>s\<^sub>t t A S" shows "\<exists>f T. t = Fun f T"
|
|
using assms by (cases t) (auto simp add: GSMP_def heterogeneous\<^sub>l\<^sub>s\<^sub>t_def proj_specific_def)
|
|
|
|
lemma proj_specific_is_homogeneous:
|
|
assumes \<A>: "\<forall>l l'. l \<noteq> l' \<longrightarrow> GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>) (trms_proj\<^sub>l\<^sub>s\<^sub>t l' \<A>) Sec"
|
|
and t: "proj_specific l m \<A> Sec"
|
|
shows "homogeneous\<^sub>l\<^sub>s\<^sub>t m \<A> Sec"
|
|
proof
|
|
assume "heterogeneous\<^sub>l\<^sub>s\<^sub>t m \<A> Sec"
|
|
then obtain s l' where s: "s \<in> subterms m" "proj_specific l' s \<A> Sec" "l \<noteq> l'"
|
|
unfolding heterogeneous\<^sub>l\<^sub>s\<^sub>t_def by moura
|
|
hence "s \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)" "s \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l' \<A>)"
|
|
using t by (auto simp add: GSMP_def proj_specific_def)
|
|
hence "s \<in> Sec \<or> {} \<turnstile>\<^sub>c s"
|
|
using \<A> s(3) by (auto simp add: GSMP_disjoint_def)
|
|
thus False using s(2) by (auto simp add: proj_specific_def)
|
|
qed
|
|
|
|
lemma deduct_synth_homogeneous:
|
|
assumes "{} \<turnstile>\<^sub>c t"
|
|
shows "homogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Sec"
|
|
proof -
|
|
have "\<forall>s \<in> subterms t. {} \<turnstile>\<^sub>c s" using deduct_synth_subterm[OF assms] by auto
|
|
thus ?thesis unfolding heterogeneous\<^sub>l\<^sub>s\<^sub>t_def proj_specific_def by auto
|
|
qed
|
|
|
|
lemma GSMP_proj_is_homogeneous:
|
|
assumes "\<forall>l l'. l \<noteq> l' \<longrightarrow> GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t l A) (trms_proj\<^sub>l\<^sub>s\<^sub>t l' A) Sec"
|
|
and "t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l A)" "t \<notin> Sec"
|
|
shows "homogeneous\<^sub>l\<^sub>s\<^sub>t t A Sec"
|
|
proof
|
|
assume "heterogeneous\<^sub>l\<^sub>s\<^sub>t t A Sec"
|
|
then obtain s l' where s: "s \<in> subterms t" "proj_specific l' s A Sec" "l \<noteq> l'"
|
|
unfolding heterogeneous\<^sub>l\<^sub>s\<^sub>t_def by moura
|
|
hence "s \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l A)" "s \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l' A)"
|
|
using assms by (auto simp add: GSMP_def proj_specific_def)
|
|
hence "s \<in> Sec \<or> {} \<turnstile>\<^sub>c s" using assms(1) s(3) by (auto simp add: GSMP_disjoint_def)
|
|
thus False using s(2) by (auto simp add: proj_specific_def)
|
|
qed
|
|
|
|
lemma homogeneous_is_not_proj_specific:
|
|
assumes "homogeneous\<^sub>l\<^sub>s\<^sub>t m \<A> Sec"
|
|
shows "\<exists>l::'lbl. \<not>proj_specific l m \<A> Sec"
|
|
proof -
|
|
let ?P = "\<lambda>l s. proj_specific l s \<A> Sec"
|
|
have "\<forall>l1 l2. \<forall>s1\<in>subterms m. \<forall>s2\<in>subterms m. (l1 \<noteq> l2 \<longrightarrow> (\<not>?P l1 s1 \<or> \<not>?P l2 s2))"
|
|
using assms heterogeneous\<^sub>l\<^sub>s\<^sub>t_def by metis
|
|
then obtain l1 l2 where "l1 \<noteq> l2" "\<not>?P l1 m \<or> \<not>?P l2 m"
|
|
by (metis term.order_refl at_least_2_labels)
|
|
thus ?thesis by metis
|
|
qed
|
|
|
|
lemma secrets_are_homogeneous:
|
|
assumes "\<forall>s \<in> Sec. P s \<longrightarrow> (\<forall>s' \<in> subterms s. {} \<turnstile>\<^sub>c s' \<or> s' \<in> Sec)" "s \<in> Sec" "P s"
|
|
shows "homogeneous\<^sub>l\<^sub>s\<^sub>t s \<A> Sec"
|
|
using assms by (auto simp add: heterogeneous\<^sub>l\<^sub>s\<^sub>t_def proj_specific_def)
|
|
|
|
lemma GSMP_is_homogeneous:
|
|
assumes \<A>: "\<forall>l l'. l \<noteq> l' \<longrightarrow> GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>) (trms_proj\<^sub>l\<^sub>s\<^sub>t l' \<A>) Sec"
|
|
and t: "t \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)" "t \<notin> Sec"
|
|
shows "homogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Sec"
|
|
proof -
|
|
obtain n where n: "t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t n \<A>)" using in_GSMP_in_proj[OF t(1)] by moura
|
|
show ?thesis using GSMP_proj_is_homogeneous[OF \<A> n t(2)] by metis
|
|
qed
|
|
|
|
lemma GSMP_intersection_is_homogeneous:
|
|
assumes \<A>: "\<forall>l l'. l \<noteq> l' \<longrightarrow> GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>) (trms_proj\<^sub>l\<^sub>s\<^sub>t l' \<A>) Sec"
|
|
and t: "t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>) \<inter> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l' \<A>)" "l \<noteq> l'"
|
|
shows "homogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Sec"
|
|
proof -
|
|
define M where "M \<equiv> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)"
|
|
define M' where "M' \<equiv> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l' \<A>)"
|
|
|
|
have t_in: "t \<in> M \<inter> M'" "t \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
|
|
using t(1) in_proj_in_GSMP[of t _ \<A>]
|
|
unfolding M_def M'_def by blast+
|
|
|
|
have "M \<inter> M' \<subseteq> Sec \<union> {m. {} \<turnstile>\<^sub>c m}"
|
|
using \<A> GSMP_disjointE[of l \<A> l' Sec] t(2)
|
|
unfolding M_def M'_def by presburger
|
|
moreover have "subterms\<^sub>s\<^sub>e\<^sub>t (M \<inter> M') = M \<inter> M'"
|
|
using GSMP_subterms unfolding M_def M'_def by blast
|
|
ultimately have *: "subterms\<^sub>s\<^sub>e\<^sub>t (M \<inter> M') \<subseteq> Sec \<union> {m. {} \<turnstile>\<^sub>c m}"
|
|
by blast
|
|
|
|
show ?thesis
|
|
proof (cases "t \<in> Sec")
|
|
case True thus ?thesis
|
|
using * secrets_are_homogeneous[of Sec "\<lambda>t. t \<in> M \<inter> M'", OF _ _ t_in(1)]
|
|
by fast
|
|
qed (metis GSMP_is_homogeneous[OF \<A> t_in(2)])
|
|
qed
|
|
|
|
lemma GSMP_is_homogeneous':
|
|
assumes \<A>: "\<forall>l l'. l \<noteq> l' \<longrightarrow> GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>) (trms_proj\<^sub>l\<^sub>s\<^sub>t l' \<A>) Sec"
|
|
and t: "t \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
|
|
"t \<notin> Sec - \<Union>{GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l1 \<A>) \<inter> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l2 \<A>) | l1 l2. l1 \<noteq> l2}"
|
|
shows "homogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Sec"
|
|
using GSMP_is_homogeneous[OF \<A> t(1)] GSMP_intersection_is_homogeneous[OF \<A>] t(2)
|
|
by blast
|
|
|
|
lemma declassified_secrets_are_homogeneous:
|
|
assumes \<A>: "\<forall>l l'. l \<noteq> l' \<longrightarrow> GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>) (trms_proj\<^sub>l\<^sub>s\<^sub>t l' \<A>) Sec"
|
|
and \<I>: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<I>)" "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>"
|
|
and s: "s \<in> declassified\<^sub>l\<^sub>s\<^sub>t \<A> \<I>"
|
|
shows "homogeneous\<^sub>l\<^sub>s\<^sub>t s \<A> Sec"
|
|
proof -
|
|
have s_in: "s \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
|
|
using declassified_proj_GSMP_subset[OF \<I>, of \<A> label_witness1]
|
|
in_proj_in_GSMP[of s label_witness1 \<A>] s
|
|
by blast
|
|
|
|
show ?thesis
|
|
proof (cases "s \<in> Sec")
|
|
case True thus ?thesis
|
|
using declassified_subterms_secrets_subset[OF \<A> \<I>]
|
|
secrets_are_homogeneous[of Sec "\<lambda>s. s \<in> declassified\<^sub>l\<^sub>s\<^sub>t \<A> \<I>", OF _ _ s]
|
|
by fast
|
|
qed (metis GSMP_is_homogeneous[OF \<A> s_in])
|
|
qed
|
|
|
|
lemma Ana_keys_homogeneous:
|
|
assumes \<A>: "\<forall>l l'. l \<noteq> l' \<longrightarrow> GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>) (trms_proj\<^sub>l\<^sub>s\<^sub>t l' \<A>) Sec"
|
|
and t: "t \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
|
|
and k: "Ana t = (K,T)" "k \<in> set K"
|
|
"k \<notin> Sec - \<Union>{GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l1 \<A>) \<inter> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l2 \<A>) | l1 l2. l1 \<noteq> l2}"
|
|
shows "homogeneous\<^sub>l\<^sub>s\<^sub>t k \<A> Sec"
|
|
proof (cases "k \<in> \<Union>{GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l1 \<A>) \<inter> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l2 \<A>) | l1 l2. l1 \<noteq> l2}")
|
|
case False
|
|
hence "k \<notin> Sec" using k(3) by fast
|
|
moreover have "k \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
|
|
using t SMP.Ana[OF _ k(1,2)] Ana_keys_fv[OF k(1)] k(2)
|
|
unfolding GSMP_def by auto
|
|
ultimately show ?thesis using GSMP_is_homogeneous[OF \<A>, of k] by metis
|
|
qed (use GSMP_intersection_is_homogeneous[OF \<A>] in blast)
|
|
|
|
subsection \<open>Lemmata: Intruder Deduction Equivalences\<close>
|
|
lemma deduct_if_hom_deduct: "\<langle>M;A;S\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m m \<Longrightarrow> M \<turnstile> m"
|
|
using deduct_if_restricted_deduct unfolding intruder_deduct_hom_def by blast
|
|
|
|
lemma hom_deduct_if_hom_ik:
|
|
assumes "\<langle>M;A;Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m m" "\<forall>m \<in> M. homogeneous\<^sub>l\<^sub>s\<^sub>t m A Sec \<and> m \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t A)"
|
|
shows "homogeneous\<^sub>l\<^sub>s\<^sub>t m A Sec \<and> m \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t A)"
|
|
proof -
|
|
let ?Q = "\<lambda>m. homogeneous\<^sub>l\<^sub>s\<^sub>t m A Sec \<and> m \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t A)"
|
|
have "?Q t'" when "?Q t" "t' \<sqsubseteq> t" for t t'
|
|
using homogeneous_subterm[OF _ that(2)] GSMP_subterm[OF _ that(2)] that(1)
|
|
by blast
|
|
thus ?thesis
|
|
using assms(1) restricted_deduct_if_restricted_ik[OF _ assms(2)]
|
|
unfolding intruder_deduct_hom_def
|
|
by blast
|
|
qed
|
|
|
|
lemma deduct_hom_if_synth:
|
|
assumes hom: "homogeneous\<^sub>l\<^sub>s\<^sub>t m \<A> Sec" "m \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
|
|
and m: "M \<turnstile>\<^sub>c m"
|
|
shows "\<langle>M; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m m"
|
|
proof -
|
|
let ?Q = "\<lambda>m. homogeneous\<^sub>l\<^sub>s\<^sub>t m \<A> Sec \<and> m \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
|
|
have "?Q t'" when "?Q t" "t' \<sqsubseteq> t" for t t'
|
|
using homogeneous_subterm[OF _ that(2)] GSMP_subterm[OF _ that(2)] that(1)
|
|
by blast
|
|
thus ?thesis
|
|
using assms deduct_restricted_if_synth[of ?Q]
|
|
unfolding intruder_deduct_hom_def
|
|
by blast
|
|
qed
|
|
|
|
lemma hom_deduct_if_deduct:
|
|
assumes \<A>: "par_comp \<A> Sec"
|
|
and M: "\<forall>m\<in>M. homogeneous\<^sub>l\<^sub>s\<^sub>t m \<A> Sec \<and> m \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
|
|
and m: "M \<turnstile> m" "m \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
|
|
shows "\<langle>M; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m m"
|
|
proof -
|
|
let ?P = "\<lambda>x. homogeneous\<^sub>l\<^sub>s\<^sub>t x \<A> Sec \<and> x \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
|
|
|
|
have GSMP_hom: "homogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Sec" when "t \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)" for t
|
|
using \<A> GSMP_is_homogeneous[of \<A> Sec t]
|
|
secrets_are_homogeneous[of Sec "\<lambda>x. True" t \<A>] that
|
|
unfolding par_comp_def by blast
|
|
|
|
have P_Ana: "?P k" when "?P t" "Ana t = (K, T)" "k \<in> set K" for t K T k
|
|
using GSMP_Ana_key[OF _ that(2,3), of "trms\<^sub>l\<^sub>s\<^sub>t \<A>"] \<A> that GSMP_hom
|
|
by presburger
|
|
|
|
have P_subterm: "?P t'" when "?P t" "t' \<sqsubseteq> t" for t t'
|
|
using GSMP_subterm[of _ "trms\<^sub>l\<^sub>s\<^sub>t \<A>"] homogeneous_subterm[of _ \<A> Sec] that
|
|
by blast
|
|
|
|
have P_m: "?P m"
|
|
using GSMP_hom[OF m(2)] m(2)
|
|
by metis
|
|
|
|
show ?thesis
|
|
using restricted_deduct_if_deduct'[OF M _ _ m(1) P_m] P_Ana P_subterm
|
|
unfolding intruder_deduct_hom_def
|
|
by fast
|
|
qed
|
|
|
|
|
|
subsection \<open>Lemmata: Deduction Reduction of Parallel Composable Constraints\<close>
|
|
lemma par_comp_hom_deduct:
|
|
assumes \<A>: "par_comp \<A> Sec"
|
|
and M: "\<forall>l. \<forall>m \<in> M l. homogeneous\<^sub>l\<^sub>s\<^sub>t m \<A> Sec"
|
|
"\<forall>l. M l \<subseteq> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)"
|
|
"\<forall>l. Discl \<subseteq> M l"
|
|
"Discl \<subseteq> Sec \<union> {m. {} \<turnstile>\<^sub>c m}"
|
|
and Sec: "\<forall>l. \<forall>s \<in> Sec - Discl. \<not>(\<langle>M l; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m s)"
|
|
and t: "\<langle>\<Union>l. M l; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m t"
|
|
shows "t \<notin> Sec - Discl" (is ?A)
|
|
"\<forall>l. t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>) \<longrightarrow> \<langle>M l; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m t" (is ?B)
|
|
proof -
|
|
have M': "\<forall>l. \<forall>m \<in> M l. m \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
|
|
proof (intro allI ballI)
|
|
fix l m show "m \<in> M l \<Longrightarrow> m \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)" using M(2) in_proj_in_GSMP[of m l \<A>] by blast
|
|
qed
|
|
|
|
show ?A ?B using t
|
|
proof (induction t rule: intruder_deduct_hom_induct)
|
|
case (AxiomH t)
|
|
then obtain lt where t_in_proj_ik: "t \<in> M lt" by moura
|
|
show t_not_Sec: "t \<notin> Sec - Discl"
|
|
proof
|
|
assume "t \<in> Sec - Discl"
|
|
hence "\<forall>l. \<not>(\<langle>M l;\<A>;Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m t)" using Sec by auto
|
|
thus False using intruder_deduct_hom_AxiomH[OF t_in_proj_ik] by metis
|
|
qed
|
|
|
|
have 1: "\<forall>l. t \<in> M l \<longrightarrow> t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)"
|
|
using M(2,3) AxiomH by auto
|
|
|
|
have 3: "\<And>l1 l2. l1 \<noteq> l2 \<Longrightarrow> t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l1 \<A>) \<inter> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l2 \<A>)
|
|
\<Longrightarrow> {} \<turnstile>\<^sub>c t \<or> t \<in> Discl"
|
|
using \<A> t_not_Sec by (auto simp add: par_comp_def GSMP_disjoint_def)
|
|
|
|
have 4: "homogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Sec" "t \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)" using M(1) M' t_in_proj_ik by auto
|
|
|
|
{ fix l assume "t \<in> Discl"
|
|
hence "t \<in> M l" using M(3) by auto
|
|
hence "\<langle>M l; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m t" by auto
|
|
} hence 5: "\<forall>l. t \<in> Discl \<longrightarrow> \<langle>M l; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m t" by metis
|
|
|
|
show "\<forall>l. t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>) \<longrightarrow> \<langle>M l; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m t"
|
|
by (metis (lifting) Int_iff empty_subsetI
|
|
1 3 4 5 t_in_proj_ik
|
|
intruder_deduct_hom_AxiomH[of t _ \<A> Sec]
|
|
deduct_hom_if_synth[of t \<A> Sec "{}"]
|
|
ideduct_hom_mono[of "{}" \<A> Sec t])
|
|
next
|
|
case (ComposeH T f)
|
|
show "\<forall>l. Fun f T \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>) \<longrightarrow> \<langle>M l; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m Fun f T"
|
|
proof (intro allI impI)
|
|
fix l
|
|
assume "Fun f T \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)"
|
|
hence "\<And>t. t \<in> set T \<Longrightarrow> t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)"
|
|
using GSMP_subterm[OF _ subtermeqI''] by auto
|
|
thus "\<langle>M l; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m Fun f T"
|
|
using ComposeH.IH(2) intruder_deduct_hom_ComposeH[OF ComposeH.hyps(1,2) _ ComposeH.hyps(4,5)]
|
|
by simp
|
|
qed
|
|
thus "Fun f T \<notin> Sec - Discl"
|
|
using Sec ComposeH.hyps(5) trms\<^sub>l\<^sub>s\<^sub>t_union[of \<A>] GSMP_Union[of \<A>]
|
|
by (metis (no_types, lifting) UN_iff)
|
|
next
|
|
case (DecomposeH t K T t\<^sub>i)
|
|
have ti_subt: "t\<^sub>i \<sqsubseteq> t" using Ana_subterm[OF DecomposeH.hyps(2)] \<open>t\<^sub>i \<in> set T\<close> by auto
|
|
have t: "homogeneous\<^sub>l\<^sub>s\<^sub>t t \<A> Sec" "t \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
|
|
using DecomposeH.hyps(1) hom_deduct_if_hom_ik M(1) M'
|
|
by auto
|
|
have ti: "homogeneous\<^sub>l\<^sub>s\<^sub>t t\<^sub>i \<A> Sec" "t\<^sub>i \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
|
|
using intruder_deduct_hom_DecomposeH[OF DecomposeH.hyps] hom_deduct_if_hom_ik M(1) M' by auto
|
|
{ fix l assume *: "t\<^sub>i \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)" "t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)"
|
|
hence "\<And>k. k \<in> set K \<Longrightarrow> \<langle>M l;\<A>;Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m k"
|
|
using GSMP_Ana_key[OF _ DecomposeH.hyps(2)] DecomposeH.IH(4) by auto
|
|
hence "\<langle>M l;\<A>;Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m t\<^sub>i" "t\<^sub>i \<notin> Sec - Discl"
|
|
using Sec DecomposeH.IH(2) *(2)
|
|
intruder_deduct_hom_DecomposeH[OF _ DecomposeH.hyps(2) _ \<open>t\<^sub>i \<in> set T\<close>]
|
|
by force+
|
|
} moreover {
|
|
fix l1 l2 assume *: "t\<^sub>i \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l1 \<A>)" "t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l2 \<A>)" "l1 \<noteq> l2"
|
|
have "GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t l1 \<A>) (trms_proj\<^sub>l\<^sub>s\<^sub>t l2 \<A>) Sec"
|
|
using *(3) \<A> by (simp add: par_comp_def)
|
|
hence "t\<^sub>i \<in> Sec \<union> {m. {} \<turnstile>\<^sub>c m}"
|
|
using GSMP_subterm[OF *(2) ti_subt] *(1) by (auto simp add: GSMP_disjoint_def)
|
|
moreover have "\<And>k. k \<in> set K \<Longrightarrow> \<langle>M l2;\<A>;Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m k"
|
|
using *(2) GSMP_Ana_key[OF _ DecomposeH.hyps(2)] DecomposeH.IH(4) by auto
|
|
ultimately have "t\<^sub>i \<notin> Sec - Discl" "{} \<turnstile>\<^sub>c t\<^sub>i \<or> t\<^sub>i \<in> Discl"
|
|
using Sec DecomposeH.IH(2) *(2)
|
|
intruder_deduct_hom_DecomposeH[OF _ DecomposeH.hyps(2) _ \<open>t\<^sub>i \<in> set T\<close>]
|
|
by (metis (lifting), metis (no_types, lifting) DiffI Un_iff mem_Collect_eq)
|
|
hence "\<langle>M l1;\<A>;Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m t\<^sub>i" "\<langle>M l2;\<A>;Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m t\<^sub>i" "t\<^sub>i \<notin> Sec - Discl"
|
|
using M(3,4) deduct_hom_if_synth[THEN ideduct_hom_mono] ti
|
|
by (meson intruder_deduct_hom_AxiomH empty_subsetI subsetCE)+
|
|
} moreover have
|
|
"\<exists>l. t\<^sub>i \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)"
|
|
"\<exists>l. t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)"
|
|
using in_GSMP_in_proj[of _ \<A>] ti(2) t(2) by presburger+
|
|
ultimately show
|
|
"t\<^sub>i \<notin> Sec - Discl"
|
|
"\<forall>l. t\<^sub>i \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>) \<longrightarrow> \<langle>M l; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m t\<^sub>i"
|
|
by (metis (no_types, lifting))+
|
|
qed
|
|
qed
|
|
|
|
lemma par_comp_deduct_proj:
|
|
assumes \<A>: "par_comp \<A> Sec"
|
|
and M: "\<forall>l. \<forall>m\<in>M l. homogeneous\<^sub>l\<^sub>s\<^sub>t m \<A> Sec"
|
|
"\<forall>l. M l \<subseteq> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)"
|
|
"\<forall>l. Discl \<subseteq> M l"
|
|
and t: "(\<Union>l. M l) \<turnstile> t" "t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)"
|
|
and Discl: "Discl \<subseteq> Sec \<union> {m. {} \<turnstile>\<^sub>c m}"
|
|
shows "M l \<turnstile> t \<or> (\<exists>s \<in> Sec - Discl. \<exists>l. M l \<turnstile> s)"
|
|
using t
|
|
proof (induction t rule: intruder_deduct_induct)
|
|
case (Axiom t)
|
|
then obtain l' where t_in_ik_proj: "t \<in> M l'" by moura
|
|
show ?case
|
|
proof (cases "t \<in> Sec - Discl \<or> {} \<turnstile>\<^sub>c t")
|
|
case True
|
|
note T = True
|
|
show ?thesis
|
|
proof (cases "t \<in> Sec - Discl")
|
|
case True thus ?thesis using intruder_deduct.Axiom[OF t_in_ik_proj] by metis
|
|
next
|
|
case False thus ?thesis using T ideduct_mono[of "{}" t] by auto
|
|
qed
|
|
next
|
|
case False
|
|
hence "t \<notin> Sec - Discl" "\<not>{} \<turnstile>\<^sub>c t" "t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)" using Axiom by auto
|
|
hence "(\<forall>l'. l \<noteq> l' \<longrightarrow> t \<notin> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l' \<A>)) \<or> t \<in> Discl"
|
|
using \<A> unfolding GSMP_disjoint_def par_comp_def by auto
|
|
hence "(\<forall>l'. l \<noteq> l' \<longrightarrow> t \<notin> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l' \<A>)) \<or> t \<in> M l \<or> {} \<turnstile>\<^sub>c t" using M by auto
|
|
thus ?thesis using Axiom deduct_if_synth[THEN ideduct_mono] t_in_ik_proj
|
|
by (metis (no_types, lifting) False M(2) intruder_deduct.Axiom subsetCE)
|
|
qed
|
|
next
|
|
case (Compose T f)
|
|
hence "Fun f T \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)" using Compose.prems by auto
|
|
hence "\<And>t. t \<in> set T \<Longrightarrow> t \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)" unfolding GSMP_def by auto
|
|
hence IH: "\<And>t. t \<in> set T \<Longrightarrow> M l \<turnstile> t \<or> (\<exists>s \<in> Sec - Discl. \<exists>l. M l \<turnstile> s)"
|
|
using Compose.IH by auto
|
|
show ?case
|
|
proof (cases "\<forall>t \<in> set T. M l \<turnstile> t")
|
|
case True thus ?thesis by (metis intruder_deduct.Compose[OF Compose.hyps(1,2)])
|
|
qed (metis IH)
|
|
next
|
|
case (Decompose t K T t\<^sub>i)
|
|
have hom_ik: "\<forall>l. \<forall>m\<in>M l. homogeneous\<^sub>l\<^sub>s\<^sub>t m \<A> Sec \<and> m \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
|
|
proof (intro allI ballI conjI)
|
|
fix l m assume m: "m \<in> M l"
|
|
thus "homogeneous\<^sub>l\<^sub>s\<^sub>t m \<A> Sec" using M(1) by simp
|
|
show "m \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)" using in_proj_in_GSMP[of m l \<A>] M(2) m by blast
|
|
qed
|
|
|
|
have par_comp_unfold:
|
|
"\<forall>l1 l2. l1 \<noteq> l2 \<longrightarrow> GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t l1 \<A>) (trms_proj\<^sub>l\<^sub>s\<^sub>t l2 \<A>) Sec"
|
|
using \<A> by (auto simp add: par_comp_def)
|
|
|
|
note ti_GSMP = in_proj_in_GSMP[OF Decompose.prems(1)]
|
|
|
|
have "\<langle>\<Union>l. M l; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m t\<^sub>i"
|
|
using intruder_deduct.Decompose[OF Decompose.hyps]
|
|
hom_deduct_if_deduct[OF \<A>, of "\<Union>l. M l"] hom_ik ti_GSMP (* ti_hom *)
|
|
by blast
|
|
hence "(\<langle>M l; \<A>; Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m t\<^sub>i) \<or> (\<exists>s \<in> Sec-Discl. \<exists>l. \<langle>M l;\<A>;Sec\<rangle> \<turnstile>\<^sub>h\<^sub>o\<^sub>m s)"
|
|
using par_comp_hom_deduct(2)[OF \<A> M Discl(1)] Decompose.prems(1)
|
|
by blast
|
|
thus ?case using deduct_if_hom_deduct[of _ \<A> Sec] by auto
|
|
qed
|
|
|
|
|
|
subsection \<open>Theorem: Parallel Compositionality for Labeled Constraints\<close>
|
|
lemma par_comp_prefix: assumes "par_comp (A@B) M" shows "par_comp A M"
|
|
proof -
|
|
let ?L = "\<lambda>l. trms_proj\<^sub>l\<^sub>s\<^sub>t l A \<union> trms_proj\<^sub>l\<^sub>s\<^sub>t l B"
|
|
have "\<forall>l1 l2. l1 \<noteq> l2 \<longrightarrow> GSMP_disjoint (?L l1) (?L l2) M"
|
|
using assms unfolding par_comp_def
|
|
by (metis trms\<^sub>s\<^sub>t_append proj_append(2) unlabel_append)
|
|
hence "\<forall>l1 l2. l1 \<noteq> l2 \<longrightarrow> GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t l1 A) (trms_proj\<^sub>l\<^sub>s\<^sub>t l2 A) M"
|
|
using SMP_union by (auto simp add: GSMP_def GSMP_disjoint_def)
|
|
thus ?thesis using assms unfolding par_comp_def by blast
|
|
qed
|
|
|
|
theorem par_comp_constr_typed:
|
|
assumes \<A>: "par_comp \<A> Sec"
|
|
and \<I>: "\<I> \<Turnstile> \<langle>unlabel \<A>\<rangle>" "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<I>)"
|
|
shows "(\<forall>l. (\<I> \<Turnstile> \<langle>proj_unl l \<A>\<rangle>)) \<or> (\<exists>\<A>'. prefix \<A>' \<A> \<and> (strand_leaks\<^sub>l\<^sub>s\<^sub>t \<A>' Sec \<I>))"
|
|
proof -
|
|
let ?L = "\<lambda>\<A>'. \<exists>t \<in> Sec - declassified\<^sub>l\<^sub>s\<^sub>t \<A>' \<I>. \<exists>l. \<lbrakk>{}; proj_unl l \<A>'@[Send t]\<rbrakk>\<^sub>d \<I>"
|
|
have "\<lbrakk>{}; unlabel \<A>\<rbrakk>\<^sub>d \<I>" using \<I> by (simp add: constr_sem_d_def)
|
|
with \<A> have "(\<forall>l. \<lbrakk>{}; proj_unl l \<A>\<rbrakk>\<^sub>d \<I>) \<or> (\<exists>\<A>'. prefix \<A>' \<A> \<and> ?L \<A>')"
|
|
proof (induction "unlabel \<A>" arbitrary: \<A> rule: List.rev_induct)
|
|
case Nil
|
|
hence "\<A> = []" using unlabel_nil_only_if_nil by simp
|
|
thus ?case by auto
|
|
next
|
|
case (snoc b B \<A>)
|
|
hence disj: "\<forall>l1 l2. l1 \<noteq> l2 \<longrightarrow> GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t l1 \<A>) (trms_proj\<^sub>l\<^sub>s\<^sub>t l2 \<A>) Sec"
|
|
by (auto simp add: par_comp_def)
|
|
|
|
obtain a A n where a: "\<A> = A@[a]" "a = (ln n, b) \<or> a = (\<star>, b)"
|
|
using unlabel_snoc_inv[OF snoc.hyps(2)[symmetric]] by moura
|
|
hence A: "\<A> = A@[(ln n, b)] \<or> \<A> = A@[(\<star>, b)]" by metis
|
|
|
|
have 1: "B = unlabel A" using a snoc.hyps(2) unlabel_append[of A "[a]"] by auto
|
|
have 2: "par_comp A Sec" using par_comp_prefix snoc.prems(1) a by metis
|
|
have 3: "\<lbrakk>{}; unlabel A\<rbrakk>\<^sub>d \<I>" by (metis 1 snoc.prems(2) snoc.hyps(2) strand_sem_split(3))
|
|
have IH: "(\<forall>l. \<lbrakk>{}; proj_unl l A\<rbrakk>\<^sub>d \<I>) \<or> (\<exists>\<A>'. prefix \<A>' A \<and> ?L \<A>')"
|
|
by (rule snoc.hyps(1)[OF 1 2 3])
|
|
|
|
show ?case
|
|
proof (cases "\<forall>l. \<lbrakk>{}; proj_unl l A\<rbrakk>\<^sub>d \<I>")
|
|
case False
|
|
then obtain \<A>' where \<A>': "prefix \<A>' A" "?L \<A>'" by (metis IH)
|
|
hence "prefix \<A>' (A@[a])" using a prefix_prefix[of _ A "[a]"] by simp
|
|
thus ?thesis using \<A>'(2) a by auto
|
|
next
|
|
case True
|
|
note IH' = True
|
|
show ?thesis
|
|
proof (cases b)
|
|
case (Send t)
|
|
hence "ik\<^sub>s\<^sub>t (unlabel A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> t \<cdot> \<I>"
|
|
using a \<open>\<lbrakk>{}; unlabel \<A>\<rbrakk>\<^sub>d \<I>\<close> strand_sem_split(2)[of "{}" "unlabel A" "unlabel [a]" \<I>]
|
|
unlabel_append[of A "[a]"]
|
|
by auto
|
|
hence *: "(\<Union>l. (ik\<^sub>s\<^sub>t (proj_unl l A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>)) \<turnstile> t \<cdot> \<I>"
|
|
using proj_ik_union_is_unlabel_ik image_UN by metis
|
|
|
|
have "ik\<^sub>s\<^sub>t (proj_unl l \<A>) = ik\<^sub>s\<^sub>t (proj_unl l A)" for l
|
|
using Send A
|
|
by (metis append_Nil2 ik\<^sub>s\<^sub>t.simps(3) proj_unl_cons(3) proj_nil(2)
|
|
singleton_lst_proj(1,2) proj_ik_append)
|
|
hence **: "ik\<^sub>s\<^sub>t (proj_unl l A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<subseteq> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)" for l
|
|
using ik_proj_subst_GSMP_subset[OF \<I>(3,4,2), of _ \<A>]
|
|
by auto
|
|
|
|
note Discl =
|
|
declassified_proj_ik_subset[of A \<I>]
|
|
declassified_proj_GSMP_subset[OF \<I>(3,4,2), of A]
|
|
declassified_secrets_subset[OF disj \<I>(3,4,2)]
|
|
declassified_append[of A "[a]" \<I>]
|
|
|
|
have Sec: "ground Sec"
|
|
using \<A> by (auto simp add: par_comp_def)
|
|
|
|
have "\<forall>m\<in>ik\<^sub>s\<^sub>t (proj_unl l \<A>) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>. homogeneous\<^sub>l\<^sub>s\<^sub>t m \<A> Sec \<or> m \<in> Sec-declassified\<^sub>l\<^sub>s\<^sub>t A \<I>"
|
|
"\<forall>m\<in>ik\<^sub>s\<^sub>t (proj_unl l \<A>) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>. m \<in> GSMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
|
|
"ik\<^sub>s\<^sub>t (proj_unl l \<A>) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<subseteq> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)"
|
|
for l
|
|
using declassified_secrets_are_homogeneous[OF disj \<I>(3,4,2)]
|
|
GSMP_proj_is_homogeneous[OF disj]
|
|
ik_proj_subst_GSMP_subset[OF \<I>(3,4,2), of _ \<A>]
|
|
apply (metis (no_types, lifting) Diff_iff Discl(4) UnCI a(1) subsetCE)
|
|
using ik_proj_subst_GSMP_subset[OF \<I>(3,4,2), of _ \<A>]
|
|
GSMP_Union[of \<A>]
|
|
by auto
|
|
moreover have "ik\<^sub>s\<^sub>t (proj_unl l [a]) = {}" for l
|
|
using Send proj_ik\<^sub>s\<^sub>t_is_proj_rcv_set[of _ "[a]"] a(2) by auto
|
|
ultimately have M:
|
|
"\<forall>l. \<forall>m\<in>ik\<^sub>s\<^sub>t (proj_unl l A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>. homogeneous\<^sub>l\<^sub>s\<^sub>t m \<A> Sec \<or> m \<in> Sec-declassified\<^sub>l\<^sub>s\<^sub>t A \<I>"
|
|
"\<forall>l. ik\<^sub>s\<^sub>t (proj_unl l A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<subseteq> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)"
|
|
using a(1) proj_ik_append[of _ A "[a]"] by auto
|
|
|
|
have prefix_A: "prefix A \<A>" using A by auto
|
|
|
|
have "s \<cdot> \<I> = s"
|
|
when "s \<in> Sec" for s
|
|
using that Sec by auto
|
|
hence leakage_case: "\<lbrakk>{}; proj_unl l A@[Send s]\<rbrakk>\<^sub>d \<I>"
|
|
when "s \<in> Sec - declassified\<^sub>l\<^sub>s\<^sub>t A \<I>" "ik\<^sub>s\<^sub>t (proj_unl l A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> s" for l s
|
|
using that strand_sem_append(2) IH' by auto
|
|
|
|
have proj_deduct_case_n:
|
|
"\<forall>m. m \<noteq> n \<longrightarrow> \<lbrakk>{}; proj_unl m (A@[a])\<rbrakk>\<^sub>d \<I>"
|
|
"ik\<^sub>s\<^sub>t (proj_unl n A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> t \<cdot> \<I> \<Longrightarrow> \<lbrakk>{}; proj_unl n (A@[a])\<rbrakk>\<^sub>d \<I>"
|
|
when "a = (ln n, Send t)"
|
|
using that IH' proj_append(2)[of _ A]
|
|
by auto
|
|
|
|
have proj_deduct_case_star:
|
|
"\<lbrakk>{}; proj_unl l (A@[a])\<rbrakk>\<^sub>d \<I>"
|
|
when "a = (\<star>, Send t)" "ik\<^sub>s\<^sub>t (proj_unl l A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> t \<cdot> \<I>" for l
|
|
using that IH' proj_append(2)[of _ A]
|
|
by auto
|
|
|
|
show ?thesis
|
|
proof (cases "\<exists>l. \<exists>m \<in> ik\<^sub>s\<^sub>t (proj_unl l A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>. m \<in> Sec - declassified\<^sub>l\<^sub>s\<^sub>t A \<I>")
|
|
case True
|
|
then obtain l s where ls: "s \<in> Sec - declassified\<^sub>l\<^sub>s\<^sub>t A \<I>" "ik\<^sub>s\<^sub>t (proj_unl l A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> s"
|
|
using intruder_deduct.Axiom by metis
|
|
thus ?thesis using leakage_case prefix_A by blast
|
|
next
|
|
case False
|
|
hence M': "\<forall>l. \<forall>m\<in>ik\<^sub>s\<^sub>t (proj_unl l A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>. homogeneous\<^sub>l\<^sub>s\<^sub>t m \<A> Sec" using M(1) by blast
|
|
|
|
note deduct_proj_lemma =
|
|
par_comp_deduct_proj[OF snoc.prems(1) M' M(2) _ *, of "declassified\<^sub>l\<^sub>s\<^sub>t A \<I>" n]
|
|
|
|
from a(2) show ?thesis
|
|
proof
|
|
assume "a = (ln n, b)"
|
|
hence "a = (ln n, Send t)" "t \<cdot> \<I> \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t n \<A>)"
|
|
using Send a(1) trms_proj\<^sub>l\<^sub>s\<^sub>t_append[of n A "[a]"]
|
|
GSMP_wt_substI[OF _ \<I>(3,4,2)]
|
|
by (metis, force)
|
|
hence
|
|
"a = (ln n, Send t)"
|
|
"\<forall>m. m \<noteq> n \<longrightarrow> \<lbrakk>{}; proj_unl m (A@[a])\<rbrakk>\<^sub>d \<I>"
|
|
"ik\<^sub>s\<^sub>t (proj_unl n A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> t \<cdot> \<I> \<Longrightarrow> \<lbrakk>{}; proj_unl n (A@[a])\<rbrakk>\<^sub>d \<I>"
|
|
"t \<cdot> \<I> \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t n \<A>)"
|
|
using proj_deduct_case_n
|
|
by auto
|
|
hence "(\<forall>l. \<lbrakk>{}; proj_unl l \<A>\<rbrakk>\<^sub>d \<I>) \<or>
|
|
(\<exists>s \<in> Sec-declassified\<^sub>l\<^sub>s\<^sub>t A \<I>. \<exists>l. ik\<^sub>s\<^sub>t (proj_unl l A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> s)"
|
|
using deduct_proj_lemma A a Discl
|
|
by fast
|
|
thus ?thesis using leakage_case prefix_A by metis
|
|
next
|
|
assume "a = (\<star>, b)"
|
|
hence ***: "a = (\<star>, Send t)" "t \<cdot> \<I> \<in> GSMP (trms_proj\<^sub>l\<^sub>s\<^sub>t l \<A>)" for l
|
|
using Send a(1) GSMP_wt_substI[OF _ \<I>(3,4,2)]
|
|
by (metis, force)
|
|
hence "t \<cdot> \<I> \<in> Sec - declassified\<^sub>l\<^sub>s\<^sub>t A \<I> \<or>
|
|
t \<cdot> \<I> \<in> declassified\<^sub>l\<^sub>s\<^sub>t A \<I> \<or>
|
|
t \<cdot> \<I> \<in> {m. {} \<turnstile>\<^sub>c m}"
|
|
using snoc.prems(1) a(1) at_least_2_labels
|
|
unfolding par_comp_def GSMP_disjoint_def
|
|
by blast
|
|
thus ?thesis
|
|
proof (elim disjE)
|
|
assume "t \<cdot> \<I> \<in> Sec - declassified\<^sub>l\<^sub>s\<^sub>t A \<I>"
|
|
hence "\<exists>s \<in> Sec - declassified\<^sub>l\<^sub>s\<^sub>t A \<I>. \<exists>l. ik\<^sub>s\<^sub>t (proj_unl l A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> s"
|
|
using deduct_proj_lemma ***(2) A a Discl
|
|
by blast
|
|
thus ?thesis using prefix_A leakage_case by blast
|
|
next
|
|
assume "t \<cdot> \<I> \<in> declassified\<^sub>l\<^sub>s\<^sub>t A \<I>"
|
|
hence "ik\<^sub>s\<^sub>t (proj_unl l A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> t \<cdot> \<I>" for l
|
|
using intruder_deduct.Axiom Discl(1) by blast
|
|
thus ?thesis using proj_deduct_case_star[OF ***(1)] a(1) by fast
|
|
next
|
|
assume "t \<cdot> \<I> \<in> {m. {} \<turnstile>\<^sub>c m}"
|
|
hence "M \<turnstile> t \<cdot> \<I>" for M using ideduct_mono[OF deduct_if_synth] by blast
|
|
thus ?thesis using IH' a(1) ***(1) by fastforce
|
|
qed
|
|
qed
|
|
qed
|
|
next
|
|
case (Receive t)
|
|
hence "\<lbrakk>{}; proj_unl l \<A>\<rbrakk>\<^sub>d \<I>" for l
|
|
using IH' a proj_append(2)[of l A "[a]"]
|
|
unfolding unlabel_def proj_def by auto
|
|
thus ?thesis by metis
|
|
next
|
|
case (Equality ac t t')
|
|
hence *: "\<lbrakk>M; [Equality ac t t']\<rbrakk>\<^sub>d \<I>" for M
|
|
using a \<open>\<lbrakk>{}; unlabel \<A>\<rbrakk>\<^sub>d \<I>\<close> unlabel_append[of A "[a]"]
|
|
by auto
|
|
show ?thesis
|
|
using a proj_append(2)[of _ A "[a]"] Equality
|
|
strand_sem_append(2)[OF _ *] IH'
|
|
unfolding unlabel_def proj_def by auto
|
|
next
|
|
case (Inequality X F)
|
|
hence *: "\<lbrakk>M; [Inequality X F]\<rbrakk>\<^sub>d \<I>" for M
|
|
using a \<open>\<lbrakk>{}; unlabel \<A>\<rbrakk>\<^sub>d \<I>\<close> unlabel_append[of A "[a]"]
|
|
by auto
|
|
show ?thesis
|
|
using a proj_append(2)[of _ A "[a]"] Inequality
|
|
strand_sem_append(2)[OF _ *] IH'
|
|
unfolding unlabel_def proj_def by auto
|
|
qed
|
|
qed
|
|
qed
|
|
thus ?thesis using \<I>(1) unfolding strand_leaks\<^sub>l\<^sub>s\<^sub>t_def by (simp add: constr_sem_d_def)
|
|
qed
|
|
|
|
theorem par_comp_constr:
|
|
assumes \<A>: "par_comp \<A> Sec" "typing_cond (unlabel \<A>)"
|
|
and \<I>: "\<I> \<Turnstile> \<langle>unlabel \<A>\<rangle>" "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>"
|
|
shows "\<exists>\<I>\<^sub>\<tau>. interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>\<^sub>\<tau> \<and> wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>\<^sub>\<tau> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<I>\<^sub>\<tau>) \<and> (\<I>\<^sub>\<tau> \<Turnstile> \<langle>unlabel \<A>\<rangle>) \<and>
|
|
((\<forall>l. (\<I>\<^sub>\<tau> \<Turnstile> \<langle>proj_unl l \<A>\<rangle>)) \<or> (\<exists>\<A>'. prefix \<A>' \<A> \<and> (strand_leaks\<^sub>l\<^sub>s\<^sub>t \<A>' Sec \<I>\<^sub>\<tau>)))"
|
|
proof -
|
|
from \<A>(2) have *:
|
|
"wf\<^sub>s\<^sub>t {} (unlabel \<A>)"
|
|
"fv\<^sub>s\<^sub>t (unlabel \<A>) \<inter> bvars\<^sub>s\<^sub>t (unlabel \<A>) = {}"
|
|
"tfr\<^sub>s\<^sub>t (unlabel \<A>)"
|
|
"wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>s\<^sub>t (unlabel \<A>))"
|
|
"Ana_invar_subst (ik\<^sub>s\<^sub>t (unlabel \<A>) \<union> assignment_rhs\<^sub>s\<^sub>t (unlabel \<A>))"
|
|
unfolding typing_cond_def tfr\<^sub>s\<^sub>t_def by metis+
|
|
|
|
obtain \<I>\<^sub>\<tau> where \<I>\<^sub>\<tau>: "\<I>\<^sub>\<tau> \<Turnstile> \<langle>unlabel \<A>\<rangle>" "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>\<^sub>\<tau>" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>\<^sub>\<tau>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<I>\<^sub>\<tau>)"
|
|
using wt_attack_if_tfr_attack_d[OF * \<I>(2,1)] by metis
|
|
|
|
show ?thesis using par_comp_constr_typed[OF \<A>(1) \<I>\<^sub>\<tau>] \<I>\<^sub>\<tau> by auto
|
|
qed
|
|
|
|
|
|
subsection \<open>Theorem: Parallel Compositionality for Labeled Protocols\<close>
|
|
subsubsection \<open>Definitions: Labeled Protocols\<close>
|
|
text \<open>
|
|
We state our result on the level of protocol traces (i.e., the constraints reachable in a
|
|
symbolic execution of the actual protocol). Hence, we do not need to convert protocol strands
|
|
to intruder constraints in the following well-formedness definitions.
|
|
\<close>
|
|
definition wf\<^sub>l\<^sub>s\<^sub>t\<^sub>s::"('fun,'var,'lbl) labeled_strand set \<Rightarrow> bool" where
|
|
"wf\<^sub>l\<^sub>s\<^sub>t\<^sub>s \<S> \<equiv> (\<forall>\<A> \<in> \<S>. wf\<^sub>l\<^sub>s\<^sub>t {} \<A>) \<and> (\<forall>\<A> \<in> \<S>. \<forall>\<A>' \<in> \<S>. fv\<^sub>l\<^sub>s\<^sub>t \<A> \<inter> bvars\<^sub>l\<^sub>s\<^sub>t \<A>' = {})"
|
|
|
|
definition wf\<^sub>l\<^sub>s\<^sub>t\<^sub>s'::"('fun,'var,'lbl) labeled_strand set \<Rightarrow> ('fun,'var,'lbl) labeled_strand \<Rightarrow> bool"
|
|
where
|
|
"wf\<^sub>l\<^sub>s\<^sub>t\<^sub>s' \<S> \<A> \<equiv> (\<forall>\<A>' \<in> \<S>. wf\<^sub>s\<^sub>t (wfrestrictedvars\<^sub>l\<^sub>s\<^sub>t \<A>) (unlabel \<A>')) \<and>
|
|
(\<forall>\<A>' \<in> \<S>. \<forall>\<A>'' \<in> \<S>. fv\<^sub>l\<^sub>s\<^sub>t \<A>' \<inter> bvars\<^sub>l\<^sub>s\<^sub>t \<A>'' = {}) \<and>
|
|
(\<forall>\<A>' \<in> \<S>. fv\<^sub>l\<^sub>s\<^sub>t \<A>' \<inter> bvars\<^sub>l\<^sub>s\<^sub>t \<A> = {}) \<and>
|
|
(\<forall>\<A>' \<in> \<S>. fv\<^sub>l\<^sub>s\<^sub>t \<A> \<inter> bvars\<^sub>l\<^sub>s\<^sub>t \<A>' = {})"
|
|
|
|
definition typing_cond_prot where
|
|
"typing_cond_prot \<P> \<equiv>
|
|
wf\<^sub>l\<^sub>s\<^sub>t\<^sub>s \<P> \<and>
|
|
tfr\<^sub>s\<^sub>e\<^sub>t (\<Union>(trms\<^sub>l\<^sub>s\<^sub>t ` \<P>)) \<and>
|
|
wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (\<Union>(trms\<^sub>l\<^sub>s\<^sub>t ` \<P>)) \<and>
|
|
(\<forall>\<A> \<in> \<P>. list_all tfr\<^sub>s\<^sub>t\<^sub>p (unlabel \<A>)) \<and>
|
|
Ana_invar_subst (\<Union>(ik\<^sub>s\<^sub>t ` unlabel ` \<P>) \<union> \<Union>(assignment_rhs\<^sub>s\<^sub>t ` unlabel ` \<P>))"
|
|
|
|
definition par_comp_prot where
|
|
"par_comp_prot \<P> Sec \<equiv>
|
|
(\<forall>l1 l2. l1 \<noteq> l2 \<longrightarrow>
|
|
GSMP_disjoint (\<Union>\<A> \<in> \<P>. trms_proj\<^sub>l\<^sub>s\<^sub>t l1 \<A>) (\<Union>\<A> \<in> \<P>. trms_proj\<^sub>l\<^sub>s\<^sub>t l2 \<A>) Sec) \<and>
|
|
ground Sec \<and> (\<forall>s \<in> Sec. \<forall>s' \<in> subterms s. {} \<turnstile>\<^sub>c s' \<or> s' \<in> Sec) \<and>
|
|
typing_cond_prot \<P>"
|
|
|
|
|
|
subsubsection \<open>Lemmata: Labeled Protocols\<close>
|
|
lemma wf\<^sub>l\<^sub>s\<^sub>t\<^sub>s_eqs_wf\<^sub>l\<^sub>s\<^sub>t\<^sub>s'[simp]: "wf\<^sub>l\<^sub>s\<^sub>t\<^sub>s S = wf\<^sub>l\<^sub>s\<^sub>t\<^sub>s' S []"
|
|
unfolding wf\<^sub>l\<^sub>s\<^sub>t\<^sub>s_def wf\<^sub>l\<^sub>s\<^sub>t\<^sub>s'_def unlabel_def by auto
|
|
|
|
lemma par_comp_prot_impl_par_comp:
|
|
assumes "par_comp_prot \<P> Sec" "\<A> \<in> \<P>"
|
|
shows "par_comp \<A> Sec"
|
|
proof -
|
|
have *: "\<forall>l1 l2. l1 \<noteq> l2 \<longrightarrow>
|
|
GSMP_disjoint (\<Union>\<A> \<in> \<P>. trms_proj\<^sub>l\<^sub>s\<^sub>t l1 \<A>) (\<Union>\<A> \<in> \<P>. trms_proj\<^sub>l\<^sub>s\<^sub>t l2 \<A>) Sec"
|
|
using assms(1) unfolding par_comp_prot_def by metis
|
|
{ fix l1 l2::'lbl assume **: "l1 \<noteq> l2"
|
|
hence ***: "GSMP_disjoint (\<Union>\<A> \<in> \<P>. trms_proj\<^sub>l\<^sub>s\<^sub>t l1 \<A>) (\<Union>\<A> \<in> \<P>. trms_proj\<^sub>l\<^sub>s\<^sub>t l2 \<A>) Sec"
|
|
using * by auto
|
|
have "GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t l1 \<A>) (trms_proj\<^sub>l\<^sub>s\<^sub>t l2 \<A>) Sec"
|
|
using GSMP_disjoint_subset[OF ***] assms(2) by auto
|
|
} hence "\<forall>l1 l2. l1 \<noteq> l2 \<longrightarrow> GSMP_disjoint (trms_proj\<^sub>l\<^sub>s\<^sub>t l1 \<A>) (trms_proj\<^sub>l\<^sub>s\<^sub>t l2 \<A>) Sec" by metis
|
|
thus ?thesis using assms unfolding par_comp_prot_def par_comp_def by metis
|
|
qed
|
|
|
|
lemma typing_cond_prot_impl_typing_cond:
|
|
assumes "typing_cond_prot \<P>" "\<A> \<in> \<P>"
|
|
shows "typing_cond (unlabel \<A>)"
|
|
proof -
|
|
have 1: "wf\<^sub>s\<^sub>t {} (unlabel \<A>)" "fv\<^sub>l\<^sub>s\<^sub>t \<A> \<inter> bvars\<^sub>l\<^sub>s\<^sub>t \<A> = {}"
|
|
using assms unfolding typing_cond_prot_def wf\<^sub>l\<^sub>s\<^sub>t\<^sub>s_def by auto
|
|
|
|
have "tfr\<^sub>s\<^sub>e\<^sub>t (\<Union>(trms\<^sub>l\<^sub>s\<^sub>t ` \<P>))"
|
|
"wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (\<Union>(trms\<^sub>l\<^sub>s\<^sub>t ` \<P>))"
|
|
"trms\<^sub>l\<^sub>s\<^sub>t \<A> \<subseteq> \<Union>(trms\<^sub>l\<^sub>s\<^sub>t ` \<P>)"
|
|
"SMP (trms\<^sub>l\<^sub>s\<^sub>t \<A>) - Var`\<V> \<subseteq> SMP (\<Union>(trms\<^sub>l\<^sub>s\<^sub>t ` \<P>)) - Var`\<V>"
|
|
using assms SMP_mono[of "trms\<^sub>l\<^sub>s\<^sub>t \<A>" "\<Union>(trms\<^sub>l\<^sub>s\<^sub>t ` \<P>)"]
|
|
unfolding typing_cond_prot_def
|
|
by (metis, metis, auto)
|
|
hence 2: "tfr\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>l\<^sub>s\<^sub>t \<A>)" and 3: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>l\<^sub>s\<^sub>t \<A>)"
|
|
unfolding tfr\<^sub>s\<^sub>e\<^sub>t_def by (meson subsetD)+
|
|
|
|
have 4: "list_all tfr\<^sub>s\<^sub>t\<^sub>p (unlabel \<A>)" using assms unfolding typing_cond_prot_def by auto
|
|
|
|
have "subterms\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t (unlabel \<A>) \<union> assignment_rhs\<^sub>s\<^sub>t (unlabel \<A>)) \<subseteq>
|
|
subterms\<^sub>s\<^sub>e\<^sub>t (\<Union>(ik\<^sub>s\<^sub>t ` unlabel ` \<P>) \<union> \<Union>(assignment_rhs\<^sub>s\<^sub>t ` unlabel ` \<P>))"
|
|
using assms(2) by auto
|
|
hence 5: "Ana_invar_subst (ik\<^sub>s\<^sub>t (unlabel \<A>) \<union> assignment_rhs\<^sub>s\<^sub>t (unlabel \<A>))"
|
|
using assms SMP_mono unfolding typing_cond_prot_def Ana_invar_subst_def by (meson subsetD)
|
|
|
|
show ?thesis using 1 2 3 4 5 unfolding typing_cond_def tfr\<^sub>s\<^sub>t_def by blast
|
|
qed
|
|
|
|
|
|
subsubsection \<open>Theorem: Parallel Compositionality for Labeled Protocols\<close>
|
|
definition component_prot where
|
|
"component_prot n P \<equiv> (\<forall>l \<in> P. \<forall>s \<in> set l. is_LabelN n s \<or> is_LabelS s)"
|
|
|
|
definition composed_prot where
|
|
"composed_prot \<P>\<^sub>i \<equiv> {\<A>. \<forall>n. proj n \<A> \<in> \<P>\<^sub>i n}"
|
|
|
|
definition component_secure_prot where
|
|
"component_secure_prot n P Sec attack \<equiv> (\<forall>\<A> \<in> P. suffix [(ln n, Send (Fun attack []))] \<A> \<longrightarrow>
|
|
(\<forall>\<I>\<^sub>\<tau>. (interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>\<^sub>\<tau> \<and> wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>\<^sub>\<tau> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<I>\<^sub>\<tau>)) \<longrightarrow>
|
|
\<not>(\<I>\<^sub>\<tau> \<Turnstile> \<langle>proj_unl n \<A>\<rangle>) \<and>
|
|
(\<forall>\<A>'. prefix \<A>' \<A> \<longrightarrow>
|
|
(\<forall>t \<in> Sec-declassified\<^sub>l\<^sub>s\<^sub>t \<A>' \<I>\<^sub>\<tau>. \<not>(\<I>\<^sub>\<tau> \<Turnstile> \<langle>proj_unl n \<A>'@[Send t]\<rangle>)))))"
|
|
|
|
definition component_leaks where
|
|
"component_leaks n \<A> Sec \<equiv> (\<exists>\<A>' \<I>\<^sub>\<tau>. interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>\<^sub>\<tau> \<and> wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>\<^sub>\<tau> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<I>\<^sub>\<tau>) \<and>
|
|
prefix \<A>' \<A> \<and> (\<exists>t \<in> Sec - declassified\<^sub>l\<^sub>s\<^sub>t \<A>' \<I>\<^sub>\<tau>. (\<I>\<^sub>\<tau> \<Turnstile> \<langle>proj_unl n \<A>'@[Send t]\<rangle>)))"
|
|
|
|
definition unsat where
|
|
"unsat \<A> \<equiv> (\<forall>\<I>. interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I> \<longrightarrow> \<not>(\<I> \<Turnstile> \<langle>unlabel \<A>\<rangle>))"
|
|
|
|
theorem par_comp_constr_prot:
|
|
assumes P: "P = composed_prot Pi" "par_comp_prot P Sec" "\<forall>n. component_prot n (Pi n)"
|
|
and left_secure: "component_secure_prot n (Pi n) Sec attack"
|
|
shows "\<forall>\<A> \<in> P. suffix [(ln n, Send (Fun attack []))] \<A> \<longrightarrow>
|
|
unsat \<A> \<or> (\<exists>m. n \<noteq> m \<and> component_leaks m \<A> Sec)"
|
|
proof -
|
|
{ fix \<A> \<A>' assume \<A>: "\<A> = \<A>'@[(ln n, Send (Fun attack []))]" "\<A> \<in> P"
|
|
let ?P = "\<exists>\<A>' \<I>\<^sub>\<tau>. interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>\<^sub>\<tau> \<and> wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>\<^sub>\<tau> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<I>\<^sub>\<tau>) \<and> prefix \<A>' \<A> \<and>
|
|
(\<exists>t \<in> Sec - declassified\<^sub>l\<^sub>s\<^sub>t \<A>' \<I>\<^sub>\<tau>. \<exists>m. n \<noteq> m \<and> (\<I>\<^sub>\<tau> \<Turnstile> \<langle>proj_unl m \<A>'@[Send t]\<rangle>))"
|
|
have tcp: "typing_cond_prot P" using P(2) unfolding par_comp_prot_def by simp
|
|
have par_comp: "par_comp \<A> Sec" "typing_cond (unlabel \<A>)"
|
|
using par_comp_prot_impl_par_comp[OF P(2) \<A>(2)]
|
|
typing_cond_prot_impl_typing_cond[OF tcp \<A>(2)]
|
|
by metis+
|
|
|
|
have "unlabel (proj n \<A>) = proj_unl n \<A>" "proj_unl n \<A> = proj_unl n (proj n \<A>)"
|
|
"\<And>A. A \<in> Pi n \<Longrightarrow> proj n A = A"
|
|
"proj n \<A> = (proj n \<A>')@[(ln n, Send (Fun attack []))]"
|
|
using P(1,3) \<A> by (auto simp add: proj_def unlabel_def component_prot_def composed_prot_def)
|
|
moreover have "proj n \<A> \<in> Pi n"
|
|
using P(1) \<A> unfolding composed_prot_def by blast
|
|
moreover {
|
|
fix A assume "prefix A \<A>"
|
|
hence *: "prefix (proj n A) (proj n \<A>)" unfolding proj_def prefix_def by force
|
|
hence "proj_unl n A = proj_unl n (proj n A)"
|
|
"\<forall>I. declassified\<^sub>l\<^sub>s\<^sub>t A I = declassified\<^sub>l\<^sub>s\<^sub>t (proj n A) I"
|
|
unfolding proj_def declassified\<^sub>l\<^sub>s\<^sub>t_def by auto
|
|
hence "\<exists>B. prefix B (proj n \<A>) \<and> proj_unl n A = proj_unl n B \<and>
|
|
(\<forall>I. declassified\<^sub>l\<^sub>s\<^sub>t A I = declassified\<^sub>l\<^sub>s\<^sub>t B I)"
|
|
using * by metis
|
|
|
|
}
|
|
ultimately have *:
|
|
"\<forall>\<I>\<^sub>\<tau>. interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>\<^sub>\<tau> \<and> wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>\<^sub>\<tau> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<I>\<^sub>\<tau>) \<longrightarrow>
|
|
\<not>(\<I>\<^sub>\<tau> \<Turnstile> \<langle>proj_unl n \<A>\<rangle>) \<and> (\<forall>\<A>'. prefix \<A>' \<A> \<longrightarrow>
|
|
(\<forall>t \<in> Sec - declassified\<^sub>l\<^sub>s\<^sub>t \<A>' \<I>\<^sub>\<tau>. \<not>(\<I>\<^sub>\<tau> \<Turnstile> \<langle>proj_unl n \<A>'@[Send t]\<rangle>)))"
|
|
using left_secure unfolding component_secure_prot_def composed_prot_def suffix_def by metis
|
|
{ fix \<I> assume \<I>: "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>" "\<I> \<Turnstile> \<langle>unlabel \<A>\<rangle>"
|
|
obtain \<I>\<^sub>\<tau> where \<I>\<^sub>\<tau>:
|
|
"interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>\<^sub>\<tau>" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>\<^sub>\<tau>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<I>\<^sub>\<tau>)"
|
|
"\<exists>\<A>'. prefix \<A>' \<A> \<and> (strand_leaks\<^sub>l\<^sub>s\<^sub>t \<A>' Sec \<I>\<^sub>\<tau>)"
|
|
using par_comp_constr[OF par_comp \<I>(2,1)] * by moura
|
|
hence "\<exists>\<A>'. prefix \<A>' \<A> \<and> (\<exists>t \<in> Sec - declassified\<^sub>l\<^sub>s\<^sub>t \<A>' \<I>\<^sub>\<tau>. \<exists>m.
|
|
n \<noteq> m \<and> (\<I>\<^sub>\<tau> \<Turnstile> \<langle>proj_unl m \<A>'@[Send t]\<rangle>))"
|
|
using \<I>\<^sub>\<tau>(4) * unfolding strand_leaks\<^sub>l\<^sub>s\<^sub>t_def by metis
|
|
hence ?P using \<I>\<^sub>\<tau>(1,2,3) by auto
|
|
} hence "unsat \<A> \<or> (\<exists>m. n \<noteq> m \<and> component_leaks m \<A> Sec)"
|
|
by (metis unsat_def component_leaks_def)
|
|
} thus ?thesis unfolding suffix_def by metis
|
|
qed
|
|
|
|
end
|
|
|
|
|
|
subsection \<open>Automated GSMP Disjointness\<close>
|
|
locale labeled_typed_model' = typed_model' arity public Ana \<Gamma> +
|
|
labeled_typed_model arity public Ana \<Gamma> label_witness1 label_witness2
|
|
for arity::"'fun \<Rightarrow> nat"
|
|
and public::"'fun \<Rightarrow> bool"
|
|
and Ana::"('fun,(('fun,'atom::finite) term_type \<times> nat)) term
|
|
\<Rightarrow> (('fun,(('fun,'atom) term_type \<times> nat)) term list
|
|
\<times> ('fun,(('fun,'atom) term_type \<times> nat)) term list)"
|
|
and \<Gamma>::"('fun,(('fun,'atom) term_type \<times> nat)) term \<Rightarrow> ('fun,'atom) term_type"
|
|
and label_witness1 label_witness2::'lbl
|
|
begin
|
|
|
|
lemma GSMP_disjointI:
|
|
fixes A' A B B'::"('fun, ('fun, 'atom) term \<times> nat) term list"
|
|
defines "f \<equiv> \<lambda>M. {t \<cdot> \<delta> | t \<delta>. t \<in> M \<and> wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>) \<and> fv (t \<cdot> \<delta>) = {}}"
|
|
and "\<delta> \<equiv> var_rename (max_var_set (fv\<^sub>s\<^sub>e\<^sub>t (set A)))"
|
|
assumes A'_wf: "list_all (wf\<^sub>t\<^sub>r\<^sub>m' arity) A'"
|
|
and B'_wf: "list_all (wf\<^sub>t\<^sub>r\<^sub>m' arity) B'"
|
|
and A_inst: "has_all_wt_instances_of \<Gamma> (set A') (set A)"
|
|
and B_inst: "has_all_wt_instances_of \<Gamma> (set B') (set (B \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>))"
|
|
and A_SMP_repr: "finite_SMP_representation arity Ana \<Gamma> A"
|
|
and B_SMP_repr: "finite_SMP_representation arity Ana \<Gamma> (B \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>)"
|
|
and AB_trms_disj:
|
|
"\<forall>t \<in> set A. \<forall>s \<in> set (B \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>). \<Gamma> t = \<Gamma> s \<and> mgu t s \<noteq> None \<longrightarrow>
|
|
(intruder_synth' public arity {} t \<and> intruder_synth' public arity {} s) \<or>
|
|
((\<exists>u \<in> Sec. is_wt_instance_of_cond \<Gamma> t u) \<and> (\<exists>u \<in> Sec. is_wt_instance_of_cond \<Gamma> s u))"
|
|
and Sec_wf: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s Sec"
|
|
shows "GSMP_disjoint (set A') (set B') ((f Sec) - {m. {} \<turnstile>\<^sub>c m})"
|
|
proof -
|
|
have A_wf: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (set A)" and B_wf: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (set (B \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>))"
|
|
and A'_wf': "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (set A')" and B'_wf': "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (set B')"
|
|
using finite_SMP_representationD[OF A_SMP_repr]
|
|
finite_SMP_representationD[OF B_SMP_repr]
|
|
A'_wf B'_wf
|
|
unfolding wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s_code[symmetric] wf\<^sub>t\<^sub>r\<^sub>m_code[symmetric] list_all_iff by blast+
|
|
|
|
have AB_fv_disj: "fv\<^sub>s\<^sub>e\<^sub>t (set A) \<inter> fv\<^sub>s\<^sub>e\<^sub>t (set (B \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>)) = {}"
|
|
using var_rename_fv_set_disjoint'[of "set A" "set B", unfolded \<delta>_def[symmetric]] by simp
|
|
|
|
have "GSMP_disjoint (set A) (set (B \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>)) ((f Sec) - {m. {} \<turnstile>\<^sub>c m})"
|
|
using ground_SMP_disjointI[OF AB_fv_disj A_SMP_repr B_SMP_repr Sec_wf AB_trms_disj]
|
|
unfolding GSMP_def GSMP_disjoint_def f_def by blast
|
|
moreover have "SMP (set A') \<subseteq> SMP (set A)" "SMP (set B') \<subseteq> SMP (set (B \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>))"
|
|
using SMP_I'[OF A'_wf' A_wf A_inst] SMP_SMP_subset[of "set A'" "set A"]
|
|
SMP_I'[OF B'_wf' B_wf B_inst] SMP_SMP_subset[of "set B'" "set (B \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>)"]
|
|
by blast+
|
|
ultimately show ?thesis unfolding GSMP_def GSMP_disjoint_def by auto
|
|
qed
|
|
|
|
end
|
|
|
|
end
|