1820 lines
71 KiB
Plaintext
1820 lines
71 KiB
Plaintext
(*
|
|
* Copyright 2014, NICTA
|
|
*
|
|
* This software may be distributed and modified according to the terms of
|
|
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
|
* See "LICENSE_GPLv2.txt" for details.
|
|
*
|
|
* @TAG(NICTA_GPL)
|
|
*)
|
|
|
|
theory Noninterference_Base_Enabledness_weak_asym
|
|
imports "../../lib/Simulation"
|
|
begin
|
|
|
|
text {*
|
|
This file contains the final output of Nikolas Stott's work as a visiting
|
|
practicum exchange student in the second half of 2012. It defines
|
|
noninterference conditions for systems that are not ``enabled'' (i.e. where
|
|
not every event is always executable in every state). It defines
|
|
a new unwinding condition for such systems and proves that, with the existing
|
|
unwinding conditions, these imply the noninterference conditions.
|
|
The given unwinding conditions are not equivalent to the noninterference
|
|
conditions (they are strictly stronger), as far as we could tell.
|
|
*}
|
|
|
|
lemma un_eq:
|
|
"\<lbrakk>S = S'; T = T'\<rbrakk> \<Longrightarrow> S \<union> T = S' \<union> T'"
|
|
apply auto
|
|
done
|
|
|
|
lemma Un_eq:
|
|
"\<lbrakk>\<And> x y. \<lbrakk>x \<in> xs; y \<in> ys\<rbrakk> \<Longrightarrow> P x = Q y; \<exists> x. x \<in> xs; \<exists> y. y \<in> ys\<rbrakk> \<Longrightarrow> (\<Union>x\<in>xs. P x) = (\<Union>y\<in>ys. Q y)"
|
|
apply auto
|
|
done
|
|
|
|
lemma Int_eq:
|
|
"\<lbrakk>\<And> x y. \<lbrakk>x \<in> xs; y \<in> ys\<rbrakk> \<Longrightarrow> P x = Q y; \<exists> x. x \<in> xs; \<exists> y. y \<in> ys\<rbrakk> \<Longrightarrow> (\<Inter>x\<in>xs. P x) = (\<Inter>y\<in>ys. Q y)"
|
|
apply auto
|
|
done
|
|
|
|
lemma Un_eq_Int:
|
|
assumes ex: "\<exists> x. x \<in> xs"
|
|
assumes ey: "\<exists> y. y \<in> ys"
|
|
assumes a: "\<And> x y. \<lbrakk>x \<in> xs; y \<in> ys\<rbrakk> \<Longrightarrow> S x = S' y"
|
|
shows "(\<Union>x\<in>xs. S x) = (\<Inter>x\<in>ys. S' x)"
|
|
apply(rule equalityI)
|
|
apply(clarsimp)
|
|
apply(drule a, assumption, simp)
|
|
apply clarsimp
|
|
apply(insert ex ey)
|
|
apply clarsimp
|
|
apply(frule a, assumption)
|
|
apply fastforce
|
|
done
|
|
|
|
primrec Run :: "('e \<Rightarrow> ('s \<times> 's) set) \<Rightarrow> 'e list \<Rightarrow> ('s \<times> 's) set" where
|
|
"Run Stepf [] = Id" |
|
|
"Run Stepf (a#as) = Stepf a O Run Stepf as"
|
|
|
|
|
|
lemma Run_mid':
|
|
shows
|
|
"\<forall> s u bs. (s,u) \<in> Run Stepf (as @ bs) \<longrightarrow> (\<exists> t. (s,t) \<in> Run Stepf as \<and> (t,u) \<in> Run Stepf bs)"
|
|
proof(induct as)
|
|
case Nil show ?case
|
|
apply(clarsimp)
|
|
done
|
|
next
|
|
case (Cons a as) show ?case
|
|
apply(clarsimp simp: relcomp_def)
|
|
apply(drule "Cons.hyps"[rule_format])
|
|
apply fastforce
|
|
done
|
|
qed
|
|
|
|
lemma Run_mid:
|
|
"(s,u) \<in> Run Stepf (as @ bs) \<Longrightarrow> (\<exists> t. (s,t) \<in> Run Stepf as \<and> (t,u) \<in> Run Stepf bs)"
|
|
apply(erule Run_mid'[rule_format])
|
|
done
|
|
|
|
lemma Run_ConsI:
|
|
"\<exists>t. (s,t)\<in>Stepf a \<and>(t,u)\<in> Run Stepf as \<Longrightarrow> (s,u)\<in> Run Stepf (a#as)"
|
|
apply(auto)
|
|
done
|
|
|
|
lemma Run_ConsD:
|
|
"(s,u) \<in> Run Stepf (a#as) \<Longrightarrow> (\<exists> t. (s,t) \<in> Stepf a \<and> (t,u) \<in> Run Stepf as)"
|
|
apply(subgoal_tac "a#as = [a]@as")
|
|
apply(drule subst,assumption)
|
|
apply(drule Run_mid,simp)
|
|
apply(auto)
|
|
done
|
|
|
|
lemma Run_trans:
|
|
"\<lbrakk> (s,t) \<in> Run Stepf as; (t,u) \<in> Run Stepf bs \<rbrakk> \<Longrightarrow> (s,u) \<in> Run Stepf (as @ bs)"
|
|
by (induct as arbitrary: s t u bs) auto
|
|
|
|
lemma Run_app:
|
|
"Run Stepf (as @ bs) = (Run Stepf as) O (Run Stepf bs)"
|
|
apply(rule equalityI)
|
|
apply(fastforce dest: Run_mid)
|
|
apply(fastforce intro: Run_trans)
|
|
done
|
|
|
|
(* we define the top-level properties for any enabled system *)
|
|
locale system =
|
|
fixes A :: "('a,'s,'e) data_type"
|
|
and s0 :: "'s" (* an initial state *)
|
|
|
|
context system begin
|
|
|
|
definition reachable where
|
|
"reachable s \<equiv> \<exists> js. s \<in> execution A s0 js"
|
|
|
|
definition Step where
|
|
"Step a \<equiv> {(s,s') . s' \<in> execution A s [a]}"
|
|
|
|
(* Executable should make sense only if the states are reachable.
|
|
'reachable s' in the second equation is to make sure that the first state of the computation is reachable,
|
|
the following become trivial by future lemma 'reachable_Step' *)
|
|
primrec Executable where
|
|
"Executable [] s = reachable s"|
|
|
"Executable (a#as) s = (reachable s \<and> (\<exists>s'. (s,s') \<in> Step a \<and> Executable as s'))"
|
|
|
|
(* An alternative definition of Executability for a sequence of actions,
|
|
which, assuming the state is reachable, is equivalent to the previous one (proved later)*)
|
|
definition Executable' where
|
|
"Executable' as s \<equiv> reachable s \<longrightarrow> (\<exists>t. t\<in>execution A s as)"
|
|
|
|
definition obs_det where
|
|
"obs_det \<equiv> \<forall> s js. \<exists> s'. execution A s js = {s'}"
|
|
|
|
lemma obs_detD:
|
|
"obs_det \<Longrightarrow> \<exists> s'. execution A s js = {s'}" by (simp add: obs_det_def)
|
|
|
|
definition no_abs where
|
|
"no_abs \<equiv> \<forall> x. Init A (Fin A x) = {x}"
|
|
|
|
lemma no_absD:
|
|
"no_abs \<Longrightarrow> Init A (Fin A x) = {x}" by (simp add: no_abs_def)
|
|
|
|
end
|
|
|
|
(* we define the unwinding conditions for systems for which a running
|
|
a sequence of events is equivalent to performing a sequence of individual
|
|
steps: one for each event in the sequence in turn *)
|
|
locale Step_system = system A s0
|
|
for A :: "('a,'s,'e) data_type" and s0 :: "'s" +
|
|
assumes reachable_s0: "reachable s0"
|
|
assumes execution_Run: "reachable s \<Longrightarrow> execution A s as = {s'. (s,s') \<in> Run Step as}"
|
|
|
|
|
|
context Step_system begin
|
|
|
|
lemma execution_Run':
|
|
"s \<in> execution A s0 js \<Longrightarrow> execution A s as = {s'. (s,s') \<in> Run Step as}"
|
|
apply(rule execution_Run)
|
|
apply(fastforce simp: reachable_def)
|
|
done
|
|
|
|
|
|
lemma reachable_execution:
|
|
"\<lbrakk>reachable s; s' \<in> execution A s js\<rbrakk> \<Longrightarrow> reachable s'"
|
|
apply(clarsimp simp: reachable_def)
|
|
apply(rule_tac x="jsa @ js" in exI)
|
|
apply(frule execution_Run'[where s=s and as=js])
|
|
apply(simp add: execution_Run[where s=s0, simplified reachable_s0])
|
|
apply(fastforce simp: Run_app)
|
|
done
|
|
|
|
|
|
lemma reachable_Step:
|
|
"\<lbrakk>reachable s; (s,s') \<in> Step a\<rbrakk> \<Longrightarrow> reachable s'"
|
|
apply(erule reachable_execution)
|
|
apply(simp add: Step_def)
|
|
done
|
|
|
|
(*We prove that Executable and Executable' are equivalent*)
|
|
lemma Executable'I:
|
|
"\<lbrakk>Executable as s\<rbrakk> \<Longrightarrow> Executable' as s"
|
|
apply(clarsimp simp: Executable'_def)
|
|
apply(induct as arbitrary: s)
|
|
apply(fastforce simp :execution_Run)
|
|
apply(clarsimp)
|
|
apply(drule_tac x=s' in meta_spec)
|
|
apply(frule reachable_Step,assumption)
|
|
apply(fastforce intro:Run_ConsI simp:execution_Run)
|
|
done
|
|
|
|
lemma Executable'D:
|
|
"\<lbrakk>reachable s; Executable' as s\<rbrakk> \<Longrightarrow> Executable as s"
|
|
apply(clarsimp simp: Executable'_def)
|
|
apply(induct as arbitrary:s)
|
|
apply(simp)
|
|
apply(simp add:execution_Run del: Run.simps)
|
|
apply(blast intro:reachable_Step dest:Run_ConsD)
|
|
done
|
|
|
|
lemma Executable_Executable'_equiv:
|
|
"reachable s \<Longrightarrow> Executable as s = Executable' as s"
|
|
apply(rule iffI)
|
|
apply(blast intro: Executable'I)
|
|
apply(blast dest: Executable'D)
|
|
done
|
|
|
|
end
|
|
|
|
locale Init_Fin_system = system A s0
|
|
for A :: "('a,'s,'e) data_type" and s0 :: "'s" +
|
|
assumes reachable_s0: "reachable s0"
|
|
assumes Fin_Init: "reachable s \<Longrightarrow> Fin A ` Init A s = {s}"
|
|
assumes Init_Fin: "x \<in> Init A (Fin A x)"
|
|
assumes obs_det_or_no_abs: "obs_det \<or> no_abs"
|
|
|
|
|
|
(* when Init is the inverse image of Fin, the above assumptions are met by a system
|
|
for which Fin is injective, or one that appears deterministic to an observer *)
|
|
locale Init_inv_Fin_system = system A s0
|
|
for A :: "('a,'s,'e) data_type" and s0 :: "'s" +
|
|
assumes Fin_Init_s0: "s0 \<in> Fin A ` Init A s0"
|
|
assumes Init_inv_Fin: "Init A s = {s'. Fin A s' = s}"
|
|
assumes Fin_inj: "obs_det \<or> inj (Fin A)"
|
|
|
|
sublocale Init_inv_Fin_system \<subseteq> Init_Fin_system
|
|
apply(unfold_locales)
|
|
apply(simp add: reachable_def)
|
|
apply(rule_tac x="[]" in exI)
|
|
apply(simp add: execution_def steps_def)
|
|
apply(simp add: Fin_Init_s0)
|
|
apply(simp add: Init_inv_Fin)
|
|
apply(simp add: image_def)
|
|
apply(fastforce simp: reachable_def execution_def)
|
|
apply(simp add: Init_inv_Fin)
|
|
apply(case_tac "obs_det", blast)
|
|
apply(rule disjI2)
|
|
apply(clarsimp simp: no_abs_def Init_inv_Fin)
|
|
apply(insert Fin_inj)
|
|
apply clarsimp
|
|
apply(auto dest: injD)
|
|
done
|
|
|
|
context Init_Fin_system begin
|
|
|
|
|
|
lemma execution_subset_Run:
|
|
"reachable s \<Longrightarrow> execution A s as \<subseteq> {s'. (s,s') \<in> Run Step as}"
|
|
apply(induct as arbitrary: s rule: rev_induct)
|
|
apply(simp add: execution_def steps_def Fin_Init)
|
|
apply(simp add: execution_def steps_def)
|
|
apply(rule subsetI)
|
|
apply clarsimp
|
|
apply(rule Run_trans)
|
|
apply blast
|
|
apply(cut_tac x=xc in Init_Fin)
|
|
apply(clarsimp simp: Step_def execution_def steps_def)
|
|
apply blast
|
|
done
|
|
|
|
lemma Run_subset_execution:
|
|
"\<lbrakk>no_abs; reachable s\<rbrakk> \<Longrightarrow> {s'. (s,s') \<in> Run Step as} \<subseteq> execution A s as"
|
|
apply(induct as arbitrary: s rule: rev_induct)
|
|
apply(simp add: execution_def steps_def Fin_Init)
|
|
apply(simp add: execution_def steps_def)
|
|
apply(rule subsetI)
|
|
apply clarsimp
|
|
apply(drule Run_mid)
|
|
apply clarsimp
|
|
apply(drule_tac x=s in meta_spec)
|
|
apply clarsimp
|
|
apply(drule_tac subsetD)
|
|
apply blast
|
|
apply(clarsimp simp: Image_def image_def Step_def execution_def steps_def)
|
|
apply(rule_tac x=xc in exI)
|
|
apply clarsimp
|
|
apply(rule_tac x=xd in bexI)
|
|
apply assumption
|
|
apply(drule_tac x=xb in no_absD)
|
|
by simp
|
|
|
|
lemma Run_det:
|
|
"obs_det \<Longrightarrow> \<exists> s'. {s'. (s,s') \<in> Run Step as} = {s'}"
|
|
apply(induct as arbitrary: s rule: rev_induct)
|
|
apply simp
|
|
apply(simp add: Run_app relcomp_def)
|
|
apply(drule_tac x=s in meta_spec)
|
|
apply clarsimp
|
|
apply(drule_tac s=s' and js="[x]" in obs_detD)
|
|
apply (clarsimp simp: Step_def)
|
|
apply(rule_tac x="s'a" in exI)
|
|
apply (auto dest: equalityD1)
|
|
done
|
|
|
|
lemma eq:
|
|
"\<lbrakk>S \<subseteq> T; \<exists> x. S = {x}; \<exists> y. T = {y}\<rbrakk> \<Longrightarrow> S = T"
|
|
apply blast
|
|
done
|
|
|
|
lemma execution_Run:
|
|
"reachable s \<Longrightarrow> execution A s as = {s'. (s,s') \<in> Run Step as}"
|
|
apply(rule disjE[OF obs_det_or_no_abs])
|
|
apply(rule eq)
|
|
apply(erule execution_subset_Run)
|
|
apply(erule obs_detD)
|
|
apply(erule Run_det)
|
|
apply(rule equalityI)
|
|
apply(erule execution_subset_Run)
|
|
apply(erule (1) Run_subset_execution)
|
|
done
|
|
|
|
end
|
|
|
|
sublocale Init_Fin_system \<subseteq> Step_system
|
|
apply(unfold_locales)
|
|
apply(rule reachable_s0)
|
|
apply(erule execution_Run)
|
|
done
|
|
|
|
|
|
locale noninterference_policy =
|
|
fixes dom :: "'e \<Rightarrow> 's \<Rightarrow> 'd" (* dynamic dom assignment *)
|
|
fixes uwr :: "'d \<Rightarrow> ('s \<times> 's) set"
|
|
fixes policy :: "('d \<times> 'd) set" (* who can send info to whom *)
|
|
fixes out :: "'d \<Rightarrow> 's \<Rightarrow> 'p" (* observable parts of d in state s *)
|
|
fixes schedDomain :: "'d"
|
|
assumes uwr_equiv_rel: "equiv UNIV (uwr u)"
|
|
assumes schedIncludesCurrentDom:
|
|
"(s,t) \<in> uwr schedDomain \<Longrightarrow> dom e s = dom e t"
|
|
assumes schedFlowsToAll:
|
|
"(schedDomain,d) \<in> policy"
|
|
assumes schedNotGlobalChannel:
|
|
"(x,schedDomain) \<in> policy \<Longrightarrow> x = schedDomain"
|
|
|
|
|
|
context noninterference_policy begin
|
|
|
|
abbreviation uwr2 :: "'s \<Rightarrow> 'd \<Rightarrow> 's \<Rightarrow> bool" ("(_/ \<sim>_\<sim>/ _)" [50,100,50] 1000)
|
|
where "s \<sim>u\<sim> t \<equiv> (s,t) \<in> uwr u"
|
|
|
|
abbreviation policy2 :: "'d \<Rightarrow> 'd \<Rightarrow> bool" (infix "\<leadsto>" 50) where
|
|
"u \<leadsto> v \<equiv> (u,v) \<in> policy"
|
|
|
|
lemma uwr_refl:
|
|
"s \<sim>(u::'d)\<sim> s"
|
|
apply(cut_tac u=u in uwr_equiv_rel)
|
|
apply(clarsimp simp: equiv_def)
|
|
apply(blast dest: refl_onD)
|
|
done
|
|
|
|
lemma uwr_sym:
|
|
"x \<sim>(u::'d)\<sim> y \<Longrightarrow> y \<sim>u\<sim> x"
|
|
apply(cut_tac u=u in uwr_equiv_rel)
|
|
apply(clarsimp simp: equiv_def)
|
|
apply(blast dest: symD)
|
|
done
|
|
|
|
lemma uwr_trans:
|
|
"\<lbrakk>x \<sim>(u::'d)\<sim> y; y \<sim>u\<sim> z\<rbrakk> \<Longrightarrow> x \<sim>u\<sim> z"
|
|
apply(cut_tac u=u in uwr_equiv_rel)
|
|
apply(clarsimp simp: equiv_def)
|
|
apply(blast dest: transD)
|
|
done
|
|
|
|
definition sameFor_dom :: "'s \<Rightarrow> 'd set \<Rightarrow> 's \<Rightarrow> bool" ("(_/ \<approx>_\<approx>/ _)" [50,100,50] 1000) where
|
|
"s \<approx>us\<approx> t \<equiv> \<forall>u\<in>us. (s,t) \<in> uwr u"
|
|
|
|
lemma sameFor_subset_dom: "\<lbrakk>s \<approx>(x::'d set)\<approx> t; y \<subseteq> x\<rbrakk> \<Longrightarrow> s \<approx>y\<approx> t"
|
|
by(fastforce simp: sameFor_dom_def)
|
|
|
|
|
|
lemma sameFor_inter_domI: "s \<approx>(S::'d set)\<approx> t \<Longrightarrow> s \<approx>(S \<inter> B)\<approx> t"
|
|
by(auto simp: sameFor_dom_def)
|
|
|
|
|
|
lemma sameFor_sym_dom:
|
|
"s \<approx>(S::'d set)\<approx> t \<Longrightarrow> t \<approx>S\<approx> s"
|
|
by(auto simp: sameFor_dom_def uwr_sym)
|
|
|
|
end
|
|
|
|
locale noninterference_system = Step_system A s0 + noninterference_policy dom uwr policy out schedDomain
|
|
for A :: "('a,'s,'e) data_type"
|
|
and s0 :: "'s"
|
|
and dom :: "'e \<Rightarrow> 's \<Rightarrow> 'd"
|
|
and uwr :: "'d \<Rightarrow> ('s \<times> 's) set"
|
|
and policy :: "('d \<times> 'd) set"
|
|
and out :: "'d \<Rightarrow> 's \<Rightarrow> 'p"
|
|
and schedDomain :: "'d"
|
|
|
|
|
|
|
|
context noninterference_system begin
|
|
|
|
(* We change the definition of sources y adding ' \<union> {u} ' in the second equation.
|
|
This is needed in the case where 'a#as' is not executable, to ensure 'u\<in>sources as s u'
|
|
We show later that assuming the sequence is executable, this definition is equivalent to the previous definition of sources*)
|
|
primrec
|
|
sources :: "'e list \<Rightarrow> 's \<Rightarrow> 'd \<Rightarrow> 'd set" where
|
|
sources_Nil: "sources [] s u = {u}"|
|
|
sources_Cons: "sources (a#as) s u = (\<Union>{sources as s' u| s'. (s,s') \<in> Step a}) \<union>
|
|
{w. w = dom a s \<and> (\<exists> v s'. dom a s \<leadsto> v \<and> (s,s') \<in> Step a \<and> v \<in> sources as s' u)} \<union> {u}"
|
|
|
|
declare sources_Nil [simp del]
|
|
declare sources_Cons [simp del]
|
|
|
|
|
|
(* The definitions of obs_equiv and uwr_equiv are now assymmetric and take into account executability of the sequences of actions
|
|
This is necessary to prove lemma Noninfluence_gen *)
|
|
definition
|
|
obs_equiv :: "'s \<Rightarrow> 'e list \<Rightarrow> 's \<Rightarrow> 'e list \<Rightarrow> 'd \<Rightarrow> bool"
|
|
where
|
|
"obs_equiv s as t bs d \<equiv> (Executable' as s \<longrightarrow> Executable' bs t) \<and> (\<forall> s' t'. s' \<in> execution A s as \<and> t' \<in> execution A t bs \<longrightarrow>
|
|
out d s' = out d t')"
|
|
|
|
|
|
definition
|
|
uwr_equiv :: "'s \<Rightarrow> 'e list \<Rightarrow> 's \<Rightarrow> 'e list \<Rightarrow> 'd \<Rightarrow> bool"
|
|
where
|
|
"uwr_equiv s as t bs d \<equiv> (Executable' as s \<longrightarrow> Executable' bs t) \<and>
|
|
(\<forall> s' t'. s' \<in> execution A s as \<and> t' \<in> execution A t bs
|
|
\<longrightarrow> s' \<sim>d\<sim> t')"
|
|
|
|
|
|
|
|
text {* Nonleakage *}
|
|
definition
|
|
Nonleakage :: "bool" where
|
|
"Nonleakage \<equiv> \<forall>as s u t. reachable s \<and> reachable t \<longrightarrow>
|
|
s \<sim>schedDomain\<sim> t \<longrightarrow>
|
|
s \<approx>(sources as s u)\<approx> t \<longrightarrow> obs_equiv s as t as u"
|
|
|
|
text {* A generalisation of Nonleakage. *}
|
|
definition Nonleakage_gen :: "bool" where
|
|
"Nonleakage_gen \<equiv> \<forall>as s u t. reachable s \<and> reachable t \<longrightarrow>
|
|
s \<sim>schedDomain\<sim> t \<longrightarrow>
|
|
s \<approx>(sources as s u)\<approx> t \<longrightarrow> uwr_equiv s as t as u"
|
|
|
|
|
|
lemma uwr_equiv_trans:
|
|
"\<lbrakk>reachable t; uwr_equiv s as t bs x; uwr_equiv t bs u cs x\<rbrakk> \<Longrightarrow> uwr_equiv s as u cs x"
|
|
apply(clarsimp simp: uwr_equiv_def Executable'_def)
|
|
apply(blast intro: uwr_trans)
|
|
done
|
|
|
|
|
|
primrec gen_purge :: "('e list \<Rightarrow> 's \<Rightarrow> 'd \<Rightarrow> 'd set) \<Rightarrow> 'd \<Rightarrow> 'e list \<Rightarrow> 's set \<Rightarrow> 'e list"
|
|
where
|
|
Nil : "gen_purge sf u [] ss = []" |
|
|
Cons: "gen_purge sf u (a#as) ss =
|
|
(if (\<exists>s\<in>ss. dom a s \<in> sf (a#as) s u) then
|
|
a#gen_purge sf u as (\<Union>s\<in>ss. {s'. (s,s') \<in> Step a})
|
|
else
|
|
gen_purge sf u as ss)"
|
|
|
|
|
|
|
|
definition ipurge where
|
|
"ipurge \<equiv> gen_purge sources"
|
|
|
|
lemma ipurge_Nil:
|
|
"ipurge u [] ss = []"
|
|
by(auto simp: ipurge_def)
|
|
|
|
lemma ipurge_Cons:
|
|
"ipurge u (a#as) ss =
|
|
(if (\<exists> s\<in>ss. dom a s \<in> sources (a#as) s u) then
|
|
a#ipurge u as (\<Union>s\<in>ss. {s'. (s,s') \<in> Step a})
|
|
else
|
|
ipurge u as ss)"
|
|
by (auto simp: ipurge_def)
|
|
|
|
|
|
lemma gen_purge_shortens:
|
|
"length (gen_purge sf u as ss) \<le> length as"
|
|
apply(induct as arbitrary: ss)
|
|
apply(simp)
|
|
apply(clarsimp)
|
|
apply(rule le_trans)
|
|
apply assumption
|
|
apply simp
|
|
done
|
|
|
|
lemma ipurge_shortens:
|
|
"length(ipurge u as s) \<le> length as"
|
|
apply(auto simp add:gen_purge_shortens ipurge_def)
|
|
done
|
|
|
|
|
|
lemma INT_cong':
|
|
assumes a: "\<And> x. Q x \<Longrightarrow> P x = P' x"
|
|
shows
|
|
"\<Inter>{P x|x. Q x} = \<Inter>{P' x|x. Q x}"
|
|
apply (auto simp: a)
|
|
done
|
|
|
|
|
|
text {* Standard Noninterfernce *}
|
|
|
|
definition
|
|
Noninterference :: "bool" where
|
|
"Noninterference \<equiv>
|
|
\<forall> u as s. reachable s \<longrightarrow>
|
|
(obs_equiv s as s (ipurge u as {s}) u)"
|
|
|
|
lemma obs_equiv_trans:
|
|
"\<lbrakk>reachable t; obs_equiv s as t bs u; obs_equiv t bs x cs u\<rbrakk> \<Longrightarrow> obs_equiv s as x cs u"
|
|
apply(clarsimp simp: obs_equiv_def Executable'_def)
|
|
apply(blast)
|
|
done
|
|
|
|
text {* Noninfluence -- the combination of Noninterference and
|
|
Nonleakage.
|
|
|
|
We add the assumption about equivalence wrt the scheduler's domain, as
|
|
is common in e.g. GVW.*}
|
|
definition
|
|
Noninfluence :: "bool" where
|
|
"Noninfluence \<equiv>
|
|
\<forall> u as s t. reachable s \<and> reachable t \<longrightarrow>
|
|
s \<approx>(sources as s u)\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow>
|
|
obs_equiv s as t (ipurge u as {t}) u"
|
|
|
|
|
|
lemma notin_policyI:
|
|
"\<lbrakk>dom a s \<notin> sources (a # list) s u; \<exists> s'. (s,s') \<in> Step a \<and> ua \<in> sources list s' u\<rbrakk> \<Longrightarrow>
|
|
(dom a s,ua) \<notin> policy"
|
|
apply(clarsimp simp: sources_Cons)
|
|
done
|
|
|
|
text {* This stronger condition is needed
|
|
to make the induction proof work for Noninterference. It can be viewed
|
|
as a generalisation of Noninfluence; hence its name here.
|
|
*}
|
|
definition
|
|
Noninfluence_gen :: "bool" where
|
|
"Noninfluence_gen \<equiv>
|
|
\<forall> u as s ts. reachable s \<and> (\<forall> t \<in> ts. reachable t) \<longrightarrow>
|
|
(\<forall>t \<in> ts. s \<approx>(sources as s u)\<approx> t) \<longrightarrow> (\<forall>t \<in> ts. s \<sim>schedDomain\<sim> t) \<longrightarrow>
|
|
(\<forall>t \<in> ts. uwr_equiv s as t (ipurge u as ts) u)"
|
|
|
|
definition
|
|
Noninfluence_uwr :: "bool" where
|
|
"Noninfluence_uwr \<equiv>
|
|
\<forall> u as s t. reachable s \<and> reachable t \<longrightarrow>
|
|
s \<approx>(sources as s u)\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow>
|
|
uwr_equiv s as t (ipurge u as {t}) u"
|
|
|
|
definition
|
|
Noninfluence_strong_uwr :: "bool" where
|
|
"Noninfluence_strong_uwr \<equiv>
|
|
\<forall> u as bs s t. reachable s \<and> reachable t \<longrightarrow>
|
|
s \<approx>(sources as s u)\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow>
|
|
ipurge u as {s} = ipurge u bs {s} \<longrightarrow>
|
|
uwr_equiv s as t bs u"
|
|
|
|
|
|
|
|
|
|
definition output_consistent :: "bool" where
|
|
"output_consistent \<equiv> \<forall> u s s'. s \<sim>u\<sim> s' \<longrightarrow> (out u s = out u s')"
|
|
|
|
definition confidentiality_u_strong :: "bool" where
|
|
"confidentiality_u_strong \<equiv> \<forall> a u s t. reachable s \<and> reachable t \<longrightarrow>
|
|
s \<sim>schedDomain\<sim> t \<longrightarrow>
|
|
((dom a s \<leadsto> u) \<longrightarrow> s \<sim>dom a s\<sim> t) \<longrightarrow>
|
|
s \<sim>u\<sim> t \<longrightarrow>
|
|
(\<forall> s' t'. (s,s') \<in> Step a \<and> (t,t') \<in> Step a \<longrightarrow>
|
|
s' \<sim>u\<sim> t')"
|
|
|
|
|
|
definition integrity_u :: "bool" where
|
|
"integrity_u \<equiv> \<forall> a u s. reachable s \<longrightarrow>
|
|
(dom a s,u) \<notin> policy \<longrightarrow>
|
|
(\<forall> s'. (s,s') \<in> Step a \<longrightarrow> s \<sim>u\<sim> s')"
|
|
|
|
(*<*)
|
|
(* integrity_u actually guarantees this (seemingly) stronger condition *)
|
|
definition integrity_u_more :: "bool" where
|
|
"integrity_u_more \<equiv> \<forall> a u s. reachable s \<longrightarrow>
|
|
(dom a s,u) \<notin> policy \<longrightarrow>
|
|
(\<forall> s' t. s \<sim>u\<sim> t \<and> (s,s') \<in> Step a \<longrightarrow> s' \<sim>u\<sim> t)"
|
|
|
|
lemma integrity_u_more:
|
|
"integrity_u \<Longrightarrow> integrity_u_more"
|
|
apply(clarsimp simp: integrity_u_more_def integrity_u_def)
|
|
apply(blast dest: uwr_sym uwr_trans)
|
|
done
|
|
|
|
|
|
lemma integrity_uD:
|
|
"\<lbrakk>integrity_u; reachable s; (dom a s,u) \<notin> policy;
|
|
s \<sim>u\<sim> t; (s,s') \<in> Step a\<rbrakk> \<Longrightarrow>
|
|
s' \<sim>u\<sim> t"
|
|
apply(drule integrity_u_more)
|
|
apply(simp add: integrity_u_more_def)
|
|
done
|
|
|
|
|
|
|
|
|
|
text {*
|
|
A weaker version of @{prop confidentiality_u_strong} that, with
|
|
@{prop integrity_u}, implies it.
|
|
*}
|
|
definition confidentiality_u where
|
|
"confidentiality_u \<equiv> \<forall> a u s t. reachable s \<and> reachable t \<longrightarrow>
|
|
s \<sim>schedDomain\<sim> t \<longrightarrow> dom a s \<leadsto> u \<longrightarrow> s \<sim>(dom a s)\<sim> t \<longrightarrow>
|
|
s \<sim>u\<sim> t \<longrightarrow>
|
|
(\<forall> s' t'. (s,s') \<in> Step a \<and> (t,t') \<in> Step a \<longrightarrow> s' \<sim>u\<sim> t')"
|
|
|
|
lemma impCE':
|
|
"\<lbrakk>P \<longrightarrow> Q; \<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R; \<not> P \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
|
|
apply auto
|
|
done
|
|
|
|
lemma confidentiality_u:
|
|
"\<lbrakk>confidentiality_u; integrity_u\<rbrakk> \<Longrightarrow>
|
|
confidentiality_u_strong"
|
|
apply(clarsimp simp: confidentiality_u_strong_def)
|
|
apply(erule impCE')
|
|
apply(subst (asm) confidentiality_u_def, blast)
|
|
apply(frule integrity_uD, simp+)
|
|
apply(drule_tac s=t and t="s'" in integrity_uD)
|
|
apply assumption
|
|
apply(drule_tac e=a in schedIncludesCurrentDom)
|
|
apply simp
|
|
apply(blast intro: uwr_sym)
|
|
apply assumption
|
|
apply(erule uwr_sym)
|
|
done
|
|
|
|
lemma obs_equivI:
|
|
"\<lbrakk>output_consistent; uwr_equiv s as t bs ob\<rbrakk> \<Longrightarrow> obs_equiv s as t bs ob"
|
|
apply(clarsimp simp: obs_equiv_def)
|
|
apply(auto simp: uwr_equiv_def output_consistent_def)
|
|
done
|
|
|
|
lemma Noninfluence_uwr_Noninfluence:
|
|
"\<lbrakk>output_consistent; Noninfluence_uwr\<rbrakk> \<Longrightarrow> Noninfluence"
|
|
apply(clarsimp simp: Noninfluence_def)
|
|
apply(erule obs_equivI)
|
|
apply(auto simp: Noninfluence_uwr_def)
|
|
done
|
|
|
|
|
|
lemma sched_equiv_preserved:
|
|
"\<lbrakk>confidentiality_u_strong; reachable s; reachable t;
|
|
s \<sim>schedDomain\<sim> t; (s,s') \<in> Step a; (t,t') \<in> Step a\<rbrakk> \<Longrightarrow>
|
|
s' \<sim>schedDomain\<sim> t'"
|
|
apply(case_tac "dom a s = schedDomain")
|
|
apply(subst (asm) confidentiality_u_strong_def)
|
|
apply(drule_tac x=a in spec)
|
|
apply(drule_tac x=schedDomain in spec)
|
|
apply(drule_tac x=s in spec)
|
|
apply(drule_tac x=t in spec)
|
|
apply blast
|
|
apply(subst (asm) confidentiality_u_strong_def)
|
|
apply(blast intro: schedNotGlobalChannel)
|
|
done
|
|
|
|
lemma sched_equiv_preserved_left:
|
|
"\<lbrakk>integrity_u; s \<sim>schedDomain\<sim> t;
|
|
dom a s \<noteq> schedDomain; (s,s') \<in> Step a; reachable s\<rbrakk> \<Longrightarrow>
|
|
s' \<sim>schedDomain\<sim> t"
|
|
apply(blast intro: integrity_uD schedNotGlobalChannel)
|
|
done
|
|
|
|
lemma Noninfluence_gen_Noninterference:
|
|
"\<lbrakk>output_consistent; Noninfluence_gen\<rbrakk> \<Longrightarrow> Noninterference"
|
|
apply(clarsimp simp: Noninterference_def Noninfluence_gen_def)
|
|
apply(erule_tac x=u in allE)
|
|
apply(erule_tac x=as in allE)
|
|
apply(erule_tac x=s in allE)
|
|
apply(erule_tac x="{s}" in allE)
|
|
apply(clarsimp simp: sameFor_dom_def uwr_refl Executable_Executable'_equiv)
|
|
apply(blast intro: obs_equivI)
|
|
done
|
|
|
|
lemma Noninfluence_gen_Noninfluence:
|
|
"\<lbrakk>output_consistent; Noninfluence_gen\<rbrakk> \<Longrightarrow> Noninfluence"
|
|
apply(clarsimp simp: Noninfluence_def Noninfluence_gen_def)
|
|
apply(erule_tac x=u in allE)
|
|
apply(erule_tac x=as in allE)
|
|
apply(erule_tac x=s in allE)
|
|
apply(erule_tac x="{t}" in allE)
|
|
apply(clarsimp simp:uwr_refl)
|
|
apply(blast intro: obs_equivI)
|
|
done
|
|
|
|
lemma Noninfluence_gen_Noninfluence_uwr:
|
|
"\<lbrakk>Noninfluence_gen\<rbrakk> \<Longrightarrow> Noninfluence_uwr"
|
|
apply(clarsimp simp: Noninfluence_uwr_def Noninfluence_gen_def)
|
|
done
|
|
|
|
end
|
|
|
|
(* we define the unwinding conditions for any system *)
|
|
locale unwinding_system = Step_system A + noninterference_policy dom uwr policy out schedDomain
|
|
for A :: "('a,'s,'e) data_type"
|
|
and dom :: "'e \<Rightarrow> 's \<Rightarrow> 'd"
|
|
and uwr :: "'d \<Rightarrow> ('s \<times> 's) set"
|
|
and policy :: "('d \<times> 'd) set"
|
|
and out :: "'d \<Rightarrow> 's \<Rightarrow> 'p"
|
|
and schedDomain :: "'d"
|
|
|
|
|
|
|
|
sublocale unwinding_system \<subseteq> noninterference_system
|
|
apply(unfold_locales)
|
|
done
|
|
|
|
context unwinding_system begin
|
|
|
|
(* This is our unwinding condition on executability *)
|
|
definition executable_u where
|
|
"executable_u \<equiv> \<forall>s t a. reachable s \<and> reachable t \<and> (s,t)\<in>uwr schedDomain \<and> (\<exists>s'. (s,s')\<in>Step a) \<longrightarrow> (\<exists>t'. (t,t')\<in>Step a)"
|
|
|
|
|
|
lemma executable_uD:
|
|
"\<lbrakk>executable_u; reachable s; reachable t; (s,s')\<in>Step a; (s,t)\<in> uwr schedDomain\<rbrakk> \<Longrightarrow> \<exists>t'. (t,t')\<in>Step a"
|
|
apply(fastforce simp:executable_u_def)
|
|
done
|
|
|
|
(* We immediatly derive a global version *)
|
|
lemma Executable_u[rule_format]:
|
|
"\<lbrakk>executable_u ; confidentiality_u_strong ; reachable s ; reachable t ; s \<sim>schedDomain\<sim> t
|
|
; Executable as s\<rbrakk> \<Longrightarrow> Executable as t"
|
|
apply(induct as arbitrary:s t)
|
|
apply simp_all
|
|
apply(blast intro:reachable_Step sched_equiv_preserved dest:executable_uD)
|
|
done
|
|
|
|
(* The symmetric/negative version*)
|
|
lemma not_Executable_u[rule_format]:
|
|
"\<lbrakk>executable_u; confidentiality_u_strong ; reachable s ; reachable t ; s \<sim>schedDomain\<sim> t
|
|
; \<not>(Executable as s) \<rbrakk> \<Longrightarrow> \<not>(Executable as t)"
|
|
apply(blast intro: Executable_u uwr_sym)
|
|
done
|
|
|
|
|
|
lemma sources_refl:
|
|
"u \<in> sources as s u"
|
|
apply(case_tac as)
|
|
by (auto simp: sources_Nil sources_Cons)
|
|
|
|
|
|
lemma schedDomain_in_sources_Cons:
|
|
"(s,s')\<in> Step a \<Longrightarrow> dom a s = schedDomain \<Longrightarrow> dom a s \<in> sources (a#as) s u"
|
|
apply(unfold sources_Cons)
|
|
apply(erule ssubst)
|
|
apply(rule UnI1)
|
|
apply(rule UnI2)
|
|
apply(clarsimp)
|
|
apply(rule_tac x=u in exI)
|
|
apply(safe)
|
|
apply(rule schedFlowsToAll)
|
|
apply(blast intro:sources_refl)
|
|
done
|
|
|
|
|
|
lemma insert_eq:
|
|
"u=v ==> s=t ==> insert u s = insert v t"
|
|
apply auto
|
|
done
|
|
|
|
lemma notin_sources_ConsD[rule_format]:
|
|
"dom a s \<notin> sources (a#as) s u --> (\<forall>s'. (s,s')\<in>Step a \<longrightarrow> dom a s \<notin> sources as s' u) & (\<forall>s' v. (dom a s,v)\<notin>policy \<or> (s,s') \<notin> Step a \<or> v \<notin> sources as s' u)"
|
|
apply (clarsimp simp: sources_Cons)
|
|
apply blast
|
|
done
|
|
|
|
|
|
lemma sources_eq':
|
|
"executable_u \<and> confidentiality_u_strong \<and> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t \<longrightarrow> sources as s u = sources as t u"
|
|
apply(induct as arbitrary:s t)
|
|
apply(simp add:sources_Nil)
|
|
apply(clarsimp simp:sources_Cons)
|
|
apply(rule insert_eq,blast)
|
|
apply(rule un_eq)
|
|
apply(rule set_eqI, rule iffI)
|
|
apply(clarsimp,rule_tac x="sources as s' u" in exI,simp)
|
|
apply(frule executable_uD,simp_all)
|
|
apply(blast intro:reachable_Step sched_equiv_preserved)
|
|
apply(clarsimp,rule_tac x="sources as s' u" in exI,simp)
|
|
apply(frule_tac s=t in executable_uD,simp_all)
|
|
apply(blast intro:uwr_sym)
|
|
apply(blast intro:reachable_Step sched_equiv_preserved)
|
|
apply safe
|
|
apply(blast intro: schedIncludesCurrentDom)
|
|
apply(rule_tac x=v in exI)
|
|
apply(frule_tac e=a in schedIncludesCurrentDom,simp)
|
|
apply(drule executable_uD,simp_all,clarsimp)
|
|
apply(blast intro:reachable_Step sched_equiv_preserved)
|
|
apply(blast intro: schedIncludesCurrentDom sym)
|
|
apply(rule_tac x=v in exI)
|
|
apply(frule_tac e=a in schedIncludesCurrentDom,simp)
|
|
apply(drule_tac s=t in executable_uD,simp_all, clarsimp simp:uwr_sym)
|
|
apply(blast intro:reachable_Step sched_equiv_preserved)
|
|
done
|
|
|
|
lemma sources_eq:
|
|
"\<lbrakk>executable_u; confidentiality_u_strong; s \<sim>schedDomain\<sim> t; reachable s; reachable t\<rbrakk> \<Longrightarrow>
|
|
sources as s u = sources as t u"
|
|
apply(rule sources_eq'[rule_format],simp)
|
|
done
|
|
|
|
|
|
lemma sameFor_sources_dom:
|
|
"\<lbrakk>s \<approx>(sources (a#as) s u)\<approx> t; dom a s \<leadsto> x; x \<in> sources as s' u; (s,s') \<in> Step a\<rbrakk> \<Longrightarrow>
|
|
s \<sim>(dom a s)\<sim> t"
|
|
apply(simp add: sameFor_dom_def)
|
|
apply(erule bspec)
|
|
apply(subst sources_Cons)
|
|
apply blast
|
|
done
|
|
|
|
lemma sources_unwinding_step:
|
|
"\<lbrakk>s \<approx>(sources (a#as) s u)\<approx> t; s \<sim>schedDomain\<sim> t; confidentiality_u_strong;
|
|
(s,s') \<in> Step a; (t,t') \<in> Step a; reachable s; reachable t\<rbrakk> \<Longrightarrow>
|
|
s' \<approx>(sources as s' u)\<approx> t'"
|
|
apply(clarsimp simp: sameFor_dom_def sources_Cons)
|
|
apply(fastforce simp: confidentiality_u_strong_def)
|
|
done
|
|
|
|
lemma ex_bex_comm:
|
|
"\<exists>y\<in>s. \<exists>x. P x y \<Longrightarrow> \<exists>x. \<exists>y\<in> s. P x y"
|
|
apply auto
|
|
done
|
|
|
|
lemma ipurge_break:
|
|
"ipurge u as {} = []"
|
|
apply(induct as)
|
|
apply(simp add:ipurge_Nil)
|
|
apply(simp add:ipurge_Cons)
|
|
done
|
|
|
|
lemma ipurge_eq':
|
|
"(\<forall> s t. s\<in>ss \<and> t\<in>ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t) \<and>
|
|
((\<exists>s. s\<in>ss) = (\<exists>t. t\<in>ts)) \<and>
|
|
confidentiality_u_strong \<and> executable_u \<and> integrity_u
|
|
\<longrightarrow> ipurge u as ss = ipurge u as ts"
|
|
apply(induct as arbitrary: ss ts)
|
|
apply(simp add:ipurge_Nil)
|
|
apply(simp add:ipurge_Cons)
|
|
apply(intro conjI impI,elim conjE)
|
|
apply(drule_tac x="\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}" in meta_spec)
|
|
apply(drule_tac x="\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a}" in meta_spec)
|
|
apply(erule impE)
|
|
apply clarsimp
|
|
apply(intro allI conjI impI, elim conjE bexE)
|
|
apply(drule_tac x=sc in spec, drule_tac x=sd in spec)
|
|
apply(fastforce dest: sched_equiv_preserved)
|
|
apply(elim conjE bexE,
|
|
drule_tac x=sc in spec, drule_tac x=sd in spec,
|
|
fastforce intro: reachable_Step)+
|
|
apply(erule iffE,erule impE,blast)
|
|
apply(rule iffI,rule ex_bex_comm,clarsimp)
|
|
apply(rule_tac x=t in bexI[rotated],assumption)
|
|
apply(rule executable_uD,simp_all)
|
|
apply blast
|
|
apply(clarsimp, rule ex_bex_comm)
|
|
apply(blast intro:executable_uD uwr_sym)
|
|
apply safe[1]
|
|
apply(drule_tac x=t in bspec,assumption)
|
|
apply(erule notE)
|
|
apply(drule_tac x=s in spec, drule_tac x=t in spec,clarsimp)
|
|
apply(frule_tac e=a in schedIncludesCurrentDom)
|
|
apply(erule subst,rule subst, rule sources_eq)
|
|
apply assumption+
|
|
apply(erule notE,blast)
|
|
apply safe[1]
|
|
apply(drule_tac x=sa in bspec,assumption)
|
|
apply(erule notE)
|
|
apply(drule_tac x=sa in spec, drule_tac x=s in spec,clarsimp)
|
|
apply(frule_tac e=a in schedIncludesCurrentDom)
|
|
apply(erule subst,rule subst, rule_tac s=s in sources_eq)
|
|
apply (assumption+,rule uwr_sym,assumption+)
|
|
apply(drule_tac e=a in schedIncludesCurrentDom)
|
|
apply simp
|
|
apply(erule notE,fastforce)
|
|
apply(blast intro: ipurge_break)
|
|
done
|
|
|
|
lemma ipurge_eq:
|
|
"\<lbrakk>s \<sim>schedDomain\<sim> t; reachable s; reachable t;
|
|
confidentiality_u_strong; executable_u; integrity_u\<rbrakk> \<Longrightarrow>
|
|
ipurge u as {s} = ipurge u as {t}"
|
|
apply(rule ipurge_eq'[rule_format], simp add: uwr_refl)
|
|
done
|
|
|
|
|
|
lemma dom_in_sources_Cons:
|
|
"\<lbrakk>confidentiality_u_strong; integrity_u; executable_u;
|
|
reachable s; reachable t;
|
|
s \<approx>(sources (a#as) s u)\<approx> t; s \<sim>schedDomain\<sim> t;
|
|
(dom a s \<in> sources (a#as) s u)\<rbrakk> \<Longrightarrow>
|
|
(dom a t \<in> sources (a#as) t u)"
|
|
apply(subgoal_tac "dom a s = dom a t")
|
|
apply(fastforce dest: sources_eq)
|
|
apply(blast intro: schedIncludesCurrentDom)
|
|
done
|
|
|
|
lemma dom_notin_sources_Cons:
|
|
"\<lbrakk>confidentiality_u_strong; integrity_u; executable_u;
|
|
reachable s; reachable t;
|
|
s \<approx>(sources (a#as) s u)\<approx> t; s \<sim>schedDomain\<sim> t;
|
|
(dom a s \<notin> sources (a#as) s u)\<rbrakk> \<Longrightarrow>
|
|
(dom a t \<notin> sources (a#as) t u)"
|
|
apply(subgoal_tac "dom a s = dom a t")
|
|
apply(fastforce dest: sources_eq)
|
|
apply(blast intro: schedIncludesCurrentDom)
|
|
done
|
|
|
|
|
|
lemma uwr_equiv_Cons_bothI:
|
|
"\<lbrakk>reachable s; reachable t; executable_u; (s,t)\<in>uwr schedDomain;
|
|
\<forall> s' t'. (s,s') \<in> Step a \<and> (t,t') \<in> Step a \<longrightarrow> uwr_equiv s' as t' bs u\<rbrakk> \<Longrightarrow>
|
|
uwr_equiv s (a # as) t (a # bs) u"
|
|
apply(clarsimp simp: uwr_equiv_def execution_Run)
|
|
apply(safe)
|
|
apply(frule Executable'D,fastforce)
|
|
apply(rule Executable'I,clarsimp)
|
|
apply(subst (asm) executable_u_def)
|
|
apply(blast intro:reachable_Step Executable'D Executable'I)
|
|
apply(fastforce simp:reachable_Step execution_Run Executable'_def)
|
|
done
|
|
|
|
lemma uwr_equiv_Cons_leftI:
|
|
"\<lbrakk>reachable s; \<forall> s'. (s,s') \<in> Step a \<longrightarrow> uwr_equiv s' as t bs u\<rbrakk> \<Longrightarrow>
|
|
uwr_equiv s (a # as) t bs u"
|
|
apply(clarsimp simp: uwr_equiv_def execution_Run reachable_Step Executable'_def)
|
|
apply blast
|
|
done
|
|
|
|
lemma uwr_equiv_eq:
|
|
"\<lbrakk>uwr_equiv s as t bs u; execution A t bs = execution A r cs; Executable cs r; Executable bs t\<rbrakk> \<Longrightarrow>
|
|
uwr_equiv s as r cs u"
|
|
apply(unfold uwr_equiv_def)
|
|
apply(blast intro: Executable'I)
|
|
done
|
|
|
|
|
|
lemma Executable_ipurge:
|
|
"\<lbrakk>confidentiality_u_strong; integrity_u; executable_u; reachable s; Executable as s; s\<in>ss\<rbrakk> \<Longrightarrow> Executable (ipurge u as ss) s"
|
|
apply(induct as arbitrary:s ss)
|
|
apply(simp add:ipurge_Nil)
|
|
apply(clarsimp simp: ipurge_Cons)
|
|
apply safe
|
|
apply(drule_tac x=s' in meta_spec, drule_tac x="(\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})" in meta_spec)
|
|
apply(blast intro:reachable_Step)
|
|
apply(drule_tac x=s in meta_spec, drule_tac x=ss in meta_spec)
|
|
apply simp
|
|
apply(drule impI, erule impE,simp_all)
|
|
apply(subgoal_tac "dom a s \<noteq> schedDomain")
|
|
apply(subgoal_tac "(s,s')\<in>uwr schedDomain")
|
|
apply(rule_tac s=s' in Executable_u)
|
|
apply(blast intro: reachable_Step uwr_sym)+
|
|
apply(rule integrity_uD[THEN uwr_sym],simp_all add: uwr_refl)
|
|
apply(blast intro: schedNotGlobalChannel)
|
|
apply(rule notI)
|
|
apply(frule schedDomain_in_sources_Cons,fastforce+)
|
|
done
|
|
|
|
|
|
(* Best. Proof. Ever. *)
|
|
lemma Noninfluence_gen:
|
|
"\<lbrakk>confidentiality_u_strong; integrity_u; executable_u\<rbrakk> \<Longrightarrow> Noninfluence_gen"
|
|
apply(subst Noninfluence_gen_def)
|
|
apply(rule allI, rule allI)
|
|
apply(induct_tac as)
|
|
apply(fastforce simp:Executable'I sameFor_dom_def ipurge_Nil sources_Nil uwr_equiv_def execution_Run)
|
|
apply(clarsimp simp: ipurge_Cons)
|
|
apply(intro conjI,clarsimp)
|
|
apply(rule uwr_equiv_Cons_bothI)
|
|
apply(blast+)[3]
|
|
apply(drule_tac x=t in bspec,assumption,blast)
|
|
apply clarsimp
|
|
apply(erule_tac x="s'" in allE,erule_tac x="\<Union>t\<in>ts. {t'. (t,t') \<in> Step a}" in allE)
|
|
apply(erule impE,blast intro: reachable_Step)
|
|
apply(erule impE,clarsimp,rename_tac ta tb)
|
|
apply(rule_tac t=ta in sources_unwinding_step,blast+)[1]
|
|
apply(erule impE,clarsimp,rename_tac ta tb)
|
|
apply(rule_tac s=s and t=ta in sched_equiv_preserved)
|
|
apply (simp_all)[6]
|
|
apply blast
|
|
apply clarsimp
|
|
apply(rule uwr_equiv_Cons_leftI,blast)
|
|
apply safe
|
|
apply(drule_tac x=s' in spec, drule_tac x=ts in spec)
|
|
apply(erule impE,blast intro: reachable_Step)
|
|
apply(erule impE,clarsimp simp: sameFor_dom_def)
|
|
apply(drule_tac x=x in bspec,assumption, drule_tac x=ua in bspec)
|
|
apply(fastforce simp: sources_Cons)
|
|
apply(subgoal_tac "dom a s \<notin> sources (a # list) s u")
|
|
apply(drule notin_sources_ConsD,clarsimp)
|
|
apply(erule_tac x=s' in allE, erule impE, assumption,erule_tac x=ua in allE)
|
|
apply(blast intro:integrity_uD)
|
|
apply(drule_tac x=t in bspec,assumption)+
|
|
apply(simp add: schedIncludesCurrentDom)
|
|
apply(subgoal_tac "sources (a # list) s u = sources (a # list) t u",blast)
|
|
apply(rule sources_eq,simp add: executable_u_def,assumption+)
|
|
apply(erule impE,clarsimp)
|
|
apply(rule integrity_uD,simp_all)
|
|
apply(case_tac "dom a s \<noteq> schedDomain")
|
|
apply(blast dest:schedNotGlobalChannel)
|
|
apply(drule_tac x=t in bspec,assumption)
|
|
apply(erule notE,subst sources_Cons)
|
|
apply(subst (asm) executable_u_def)
|
|
apply(erule_tac x=s in allE, erule_tac x=t in allE, erule_tac x=a in allE,simp)
|
|
apply(erule impE,blast)
|
|
apply(rule disjI2)+
|
|
apply(rule_tac x=u in exI)
|
|
apply(rule conjI)
|
|
apply(drule_tac x=t in bspec,assumption)+
|
|
apply(frule_tac e=a in schedIncludesCurrentDom,simp)
|
|
apply(rule schedFlowsToAll)
|
|
apply(fastforce simp:sources_refl)
|
|
done
|
|
|
|
|
|
lemma obs_equiv_Cons_bothI:
|
|
"\<lbrakk>reachable s; reachable t; executable_u; (s,t)\<in>uwr schedDomain;
|
|
\<forall> s' t'. (s,s') \<in> Step a \<and> (t,t') \<in> Step a \<longrightarrow> obs_equiv s' as t' bs u\<rbrakk> \<Longrightarrow>
|
|
obs_equiv s (a # as) t (a # bs) u"
|
|
apply(clarsimp simp: obs_equiv_def execution_Run)
|
|
apply(safe)
|
|
apply(frule Executable'D,fastforce)
|
|
apply(rule Executable'I,clarsimp)
|
|
apply(subst (asm) executable_u_def,erule_tac x=s in allE, erule_tac x=t in allE, erule_tac x=a in allE,clarsimp)
|
|
apply(erule impE,blast,clarsimp)
|
|
apply(drule_tac x=s' in spec, drule_tac x=t' in spec,safe)
|
|
apply(blast intro:Executable'I)
|
|
apply(blast intro:reachable_Step Executable'D)
|
|
apply(fastforce simp:reachable_Step execution_Run Executable'_def)
|
|
done
|
|
|
|
lemma Nonleakage:
|
|
"\<lbrakk>confidentiality_u_strong; executable_u; output_consistent\<rbrakk> \<Longrightarrow> Nonleakage"
|
|
apply(subst Nonleakage_def)
|
|
apply(rule allI)
|
|
apply(induct_tac as)
|
|
apply(clarsimp simp:obs_equiv_def)
|
|
apply(simp add: Executable'I execution_Run output_consistent_def sameFor_dom_def sources_refl)
|
|
apply(clarsimp)
|
|
apply(rule obs_equiv_Cons_bothI,assumption+)
|
|
apply(blast intro:reachable_Step sched_equiv_preserved sources_unwinding_step)
|
|
done
|
|
|
|
(*In fact, if as is executable, sources as s u matches the result of sources' as s u, where sources' is the usual formulation :*)
|
|
primrec
|
|
sources' :: "'e list \<Rightarrow> 's \<Rightarrow> 'd \<Rightarrow> 'd set" where
|
|
sources'_Nil: "sources' [] s u = {u}"|
|
|
sources'_Cons: "sources' (a#as) s u = (\<Union>{sources' as s' u| s'. (s,s') \<in> Step a}) \<union>
|
|
{w. w = dom a s \<and> (\<exists> v s'. dom a s \<leadsto> v \<and> (s,s') \<in> Step a \<and> v \<in> sources' as s' u)}"
|
|
|
|
declare sources'_Nil [simp del]
|
|
declare sources'_Cons [simp del]
|
|
|
|
lemma insert_eq_left:
|
|
"u\<in>s \<Longrightarrow> s = t \<Longrightarrow> insert u s = t"
|
|
apply auto
|
|
done
|
|
|
|
lemma sources'_refl:
|
|
"reachable s \<and> Executable as s \<Longrightarrow> u \<in> sources' as s u"
|
|
apply(induct as arbitrary: s)
|
|
apply(simp add: sources'_Nil)
|
|
apply(clarsimp simp: sources'_Cons)
|
|
apply(blast intro:reachable_Step)
|
|
done
|
|
|
|
lemma sources_sources'_equiv:
|
|
"\<lbrakk>executable_u; confidentiality_u_strong; reachable s; Executable as s\<rbrakk> \<Longrightarrow> sources as s u = sources' as s u"
|
|
apply(induct as arbitrary:s)
|
|
apply(simp add: sources'_Nil sources_Nil)
|
|
apply(simp add: sources'_Cons sources_Cons)
|
|
apply(rule insert_eq_left)
|
|
apply(rule UnI1)
|
|
apply clarsimp
|
|
apply(rule_tac x="sources as s' u" in exI)
|
|
apply(rule conjI,rule_tac x=s' in exI,simp)
|
|
apply(blast intro:reachable_Step sources'_refl)
|
|
apply(rule un_eq)
|
|
apply(rule set_eqI,rule iffI)
|
|
apply(clarsimp)
|
|
apply(rule_tac x="sources as s'a u" in exI,simp)
|
|
apply(rule_tac x=s'a in exI,simp)
|
|
apply(drule_tac x=s'a in meta_spec)
|
|
apply(frule_tac s'=s'a in reachable_Step,simp,simp)
|
|
apply(drule impI,erule impE)
|
|
apply(rule Executable_u,simp_all add:uwr_refl)
|
|
apply(blast intro:reachable_Step)
|
|
apply(rule sched_equiv_preserved,simp_all add:uwr_refl)
|
|
apply clarsimp
|
|
apply(rule_tac x="sources' as s'a u" in exI,simp)
|
|
apply(rule_tac x=s'a in exI,simp)
|
|
apply(drule_tac x=s'a in meta_spec)
|
|
apply(frule_tac s'=s'a in reachable_Step,simp,simp)
|
|
apply(drule impI,erule impE)
|
|
apply(rule Executable_u,simp_all add:uwr_refl)
|
|
apply(blast intro:reachable_Step)
|
|
apply(rule sched_equiv_preserved,simp_all add:uwr_refl)
|
|
apply safe
|
|
apply(rule_tac x=v in exI,simp)
|
|
apply(rule_tac x=s'a in exI,simp)
|
|
apply(drule_tac x=s'a in meta_spec)
|
|
apply(frule_tac s'=s'a in reachable_Step,simp,simp)
|
|
apply(drule impI,erule impE)
|
|
apply(rule Executable_u,simp_all add:uwr_refl)
|
|
apply(blast intro:reachable_Step)
|
|
apply(rule sched_equiv_preserved,simp_all add:uwr_refl)
|
|
apply(rule_tac x=v in exI,simp)
|
|
apply(rule_tac x=s'a in exI,simp)
|
|
apply(drule_tac x=s'a in meta_spec)
|
|
apply(frule_tac s'=s'a in reachable_Step,simp,simp)
|
|
apply(drule impI,erule impE)
|
|
apply(rule Executable_u,simp_all add:uwr_refl)
|
|
apply(blast intro:reachable_Step)
|
|
apply(rule sched_equiv_preserved,simp_all add:uwr_refl)
|
|
done
|
|
|
|
|
|
|
|
lemma Noninterference:
|
|
"\<lbrakk>confidentiality_u; output_consistent; integrity_u; executable_u\<rbrakk> \<Longrightarrow>
|
|
Noninterference"
|
|
apply(rule Noninfluence_gen_Noninterference)
|
|
apply assumption
|
|
apply(blast intro: Noninfluence_gen confidentiality_u)
|
|
done
|
|
|
|
lemma Noninfluence:
|
|
"\<lbrakk>confidentiality_u; output_consistent; integrity_u; executable_u\<rbrakk> \<Longrightarrow>
|
|
Noninfluence"
|
|
apply(rule Noninfluence_gen_Noninfluence)
|
|
apply assumption
|
|
apply(blast intro: Noninfluence_gen confidentiality_u)
|
|
done
|
|
|
|
|
|
lemma Noninfluence_uwr:
|
|
"\<lbrakk>confidentiality_u; integrity_u; executable_u\<rbrakk> \<Longrightarrow>
|
|
Noninfluence_uwr"
|
|
apply(rule Noninfluence_gen_Noninfluence_uwr)
|
|
apply(blast intro: Noninfluence_gen confidentiality_u)
|
|
done
|
|
|
|
|
|
lemma sources_Step:
|
|
"\<lbrakk>reachable s; (dom a s, u) \<notin> policy; (s,s')\<in>Step a\<rbrakk> \<Longrightarrow>
|
|
sources [a] s u = {u}"
|
|
apply(auto simp add: sources_Cons sources_Nil)
|
|
done
|
|
|
|
lemma sources_Step_2:
|
|
"\<lbrakk>reachable s; (dom a s, u) \<in> policy; (s,s')\<in>Step a\<rbrakk> \<Longrightarrow>
|
|
sources [a] s u = {dom a s,u}"
|
|
apply(auto simp: sources_Cons sources_Nil)
|
|
done
|
|
|
|
lemma execution_Nil:
|
|
"reachable s \<Longrightarrow> execution A s [] = {s}"
|
|
apply(simp add: execution_Run)
|
|
done
|
|
|
|
lemma execution_executable:
|
|
"s' \<in> execution A s [a] ==> (s,s')\<in>Step a"
|
|
apply(auto simp add: Step_def execution_Run)
|
|
done
|
|
|
|
lemma executable_execution:
|
|
"reachable s ==> (s,s')\<in>Step a ==> \<exists>s'. s' \<in> execution A s [a]"
|
|
apply(auto simp add: execution_Run)
|
|
done
|
|
|
|
lemma Noninfluence_gen_confidentiality_u:
|
|
"Noninfluence_gen \<Longrightarrow> confidentiality_u"
|
|
apply(clarsimp simp: Noninfluence_gen_def confidentiality_u_def)
|
|
apply(drule_tac x=u in spec, drule_tac x="[a]" in spec)
|
|
apply(drule_tac x=s in spec, drule_tac x="{t}" in spec)
|
|
apply(simp add: sources_Step_2 sameFor_dom_def uwr_equiv_def Step_def ipurge_Cons ipurge_Nil add: schedIncludesCurrentDom)
|
|
done
|
|
|
|
lemma Noninfluence_strong_uwr_confidentiality_u:
|
|
"Noninfluence_strong_uwr \<Longrightarrow> confidentiality_u"
|
|
apply(clarsimp simp: Noninfluence_strong_uwr_def confidentiality_u_def)
|
|
apply(drule_tac x=u in spec, drule_tac x="[a]" in spec, drule_tac x="[a]" in spec)
|
|
apply(drule_tac x=s in spec, drule_tac x=t in spec)
|
|
apply(simp add: sources_Step_2 sameFor_dom_def uwr_equiv_def Step_def)
|
|
done
|
|
|
|
|
|
(* A potentially useful lemma if executable_u changes and then Executable_u takes into account equivalency with respect to sources:
|
|
The equivalent of sources_unwinding_step if a is purged *)
|
|
lemma sources_unwinding_step_aux:
|
|
"\<lbrakk>s \<approx>(sources (a#as) s u)\<approx> t; s \<sim>schedDomain\<sim> t; integrity_u;
|
|
(s,s') \<in> Step a; reachable s; reachable t; dom a s \<notin>sources (a#as) s u\<rbrakk> \<Longrightarrow>
|
|
s' \<approx>(sources as s' u)\<approx> t"
|
|
apply(clarsimp simp: sameFor_dom_def sources_Cons)
|
|
apply(blast intro: integrity_uD)
|
|
done
|
|
|
|
(* with this lemma, 'sameFor_dom _ (sources as _ u) _' is (decreadingly) preserved through an sequence and its ipurge *)
|
|
lemma sources_unwinding_step2:
|
|
"\<lbrakk>s \<approx>(sources (a#as) s u)\<approx> t; s \<sim>schedDomain\<sim> t; integrity_u; confidentiality_u_strong; executable_u;
|
|
(s,s') \<in> Step a; reachable s; reachable t; dom a t \<notin>sources (a#as) t u\<rbrakk> \<Longrightarrow>
|
|
s' \<approx>(sources as s' u)\<approx> t"
|
|
apply(rule_tac s=s and t=t in sources_unwinding_step_aux,simp_all)
|
|
apply(subgoal_tac "dom a s = dom a t")
|
|
apply(fastforce dest: sources_eq)
|
|
apply(blast intro: schedIncludesCurrentDom)
|
|
done
|
|
|
|
|
|
(* Assuming the sequence of actions is executable,
|
|
the unwinding conditions imply that the sources of a sequence and its ipurge are the same*)
|
|
lemma sources_ipurge:
|
|
"s\<in>ss \<Longrightarrow> executable_u \<Longrightarrow> integrity_u \<Longrightarrow> confidentiality_u_strong \<Longrightarrow>
|
|
Executable as s\<Longrightarrow> sources (ipurge u as ss) s u = sources as s u"
|
|
apply(induct as arbitrary:s ss)
|
|
apply(clarsimp simp:sources_Nil ipurge_Nil)
|
|
apply(subst ipurge_Cons)
|
|
apply(case_tac "\<exists>s\<in>ss. dom a s \<in> sources (a # as) s u ")
|
|
defer
|
|
apply(clarsimp)
|
|
apply(drule_tac x=s in meta_spec,drule_tac x=ss in meta_spec)
|
|
apply(clarsimp)
|
|
apply(drule impI,erule impE)
|
|
apply(rule Executable_u,simp_all)
|
|
apply(blast intro:reachable_Step)
|
|
apply(drule_tac x=s in bspec,assumption)
|
|
apply(rule integrity_uD,simp_all)
|
|
apply(erule contrapos_nn)
|
|
apply(drule schedNotGlobalChannel)
|
|
apply(rule schedDomain_in_sources_Cons,simp_all add:uwr_refl)
|
|
apply(subgoal_tac "(dom a s, schedDomain) \<notin> policy")
|
|
apply(subst sources_Cons)
|
|
apply clarsimp
|
|
apply(rule insert_eq_left[THEN sym])
|
|
apply(blast intro:sources_refl)
|
|
apply(rule equalityI)
|
|
apply(clarsimp|rule conjI)+
|
|
apply(subst sources_eq,simp_all)
|
|
apply(rule uwr_sym)
|
|
apply(rule integrity_uD,simp_all add:uwr_refl)
|
|
apply(blast intro:reachable_Step)
|
|
apply clarsimp
|
|
apply(drule_tac x=s in bspec,assumption)
|
|
apply(drule notin_sources_ConsD,blast)
|
|
apply(rule subsetI)
|
|
apply(rule UnI1,simp)
|
|
apply(rule_tac x="sources as s u" in exI,simp)
|
|
apply(rule_tac x=s' in exI,simp)
|
|
apply(rule sources_eq,simp_all)
|
|
apply(rule integrity_uD[THEN uwr_sym],simp_all add:uwr_refl)
|
|
apply(blast intro:reachable_Step)
|
|
apply(drule_tac x=s in bspec,assumption)
|
|
apply(erule contrapos_nn)
|
|
apply(drule schedNotGlobalChannel)
|
|
apply(rule schedDomain_in_sources_Cons,simp_all)
|
|
apply(clarsimp)
|
|
apply(subst sources_Cons)+
|
|
apply(rule un_eq,simp_all)
|
|
apply(rule un_eq)
|
|
apply(rule set_eqI,rule iffI)
|
|
apply clarsimp
|
|
apply(rule_tac x="sources (ipurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})) s'a u" in exI,simp)
|
|
apply(rule_tac x=s'a in exI,simp)
|
|
apply(drule_tac x=s'a in meta_spec,drule_tac x="\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}" in meta_spec)
|
|
apply(drule_tac t=s'a in Executable_u,simp_all)
|
|
apply(blast intro:reachable_Step)+
|
|
apply(blast intro:sched_equiv_preserved uwr_refl)
|
|
apply simp
|
|
apply(drule impI,erule impE,blast,blast)
|
|
apply clarsimp
|
|
apply(rule_tac x="sources as s'a u" in exI,simp)
|
|
apply(rule_tac x=s'a in exI,simp)
|
|
apply(drule_tac x=s'a in meta_spec,drule_tac x="\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}" in meta_spec)
|
|
apply(drule_tac t=s'a in Executable_u,simp_all)
|
|
apply(blast intro:reachable_Step)+
|
|
apply(blast intro:sched_equiv_preserved uwr_refl)
|
|
apply simp
|
|
apply(drule impI,erule impE,blast,blast)
|
|
apply safe
|
|
apply(rule_tac x=v in exI,simp)
|
|
apply(rule_tac x=s'a in exI,simp)
|
|
apply(drule_tac x=s'a in meta_spec,drule_tac x="\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}" in meta_spec,simp)
|
|
apply(drule_tac t=s'a in Executable_u,simp_all)
|
|
apply(blast intro:reachable_Step)+
|
|
apply(blast intro:sched_equiv_preserved uwr_refl,simp)
|
|
apply(drule impI,erule impE,blast)
|
|
apply blast
|
|
apply(rule_tac x=v in exI,simp)
|
|
apply(rule_tac x=s'a in exI,simp)
|
|
apply(drule_tac x=s'a in meta_spec,drule_tac x="\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}" in meta_spec,simp)
|
|
apply(drule_tac t=s'a in Executable_u,simp_all)
|
|
apply(blast intro:reachable_Step)+
|
|
apply(blast intro:sched_equiv_preserved uwr_refl,simp)
|
|
apply(drule impI,erule impE,blast)
|
|
apply blast
|
|
done
|
|
|
|
(*Using the previous lemma, we can show that ipurge is idempotent,assuming the sequence is executable*)
|
|
lemma ipurge_idem':
|
|
"s\<in>ss \<longrightarrow> executable_u \<longrightarrow> integrity_u \<longrightarrow> confidentiality_u_strong \<longrightarrow>
|
|
Ball ss reachable \<longrightarrow> Ball ss (Executable as) \<longrightarrow>
|
|
(\<forall>s t. s\<in>ss \<and>t\<in>ss \<longrightarrow> (s,t)\<in>uwr schedDomain) \<longrightarrow>
|
|
ipurge u (ipurge u as ss) ss = ipurge u as ss"
|
|
apply(induct as arbitrary: s ss)
|
|
apply(simp add:ipurge_Nil)
|
|
apply(subst ipurge_Cons)+
|
|
apply(case_tac "\<exists>s\<in>ss. dom a s \<in> sources (a # as) s u")
|
|
apply clarsimp
|
|
apply(subst ipurge_Cons)
|
|
apply(case_tac "\<exists>s\<in>ss. dom a s \<in> sources (a # ipurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})) s u")
|
|
apply clarsimp
|
|
apply(drule_tac x=sa in bspec,assumption,clarsimp)
|
|
apply(drule_tac x=s' in meta_spec,drule_tac x="\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}" in meta_spec)
|
|
apply(erule impE,blast intro:reachable_Step)
|
|
apply(erule impE,blast intro:reachable_Step)
|
|
apply(erule impE,clarsimp,rule Executable_u,simp_all)
|
|
apply(blast intro:reachable_Step)
|
|
apply(blast intro:reachable_Step)
|
|
apply(rule sched_equiv_preserved,simp_all)
|
|
apply(erule impE,blast intro:sched_equiv_preserved)
|
|
apply blast
|
|
apply(drule_tac x=sa in bspec,assumption) back back
|
|
apply(subst (asm) sources_ipurge[THEN sym],simp_all)
|
|
apply(subst (asm)ipurge_Cons)
|
|
apply(case_tac " \<exists>s\<in>ss. dom a s \<in> sources (a # as) s u")
|
|
apply clarsimp
|
|
apply clarsimp
|
|
apply(drule notin_sources_ConsD)
|
|
apply(drule_tac x=sa in bspec,assumption)+
|
|
apply clarsimp
|
|
apply(drule_tac x=s' in spec,simp)+
|
|
apply(subst (asm) sources_ipurge,simp_all)
|
|
apply(rule Executable_u,simp_all)
|
|
apply(blast intro:reachable_Step)
|
|
apply(rule integrity_uD,simp_all)
|
|
apply(erule contrapos_nn)
|
|
apply(drule schedNotGlobalChannel)
|
|
apply(rule schedDomain_in_sources_Cons,simp_all)
|
|
apply(frule notin_sources_ConsD,clarsimp)
|
|
apply(drule_tac x=s' in spec,simp)+
|
|
apply(erule notE,subst sources_eq,simp_all) back
|
|
apply(rule integrity_uD,simp_all)
|
|
apply(erule contrapos_nn)
|
|
apply(drule schedNotGlobalChannel)
|
|
apply(rule schedDomain_in_sources_Cons,simp_all)
|
|
apply(blast intro:reachable_Step)
|
|
apply(subgoal_tac "sources as s' u = sources as sa u")
|
|
apply(simp)
|
|
apply(rule sources_eq,simp_all)
|
|
apply(rule integrity_uD,simp_all)
|
|
apply(erule contrapos_nn)
|
|
apply(drule schedNotGlobalChannel)
|
|
apply(rule schedDomain_in_sources_Cons,simp_all)
|
|
apply(blast intro:reachable_Step)
|
|
apply clarsimp
|
|
apply(drule_tac x=s in meta_spec, drule_tac x=ss in meta_spec,simp_all)
|
|
apply(erule impE,clarsimp)
|
|
apply(drule_tac x=s in bspec,assumption,erule exE,clarsimp)
|
|
apply(rule_tac s=s' in Executable_u,simp_all)
|
|
apply(blast intro:reachable_Step)
|
|
apply(rule integrity_uD,simp_all)
|
|
apply(drule_tac x=s in bspec,assumption)
|
|
apply(erule contrapos_nn)
|
|
apply(drule schedNotGlobalChannel)
|
|
apply(rule schedDomain_in_sources_Cons,simp_all)
|
|
done
|
|
|
|
|
|
lemma ipurge_idem:
|
|
"executable_u \<Longrightarrow> integrity_u \<Longrightarrow> confidentiality_u_strong \<Longrightarrow>
|
|
Executable as s \<Longrightarrow>
|
|
ipurge u (ipurge u as {s}) {s} = ipurge u as {s}"
|
|
apply(rule ipurge_idem'[rule_format],simp_all add:uwr_refl)
|
|
apply(case_tac as,simp_all)
|
|
done
|
|
|
|
|
|
(* When we delete the executability assumption, we still have an inclusion*)
|
|
lemma sources_subset_sources_ipurge:
|
|
"s\<in>ss \<Longrightarrow> reachable s \<Longrightarrow> executable_u \<Longrightarrow> integrity_u \<Longrightarrow> confidentiality_u_strong \<Longrightarrow>
|
|
sources as s u \<subseteq> sources (ipurge u as ss) s u"
|
|
apply(induct as arbitrary:s ss)
|
|
apply(simp add:sources_Nil ipurge_Nil)
|
|
apply(subst ipurge_Cons)
|
|
apply(case_tac "\<exists>s\<in>ss. dom a s \<in> sources (a # as) s u")
|
|
apply(clarsimp)
|
|
apply(subst (asm) sources_Cons)
|
|
apply safe[1]
|
|
apply(drule_tac x=s' in meta_spec,drule_tac x="\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}" in meta_spec,simp)
|
|
apply(frule reachable_Step,simp,simp)
|
|
apply(drule impI,erule impE,blast)
|
|
apply(rule subsetD,simp_all)
|
|
apply(erule subset_trans)
|
|
apply(subst sources_Cons)
|
|
apply(rule subsetI)
|
|
apply(rule UnI1)+
|
|
apply clarsimp
|
|
apply(rule_tac x="sources (ipurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})) s' u" in exI,simp,blast)
|
|
apply(subst sources_Cons)
|
|
apply(rule UnI1,rule UnI2)
|
|
apply clarsimp
|
|
apply(rule_tac x=v in exI,simp)
|
|
apply(rule_tac x=s' in exI,simp)
|
|
apply(drule_tac x=s' in meta_spec,drule_tac x="\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}" in meta_spec)
|
|
apply(blast intro:reachable_Step)
|
|
apply(rule sources_refl)
|
|
apply(drule_tac x=s in bspec,assumption)
|
|
apply(drule notin_sources_ConsD,clarsimp)
|
|
apply(subst (asm) sources_Cons,clarsimp)
|
|
apply safe
|
|
apply(rule sources_refl)
|
|
apply(drule_tac x=s in meta_spec, drule_tac x=ss in meta_spec,simp)
|
|
apply(rule subsetD,simp)
|
|
apply(subst sources_eq,simp_all)
|
|
apply(rule integrity_uD[THEN uwr_sym],simp_all add:uwr_refl)
|
|
apply(drule_tac x=s' in spec,simp)+
|
|
apply(rule notI,drule schedNotGlobalChannel)
|
|
apply(erule_tac x=u in allE,erule impE,simp add:schedFlowsToAll)
|
|
apply(blast intro:sources_refl)
|
|
apply(blast intro:reachable_Step)
|
|
done
|
|
|
|
(* the previous inclusion if sufficient to prove that ipurge is idempotent, even if the sequence is not executable *)
|
|
lemma ipurge_idemp_gen:
|
|
"s\<in>ss \<longrightarrow> executable_u \<longrightarrow> integrity_u \<longrightarrow> confidentiality_u_strong \<longrightarrow>
|
|
Ball ss reachable \<longrightarrow>
|
|
ipurge u (ipurge u as ss) ss = ipurge u as ss"
|
|
apply(induct as arbitrary: s ss)
|
|
apply(simp add:ipurge_Nil)
|
|
apply(subst ipurge_Cons)+
|
|
apply(case_tac "\<exists>s\<in>ss. dom a s \<in> sources (a # as) s u")
|
|
apply clarsimp
|
|
apply(subst ipurge_Cons)
|
|
apply(case_tac "\<exists>s\<in>ss. dom a s \<in> sources (a # ipurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})) s u")
|
|
apply clarsimp
|
|
apply(case_tac "\<exists>s'. s'\<in>(\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})")
|
|
apply clarsimp
|
|
apply(drule_tac x=s' in meta_spec, drule_tac x="\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}" in meta_spec)
|
|
apply(erule impE,blast)
|
|
apply(erule impE,blast intro:reachable_Step)
|
|
apply blast
|
|
apply(clarsimp simp:ipurge_break)
|
|
apply clarsimp
|
|
apply(subst (asm) sources_Cons,clarsimp)
|
|
apply(erule disjE)
|
|
apply(drule_tac x=s in bspec,assumption, blast intro:sources_refl)
|
|
apply(erule disjE,clarsimp)
|
|
apply(drule_tac x=sa in bspec,assumption,drule notin_sources_ConsD,clarsimp)
|
|
apply(drule_tac x=s' in spec,simp)+
|
|
apply(cut_tac s=s' and u=u and as=as and ss="\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}" in sources_subset_sources_ipurge,simp_all)
|
|
apply(blast)
|
|
apply(blast intro:reachable_Step)
|
|
apply(drule subsetD,assumption,blast)
|
|
apply clarsimp
|
|
apply(drule_tac x=sa in bspec,assumption,drule notin_sources_ConsD)
|
|
apply clarsimp
|
|
apply(drule_tac x=s' in spec,simp)+
|
|
apply(drule_tac x=v in spec,simp)
|
|
apply(cut_tac s=s' and u=u and as=as and ss="\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}" in sources_subset_sources_ipurge,simp_all)
|
|
apply(blast)
|
|
apply(blast intro:reachable_Step)
|
|
apply(drule subsetD,assumption,blast)
|
|
done
|
|
|
|
lemma ipurge_idemp:
|
|
"executable_u \<Longrightarrow> integrity_u \<Longrightarrow> confidentiality_u_strong \<Longrightarrow>
|
|
reachable s \<Longrightarrow> ipurge u (ipurge u as {s}) {s} = ipurge u as {s}"
|
|
apply(rule ipurge_idemp_gen[rule_format])
|
|
apply(auto simp add:uwr_refl)
|
|
done
|
|
|
|
|
|
(* This is the kind of lemma we would need with any unwinding condition *)
|
|
lemma dom_dom_in_policy_example[rule_format]:
|
|
"executable_u \<longrightarrow> confidentiality_u_strong \<longrightarrow> integrity_u\<longrightarrow>
|
|
reachable s \<longrightarrow> Executable (b#as) s \<longrightarrow> (s,s')\<in>Step a \<longrightarrow> (\<not> Executable (b#as) s') \<longrightarrow>
|
|
dom a s \<notin> sources (a#b#as) s u \<longrightarrow>
|
|
(dom a s,dom b s)\<in>policy"
|
|
apply clarsimp
|
|
apply(frule_tac s'=s' in reachable_Step,simp+)
|
|
apply(subgoal_tac "\<exists>t'. (s',t')\<in>Step b")
|
|
apply(clarsimp,drule_tac x=t' in spec,simp)
|
|
apply(erule notE,rule Executable_u,simp_all)
|
|
apply(blast intro:reachable_Step)+
|
|
apply(rule sched_equiv_preserved,simp_all)
|
|
apply(rule integrity_uD[THEN uwr_sym],simp_all)
|
|
apply(erule contrapos_nn,drule schedNotGlobalChannel)
|
|
apply(rule schedDomain_in_sources_Cons,simp_all add:uwr_refl)
|
|
apply(rule executable_uD,simp_all)
|
|
apply(rule integrity_uD[THEN uwr_sym],simp_all)
|
|
apply(erule contrapos_nn,drule schedNotGlobalChannel)
|
|
apply(rule schedDomain_in_sources_Cons,simp_all add:uwr_refl)
|
|
done
|
|
|
|
|
|
|
|
(* we just define 'enabled' here to show it is preserved by our refinement *)
|
|
|
|
definition enabled where
|
|
"enabled \<equiv> (\<forall>s a. reachable s \<longrightarrow> (\<exists>s'. (s,s')\<in>Step a))"
|
|
|
|
lemma enabled_executable_u:
|
|
"enabled \<Longrightarrow> executable_u"
|
|
apply(clarsimp simp:enabled_def executable_u_def)
|
|
done
|
|
|
|
lemma ipurge_idem_enabled:
|
|
"enabled \<Longrightarrow> integrity_u \<Longrightarrow> confidentiality_u_strong \<Longrightarrow>
|
|
reachable s \<Longrightarrow>
|
|
ipurge u (ipurge u as {s}) {s} = ipurge u as {s}"
|
|
apply(rule ipurge_idemp,simp_all)
|
|
apply(blast intro:enabled_executable_u)
|
|
done
|
|
|
|
end
|
|
|
|
|
|
locale complete_unwinding_system = unwinding_system +
|
|
assumes policy_refl:
|
|
"(u,u) \<in> policy"
|
|
|
|
context complete_unwinding_system begin
|
|
|
|
lemma Noninfluence_gen_integrity_u:
|
|
"Noninfluence_gen \<Longrightarrow> integrity_u"
|
|
apply(clarsimp simp: Noninfluence_gen_def integrity_u_def)
|
|
apply(drule_tac x=u in spec, drule_tac x="[a]" in spec)
|
|
apply(drule_tac x=s in spec, drule_tac x="{s}" in spec)
|
|
apply(simp add: sources_Step sameFor_dom_def uwr_equiv_def Step_def ipurge_Cons ipurge_Nil add: uwr_refl policy_refl execution_Nil uwr_sym)
|
|
apply(case_tac "dom a s=u")
|
|
apply(clarsimp simp:Executable'_def ipurge_Nil policy_refl)+
|
|
apply(fastforce simp:execution_Run uwr_sym)
|
|
done
|
|
|
|
|
|
lemma Noninfluence_strong_uwr_integrity_u: "Noninfluence_strong_uwr \<Longrightarrow> integrity_u"
|
|
apply(clarsimp simp: Noninfluence_strong_uwr_def integrity_u_def)
|
|
apply(drule_tac x=u in spec, drule_tac x="[a]" in spec, drule_tac x="[]" in spec)
|
|
apply(drule_tac x=s in spec, drule_tac x=s in spec)
|
|
apply(simp add: sources_Step sameFor_dom_def uwr_refl uwr_equiv_def Step_def ipurge_Cons ipurge_Nil)
|
|
apply(case_tac "dom a s = u",simp)
|
|
apply(blast intro: policy_refl)
|
|
apply(clarsimp simp:sources_Cons sources_Nil Executable'_def execution_Nil ipurge_Nil)
|
|
apply(blast intro:uwr_sym)
|
|
done
|
|
|
|
lemma Noninfluence_strong_uwr_executable_u: "Noninfluence_strong_uwr \<Longrightarrow> executable_u"
|
|
apply(clarsimp simp: Noninfluence_strong_uwr_def executable_u_def uwr_equiv_def)
|
|
apply(drule_tac x=schedDomain in spec)
|
|
apply(drule_tac x="[a]" in spec)+
|
|
apply(drule_tac x=s in spec, drule_tac x=t in spec)
|
|
apply(erule impE,blast)
|
|
apply(erule impE)
|
|
apply(clarsimp simp:sources_Cons sources_Nil sameFor_dom_def)
|
|
apply(blast dest:schedNotGlobalChannel)
|
|
apply(erule impE,blast)+
|
|
apply(simp add: Executable'_def Step_def,blast)
|
|
done
|
|
|
|
lemma Noninfluence_strong_uwr_Noninfluence_gen:
|
|
"Noninfluence_strong_uwr \<Longrightarrow> Noninfluence_gen"
|
|
apply(rule Noninfluence_gen)
|
|
apply(rule confidentiality_u)
|
|
apply(rule Noninfluence_strong_uwr_confidentiality_u,assumption)
|
|
apply(rule Noninfluence_strong_uwr_integrity_u,assumption)+
|
|
apply(rule Noninfluence_strong_uwr_executable_u,assumption)
|
|
done
|
|
|
|
|
|
(* Experimenting with other unwinding conditions *)
|
|
|
|
text {*
|
|
Properties alternative unwinding conditions for executability should verify :
|
|
- Noninfluence_gen \<longrightarrow> executable_u
|
|
- executable_u \<and> (other assumptions) \<and> Executable as s \<longrightarrow> Executable (ipurge u as {s}) s
|
|
- executable_u \<and> (other assumptions) \<and> Executable as s \<longrightarrow> Executable as t
|
|
- executable_u \<and> (other assumptions) \<and> \<not>Executable as s \<longrightarrow> sources as s u = sources as t u
|
|
- executable_u \<and> (other assumptions) \<longrightarrow> ipurge u as {s} = ipurge u as {t}
|
|
- lemma dom_dom_in_policy_example stated above and/or lemma example stated below
|
|
|
|
Intuitions on alternative unwinding conditions and possible changes to the theory :
|
|
- the unwinding condition should state : (s,t)\<in>uwr (dom a s)
|
|
- the problem arises when the action is purged, so there are 3 possible fixes :
|
|
- add assumptions to the unwinding condition (difficult to combine with 'Noninfluence_gen \<longrightarrow> executable_u'
|
|
- change the definition of sources/ipurge, to purge an action iff it doesn't affect, directly or indirectly the target domain,
|
|
or any domain involved in the computation
|
|
- break symmetry in the unwinding condition (uwr_equiv is assymmetric, why not the unwinding condition ?)
|
|
|
|
The key lemma to obtain is Executable_u, the global version of the local property stated by the unwinding condition.
|
|
Assumptions that are reasonable are :
|
|
- the states are reachable,
|
|
- they are equivalent with respect to schedDomain,
|
|
- they are equivalent with respect to 'sources as s u' (<-- what 'u' ?)
|
|
|
|
Lemmas that may be helpful in proving that property are dom_dom_in_policy (above) and example (below).
|
|
|
|
*}
|
|
|
|
|
|
|
|
definition executable_u_weak where
|
|
"executable_u_weak \<equiv> \<forall>s t a.
|
|
reachable s \<and>
|
|
reachable t \<and> s \<sim>schedDomain\<sim> t \<and> s \<sim>dom a s\<sim>t \<and> (\<exists>s'. (s,s')\<in>Step a) \<longrightarrow>
|
|
(\<exists>t'. (t,t')\<in>Step a)"
|
|
|
|
|
|
lemma executable_u_weak_executable_u:
|
|
"executable_u \<Longrightarrow> executable_u_weak"
|
|
apply(fastforce simp:executable_u_def executable_u_weak_def)
|
|
done
|
|
|
|
lemma executable_u_weakD:
|
|
"\<lbrakk>executable_u_weak; reachable s; reachable t; (s,t)\<in>uwr schedDomain; (s,t)\<in>uwr (dom a s); (s,s')\<in>Step a\<rbrakk> \<Longrightarrow> \<exists>t'. (t,t')\<in>Step a"
|
|
apply(fastforce simp: executable_u_weak_def)
|
|
done
|
|
|
|
(* This is an example illustrating the use of the unwinding condition *)
|
|
lemma example:
|
|
"\<lbrakk>integrity_u; executable_u_weak; reachable s; (s,s')\<in> Step a;
|
|
\<exists>s''.(s',s'')\<in>Step b; (dom a s, dom b s') \<notin> policy\<rbrakk> \<Longrightarrow> \<exists>s'.(s,s')\<in>Step b"
|
|
apply(clarsimp simp: executable_u_weak_def)
|
|
apply(erule_tac x=s' in allE, erule_tac x=s in allE, erule_tac x=b in allE,simp)
|
|
apply(erule impE, safe)
|
|
apply(blast intro:reachable_Step)
|
|
apply(rule integrity_uD,simp_all add:uwr_refl)
|
|
apply(rule notI,drule schedNotGlobalChannel)
|
|
apply(erule notE,clarsimp simp:schedFlowsToAll)
|
|
apply(rule integrity_uD,simp_all add:uwr_refl)
|
|
apply blast
|
|
done
|
|
|
|
|
|
(* This lemma, consequence of the example, shows the importance of the link between executability and the policy *)
|
|
lemma dom_dom_in_policyI:
|
|
"reachable s \<Longrightarrow>
|
|
integrity_u \<Longrightarrow> executable_u_weak \<Longrightarrow> confidentiality_u_strong \<Longrightarrow>
|
|
Executable [a, b] s \<Longrightarrow> \<not> Executable [b] s \<Longrightarrow> dom a s \<leadsto> dom b s "
|
|
apply(rule classical, erule notE)
|
|
apply clarsimp
|
|
apply(frule_tac s'=s' in example,simp_all)
|
|
apply blast
|
|
apply(subgoal_tac "dom b s = dom b s'")
|
|
apply simp
|
|
apply(rule schedIncludesCurrentDom)
|
|
apply(rule integrity_uD[THEN uwr_sym],simp_all add:uwr_refl)
|
|
apply(case_tac "dom a s=schedDomain")
|
|
apply(erule notE,simp add:schedFlowsToAll)
|
|
apply(blast intro:schedNotGlobalChannel)
|
|
apply(blast intro:reachable_Step)
|
|
done
|
|
|
|
|
|
|
|
lemma self_step_eq:
|
|
"\<lbrakk>reachable s ; confidentiality_u_strong ; (s,s')\<in>Step a\<rbrakk> \<Longrightarrow> (\<forall>s' t'.(s,s')\<in>Step a \<and> (s,t')\<in>Step a \<longrightarrow> (\<forall>d. (s',t')\<in> uwr d))"
|
|
apply(clarsimp simp: confidentiality_u_strong_def)
|
|
apply(erule_tac x=a in allE, erule_tac x=d in allE,erule_tac x=s in allE,erule_tac x=s in allE)
|
|
apply(simp add: uwr_refl)
|
|
done
|
|
|
|
|
|
lemma allDomains_step_equiv[rule_format]:
|
|
"\<lbrakk>confidentiality_u_strong; reachable s; reachable t;
|
|
\<forall>d. (s,t)\<in>uwr d\<rbrakk> \<Longrightarrow>
|
|
(\<forall>s' t'. (s,s')\<in> Step a \<and> (t,t')\<in> Step a \<longrightarrow> (\<forall>d. (s',t')\<in> uwr d))"
|
|
apply(fastforce simp:confidentiality_u_strong_def)
|
|
done
|
|
|
|
|
|
lemma Executable_u_strong[rule_format]:
|
|
"\<forall>s t a. reachable s \<and> reachable t \<and> (\<forall>d. (s,t)\<in>uwr d) \<and>
|
|
Executable as s \<and> executable_u_weak \<and> confidentiality_u_strong \<longrightarrow> Executable as t"
|
|
apply(induct as)
|
|
apply simp
|
|
apply clarsimp
|
|
apply(subst (asm) executable_u_weak_def)
|
|
apply(erule_tac x=s in allE, erule_tac x=t in allE, erule_tac x=a in allE)
|
|
apply(blast dest:allDomains_step_equiv intro:reachable_Step)
|
|
done
|
|
|
|
|
|
(*Use in sources_eq' proof to simplify steps*)
|
|
lemma Executable_StepD:
|
|
"\<lbrakk>executable_u_weak ; confidentiality_u_strong ; reachable s ; (s,s')\<in>Step a; Executable (a#as) s\<rbrakk> \<Longrightarrow> Executable as s'"
|
|
apply(clarsimp)
|
|
apply(frule self_step_eq,auto)
|
|
apply(erule_tac x=s'a in allE, erule_tac x=s' in allE,simp)
|
|
apply(frule_tac s=s in reachable_Step,assumption)
|
|
apply(frule_tac s=s and s'=s'a in reachable_Step,assumption)
|
|
apply(rule Executable_u_strong,fastforce)
|
|
done
|
|
|
|
(*Use in sources_eq' proof to simplify steps*)
|
|
lemma ExecutableD2:
|
|
"\<lbrakk>executable_u_weak; confidentiality_u_strong; reachable s; reachable t; \<forall>d.(s,t)\<in> uwr d; (t,t')\<in> Step a; (s,s')\<in>Step a; Executable as s'\<rbrakk> \<Longrightarrow> Executable as t'"
|
|
apply(rule Executable_u_strong[rule_format,where s=s'],simp)
|
|
apply(rule conjI,blast intro:reachable_Step)+
|
|
apply(clarsimp,rule_tac s=s and t=t in allDomains_step_equiv)
|
|
apply blast+
|
|
done
|
|
|
|
|
|
lemma sources_eq':
|
|
"executable_u_weak \<and> confidentiality_u_strong \<and> s \<sim>schedDomain\<sim> t \<and>
|
|
reachable s \<and> reachable t \<and> Executable as s \<and> Executable as t \<longrightarrow> sources as s u = sources as t u"
|
|
proof (induct as arbitrary: s t)
|
|
case Nil show ?case
|
|
apply(simp add: sources_Nil)
|
|
done
|
|
next
|
|
case (Cons a as)
|
|
show ?case
|
|
apply(clarsimp simp: sources_Cons)
|
|
apply(rule insert_eq,simp)
|
|
apply(rule un_eq,rule set_eqI,rule iffI)
|
|
apply(erule_tac t="\<Union>{sources as t' u|t'. (t,t') \<in> Step a}" in subst[rotated])
|
|
apply(simp only: Union_eq, simp only: UNION_eq[symmetric])
|
|
apply(rule Un_eq)
|
|
apply clarsimp
|
|
apply(rule "Cons.hyps"[rule_format])
|
|
apply simp
|
|
apply(rule conjI)
|
|
apply(blast intro: sched_equiv_preserved)
|
|
apply(rule conjI,blast intro!: reachable_Step)+
|
|
apply(rule conjI)
|
|
apply(fastforce intro: ExecutableD2 simp:uwr_refl)
|
|
apply(fastforce intro: ExecutableD2 simp:uwr_refl)
|
|
apply(fastforce)
|
|
apply(fastforce)
|
|
apply(erule_tac t="\<Union>{sources as s' u|s'. (s,s') \<in> Step a}" in subst[rotated])
|
|
apply(simp only: Union_eq, simp only: UNION_eq[symmetric])
|
|
apply(rule Un_eq)
|
|
apply clarsimp
|
|
apply(rule "Cons.hyps"[rule_format])
|
|
apply simp
|
|
apply(rule conjI, blast intro: sched_equiv_preserved uwr_sym reachable_Step)+
|
|
apply(rule conjI)
|
|
apply(fastforce intro: ExecutableD2 simp:uwr_refl)
|
|
apply(rule_tac s=s' and t=s'c in Executable_u_strong,clarsimp)
|
|
apply(rule conjI,blast intro: reachable_Step)+
|
|
apply(clarsimp,blast intro:self_step_eq[rule_format])
|
|
apply(fastforce)
|
|
apply(fastforce)
|
|
apply(clarsimp simp: schedIncludesCurrentDom)
|
|
apply safe
|
|
apply(rule_tac x=v in exI,simp)
|
|
apply(rule_tac x=s'a in exI,simp)
|
|
apply(erule_tac t="sources as s'a u" in subst[rotated])
|
|
apply(rule "Cons.hyps"[rule_format],simp)
|
|
apply(rule conjI, blast intro:sched_equiv_preserved uwr_sym reachable_Step)+
|
|
apply(rule ExecutableD2,simp_all add:uwr_refl)
|
|
apply(rule_tac x=v in exI,simp)
|
|
apply(rule_tac x=s' in exI,simp)
|
|
apply(erule_tac t="sources as s' u" in subst[rotated])
|
|
apply(rule "Cons.hyps"[rule_format])
|
|
apply(rule conjI, blast intro: sched_equiv_preserved uwr_sym reachable_Step)+
|
|
apply(rule conjI)
|
|
apply(fastforce intro: ExecutableD2 simp:uwr_refl)+
|
|
done
|
|
qed
|
|
|
|
|
|
lemma sources_eq:
|
|
"\<lbrakk>executable_u_weak; confidentiality_u_strong; s \<sim>schedDomain\<sim> t; reachable s; reachable t; Executable as s; Executable as t\<rbrakk> \<Longrightarrow>
|
|
sources as s u = sources as t u"
|
|
apply(rule sources_eq'[rule_format], simp)
|
|
done
|
|
|
|
|
|
lemma in_policy:
|
|
"\<lbrakk>integrity_u; reachable s; (s,s')\<in>Step a; (s,t)\<in>uwr u; (s',t)\<notin>uwr u\<rbrakk>\<Longrightarrow>(dom a s,u)\<in>policy"
|
|
apply(auto dest:integrity_uD)
|
|
done
|
|
|
|
|
|
lemma uwr_equiv_Cons_bothI:
|
|
"\<lbrakk>reachable s; reachable t; executable_u_weak; (s,t)\<in>uwr schedDomain; (s,t)\<in>uwr (dom a s);
|
|
\<forall> s' t'. (s,s') \<in> Step a \<and> (t,t') \<in> Step a \<longrightarrow> uwr_equiv s' as t' bs u\<rbrakk> \<Longrightarrow>
|
|
uwr_equiv s (a # as) t (a # bs) u"
|
|
apply(clarsimp simp: uwr_equiv_def execution_Run)
|
|
apply(safe)
|
|
apply(frule Executable'D,fastforce)
|
|
apply(rule Executable'I,clarsimp)
|
|
apply(subst (asm) executable_u_weak_def,erule_tac x=s in allE,
|
|
erule_tac x=t in allE, erule_tac x=a in allE,clarsimp)
|
|
apply(erule impE,blast,safe)
|
|
apply(blast dest:Executable'D reachable_Step Executable'I)
|
|
apply(fastforce simp:reachable_Step execution_Run Executable'_def)
|
|
done
|
|
|
|
lemma uwr_equiv_Cons_leftI:
|
|
"\<lbrakk>reachable s; \<forall> s'. (s,s') \<in> Step a \<longrightarrow> uwr_equiv s' as t bs u\<rbrakk> \<Longrightarrow>
|
|
uwr_equiv s (a # as) t bs u"
|
|
apply(clarsimp simp: uwr_equiv_def execution_Run reachable_Step Executable'_def)
|
|
apply fastforce
|
|
done
|
|
|
|
lemma Noninfluence_gen_executable_u_weak:
|
|
"Noninfluence_gen \<Longrightarrow> executable_u_weak"
|
|
apply(clarsimp simp: executable_u_weak_def Noninfluence_gen_def)
|
|
apply(drule_tac x="dom a s" in spec)
|
|
apply(erule_tac x="[a]" in allE,
|
|
erule_tac x=s in allE, erule_tac x="{t}" in allE)
|
|
apply(clarsimp simp:uwr_equiv_def Executable'_def)
|
|
apply(erule impE,fastforce simp:sources_Cons sources_Nil sameFor_dom_def)
|
|
apply(erule conjE)
|
|
apply(erule impE, fastforce simp:execution_Run)
|
|
apply(frule_tac e=a in schedIncludesCurrentDom)
|
|
apply(fastforce simp:ipurge_Cons ipurge_Nil sources_Cons sources_Nil Step_def)
|
|
done
|
|
|
|
end
|
|
|
|
end
|