(*
 * 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
imports "Lib.Simulation"
begin

text {*
  Toby's extended noninterference definitions to handle dynamic assignment,
  that depends on the current state, of
  the domain that each action is assigned to. This is the gory details
  reported in the the CPP 2012 paper
  \emph{Noninterference for Operating System Kernels}.
*}

section {* Generic systems *}

lemma un_eq:
  "\<lbrakk>S = S'; T = T'\<rbrakk> \<Longrightarrow> S \<union> T = S' \<union> T'"
  by auto

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

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

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

subsection{* Run function *}

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[rule_format]:
  shows
  "(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 arbitrary: s u bs)
  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_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: bs s t u) 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




subsection {* Base system locale *}

text {* An ADT with an initial state. *}
locale system =
  fixes A :: "('a,'s,'e) data_type"
  and s0 :: "'s"  (* an initial state *)
begin

(* State 's' is reachable from the initial state 's0'. *)
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]}"

(* The system is "observationally deterministic": that is, the
 * observable part of the system is always deterministic. *)
definition obs_det
where
  "obs_det \<equiv> \<forall> s js. (\<exists> s'. execution A s js = {s'})"

lemmas obs_detD = obs_det_def[THEN meta_eq_to_obj_eq, THEN iffD1, rule_format]

(* The abstraction/concretisation functions "Init"/"Fin"
 * don't abstract away information. *)
definition no_abs
where
  "no_abs \<equiv> \<forall> x s as . reachable s \<longrightarrow> x \<in> steps (Simulation.Step A) (Init A s) as
                        \<longrightarrow> Init A (Fin A x) = {x}"

lemmas no_absD = no_abs_def[THEN meta_eq_to_obj_eq, THEN iffD1, rule_format]

end


subsection {* Enabled system *}

text{*
  A system that is always enabled.

  In particular, the system will never be in deadlock, and there
  is always an enabled transition from every reachable state. *}

locale enabled_system = system +
  assumes enabled: "(\<exists> js. s \<in> execution A s0 js) \<Longrightarrow> \<exists> s'. s' \<in> execution A s js"
begin

lemma reachable_enabled:
  "reachable s \<Longrightarrow> \<exists> s'. s' \<in> execution A s js"
  apply(simp add: reachable_def)
  apply(erule enabled)
  done

lemma enabled_Step:
  "reachable s \<Longrightarrow> \<exists> s'. (s,s') \<in> Step a"
  apply(simp add: Step_def, blast intro: reachable_enabled)
  done

end

subsection {* Step system *}

text {* A Step system is a system 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. In other words
   running [a,b,c,...] is the same than running [a] then running [b] then ...
   This correspond to projecting to the observable state and deducing the real
   state from that observable state on each event.

   We define the unwinding conditions on this kind of system *}
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}"
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_Run:
  "reachable s \<Longrightarrow> \<exists>as. (s0,s) \<in> Run Step as"
  apply (clarsimp simp add: reachable_def)
  apply (cut_tac as=js in execution_Run[OF reachable_s0])
  apply blast
  done

lemma Run_reachable:
  "\<exists>as. (s0,s) \<in> Run Step as \<Longrightarrow> reachable s"
  apply (clarsimp simp add: reachable_def)
  apply (cut_tac as=as in execution_Run[OF reachable_s0])
  apply blast
  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

lemma reachable_induct_helper:
  assumes a:
    "\<And>s s' a. \<lbrakk>reachable s; P s; (s, s') \<in> Step a\<rbrakk> \<Longrightarrow> P s'"
  shows "\<lbrakk>(s0, s1) \<in> Run Step as; P s0\<rbrakk> \<Longrightarrow> P s1"
  apply (induct as arbitrary: s1 rule: rev_induct)
   apply simp
  apply(fastforce dest: Run_mid intro: a Run_reachable)
  done

lemma reachable_induct:
  "\<lbrakk>(\<And>s s' a. reachable s \<Longrightarrow> (s,s') \<in> (Step a) \<Longrightarrow> P s \<Longrightarrow> P s'); reachable s1; P s0\<rbrakk> \<Longrightarrow> P s1"
  apply (drule reachable_Run)
  apply (elim exE)
  apply (rule reachable_induct_helper)
    apply simp+
  done

end

subsection {* Init Fin system *}

text {* An Init Fin system a stronger kind of Step system where know directly
   that Fin and Init behave nicely as nearly "inverse" of each other which imply
   that projecting to observable state then deducing the original state behave
   as expected in Step system.
  *}

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: "reachable s \<Longrightarrow> x \<in> steps (Simulation.Step A) (Init A s) as \<Longrightarrow>  x \<in> Init A (Fin A x)"
  assumes obs_det_or_no_abs: "obs_det \<or> no_abs"
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 and s=s and as=xs in Init_Fin, (simp add: steps_def)+)
  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)
    apply(simp add: steps_def Image_def)+
  done

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

lemma Init_Fin_system_Step_system:
  "Init_Fin_system A s0 \<Longrightarrow> Step_system A s0"
  apply(unfold_locales)
   apply(erule Init_Fin_system.reachable_s0)
  apply(erule (1) Init_Fin_system.execution_Run)
  done

sublocale Init_Fin_system \<subseteq> Step_system
  apply(rule Init_Fin_system_Step_system)
  apply(unfold_locales)
  done

subsection {* Init inv Fin system *}

text {* Here we go one step further than the Init_Fin_system:
  In this local Init and Fin are actually inverse of each other
  Fin is injective
  if s : range Fin A then Init A s = {s'} and Fin A s' = s else Init A s = {}.

  The internal state space is thus just a restriction of the observable state space.
*}

(* 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: "reachable s \<Longrightarrow> Init A s = {s'. Fin A s' = s}"
  assumes Fin_inj: "inj (Fin A)"
begin

lemma inv_and_inj: "reachable s \<Longrightarrow> Fin A i = s \<Longrightarrow> Init A s = {i}"
  using Fin_inj Init_inv_Fin by (blast dest:injD)

lemma s0_reachable:
  "reachable s0"
  apply(simp add: reachable_def)
  apply(rule_tac x="[]" in exI)
  apply(simp add: execution_def steps_def)
  using Fin_Init_s0.

lemma foldl_foldl_Step:
  "\<lbrakk>x \<in> foldl (\<lambda>S j. data_type.Step A j `` S) M as;
   M \<subseteq> foldl (\<lambda>S j. data_type.Step A j `` S) B js\<rbrakk>
       \<Longrightarrow> x \<in> foldl (\<lambda>S j. data_type.Step A j `` S)
               (foldl (\<lambda>S j. data_type.Step A j `` S) B js) as"
  apply(induct  as arbitrary: x M js B rule: rev_induct)
   apply fastforce
  apply simp
  apply(erule ImageE)
  apply(drule_tac x=xb in meta_spec)
  apply(drule_tac x=M in meta_spec)
  apply simp
  apply(drule_tac x=js in meta_spec)
  apply(drule_tac x=B in meta_spec, simp)
  apply(blast)
  done

lemma reachable_Fin:
  "\<lbrakk>reachable s;
    x \<in> steps (Simulation.Step A) (Init A s) as\<rbrakk>
   \<Longrightarrow> reachable (Fin A x)"
  apply(cut_tac s=s in Init_inv_Fin, assumption)
  apply(clarsimp simp: reachable_def execution_def steps_def)
  apply(rule_tac x="js@as" in exI)
  apply(rule imageI)
  apply(subgoal_tac "{s'. Fin A s' = Fin A xa} = {xa}")
   apply simp
   apply(erule foldl_foldl_Step)
   apply blast
  apply(blast dest: injD[OF Fin_inj])
  done

end

lemma Init_inv_Fin_system_Init_Fin_system:
  "Init_inv_Fin_system A s0 \<Longrightarrow> Init_Fin_system A s0"
  apply(unfold_locales)
     apply(erule Init_inv_Fin_system.s0_reachable)
    apply(simp add: Init_inv_Fin_system.Init_inv_Fin)
    apply(simp add: image_def)
    apply(fastforce simp: system.reachable_def execution_def)
   apply(cut_tac s="Fin A x" in Init_inv_Fin_system.Init_inv_Fin)
     apply assumption
    apply(blast intro: Init_inv_Fin_system.reachable_Fin)
   apply simp
  apply(rule disjI2)
  apply(clarsimp simp: system.no_abs_def)
  apply(frule Init_inv_Fin_system.Fin_inj)
  apply(cut_tac s="Fin A x" in Init_inv_Fin_system.Init_inv_Fin)
    apply assumption
   apply(blast intro: Init_inv_Fin_system.reachable_Fin)
  apply simp
  apply(fastforce dest: injD)
  done

sublocale Init_inv_Fin_system \<subseteq> Init_Fin_system
  apply(rule Init_inv_Fin_system_Init_Fin_system)
  apply(unfold_locales)
  done



section {* Non interference *}

subsection {* Policy *}

text{* This local represent an whole infoflow policy with the all the field needed
       for defining non leakage, non interference and non influence*}

locale noninterference_policy =
  fixes dom :: "'e \<Rightarrow> 's \<Rightarrow> 'd"        (* dynamic dom assignment *)
  fixes uwr :: "'d \<Rightarrow> ('s \<times> 's) set"  (* unwinding relation *)
  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"
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




subsection {* Non interference system *}

locale noninterference_system = enabled_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"
begin

(* The set of domains (which carry out actions in the list "as") which
 * may influence "u", assuming we start in state "s". *)
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]



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> \<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> \<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_sym:
  "uwr_equiv s as t bs u \<Longrightarrow> uwr_equiv t bs s as u"
  apply(fastforce simp: uwr_equiv_def uwr_sym)
  done

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)
  apply(cut_tac s=t and js=bs in reachable_enabled)
   apply assumption
  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 source_func u []     ss = []" |
  Cons: "gen_purge source_func u (a#as) ss =
            (if (\<exists>s\<in>ss. dom a s \<in> source_func (a#as) s u) then
               a#gen_purge source_func u as (\<Union>s\<in>ss. {s'. (s,s') \<in> Step a})
             else
               gen_purge source_func 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 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 Noninterference *}

definition Noninterference :: "bool"
where
 "Noninterference \<equiv>
  \<forall> u as s. reachable s \<longrightarrow>
         (obs_equiv s as s (ipurge u as {s}) u)"


text {* Strong Noninterference *}
definition Noninterference_strong :: "bool"
where
 "Noninterference_strong \<equiv>
  \<forall> u as bs s. reachable s \<longrightarrow>
         (ipurge u as {s}) = (ipurge u bs {s}) \<longrightarrow>
         (obs_equiv s as s bs u)"



lemma obs_equiv_sym:
  "obs_equiv s as t bs u \<Longrightarrow> obs_equiv t bs s as u"
  apply(clarsimp simp: obs_equiv_def)
  done

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)
  apply(cut_tac s=t and js=bs in reachable_enabled, assumption, blast)
  done

lemma Noninterference_Noninterference_strong:
  "\<lbrakk>Noninterference\<rbrakk> \<Longrightarrow> Noninterference_strong"
  apply(clarsimp simp: Noninterference_def Noninterference_strong_def)
  apply(drule_tac x=u in spec)
  apply(frule_tac x=as in spec, drule_tac x=s in spec)
  apply(drule_tac x=bs in spec, drule_tac x=s in spec)
  apply clarsimp
  apply(rule obs_equiv_trans)
    apply assumption
   apply assumption
  apply(erule obs_equiv_sym)
  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"




definition Noninfluence_strong  :: "bool"
where
 "Noninfluence_strong \<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>
         obs_equiv s as t bs 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


lemma Noninfluence_strong_Noninterference_strong:
  "Noninfluence_strong \<Longrightarrow> Noninterference_strong"
  apply(clarsimp simp: Noninfluence_strong_def Noninterference_strong_def)
  apply(drule_tac x=u in spec, drule_tac x=as in spec, drule_tac x=bs in spec)
  apply(fastforce simp: sameFor_dom_def uwr_refl)
  done

lemma Noninfluence_strong_Nonleakage:
  "Noninfluence_strong \<Longrightarrow> Nonleakage"
  apply(clarsimp simp: Noninfluence_strong_def Nonleakage_def)
  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 :: "bool"
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 no_domain_visible_nondeterminism:
  "\<lbrakk>confidentiality_u; reachable s; (s,s') \<in> Step a; (s,s'') \<in> Step a\<rbrakk> \<Longrightarrow> s' \<sim>d\<sim> s''"
  apply(clarsimp simp: confidentiality_u_def)
  apply(fastforce intro: uwr_refl)
  done

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} that, with
  @{prop integrity_u}, implies it.
*}
definition confidentiality_u_weak
where
  "confidentiality_u_weak \<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 confidentiality_u_confidentiality_u_weak:
  "confidentiality_u \<Longrightarrow> confidentiality_u_weak"
  apply (simp add: confidentiality_u_def confidentiality_u_weak_def)
  apply blast
  done

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_weak:
  "\<lbrakk>confidentiality_u_weak; integrity_u\<rbrakk> \<Longrightarrow>
  confidentiality_u"
  apply(clarsimp simp: confidentiality_u_def)
  apply(erule impCE')
   apply(subst (asm) confidentiality_u_weak_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 Noninfluence_strong_uwr_Noninfluence_strong:
  "\<lbrakk>output_consistent; Noninfluence_strong_uwr\<rbrakk> \<Longrightarrow> Noninfluence_strong"
  apply(clarsimp simp: Noninfluence_strong_def)
  apply(erule obs_equivI)
  apply(auto simp: Noninfluence_strong_uwr_def)
  done

lemma sched_equiv_preserved:
  "\<lbrakk>confidentiality_u;  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_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 simp
  apply(subst (asm) confidentiality_u_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)
  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(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

lemma Noninfluence_gen_Noninterference_strong:
  "\<lbrakk>output_consistent; Noninfluence_gen\<rbrakk> \<Longrightarrow> Noninterference_strong"
  apply(rule Noninterference_Noninterference_strong)
  apply(blast intro: Noninfluence_gen_Noninterference)
  done


end

subsection {* Noninterference on enabled Step system : unwinding system *}

locale enabled_Step_system = enabled_system A s0 + Step_system A s0
  for A :: "('a,'s,'e) data_type" and s0 :: "'s"


(* we define the unwinding conditions for any system *)
locale unwinding_system = enabled_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"

sublocale unwinding_system \<subseteq> noninterference_system
  apply(unfold_locales)
  done

context unwinding_system begin




lemma sources_refl:
  "reachable s \<Longrightarrow> u \<in> sources as s u"
  apply(induct as arbitrary: s)
   apply(simp add: sources_Nil)
  apply(simp add: sources_Cons)
  apply(frule_tac a=a in enabled_Step)
  apply (auto simp: reachable_Step)
  done



lemma schedDomain_in_sources_Cons:
  "reachable s \<Longrightarrow> dom a s = schedDomain \<Longrightarrow> dom a s \<in> sources (a#as) s u"
  apply(unfold sources_Cons)
  apply(erule ssubst)
  apply(rule UnI2)
  apply(clarsimp)
  apply(rule_tac x=u in exI)
  apply(safe)
   apply(rule schedFlowsToAll)
  apply(frule_tac a=a in enabled_Step)
  apply(fastforce dest: sources_refl reachable_Step)
  done



lemma sources_eq':
  "confidentiality_u \<and> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable 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 un_eq)
   apply(simp only: Union_eq, simp only: UNION_eq[symmetric])
   apply(rule Un_eq, clarsimp)
     apply(metis "Cons.hyps"[rule_format] sched_equiv_preserved reachable_Step)
    apply(fastforce intro: enabled_Step)
   apply(fastforce intro: enabled_Step)
  apply(clarsimp simp: schedIncludesCurrentDom)
  apply(rule Collect_cong)
  apply(rule conj_cong, rule refl)
  apply(rule iff_exI)
  apply(metis "Cons.hyps"[rule_format] sched_equiv_preserved reachable_Step enabled_Step)
  done
  qed


lemma sources_eq:
  "\<lbrakk>confidentiality_u; s \<sim>schedDomain\<sim> t; reachable s; reachable t\<rbrakk> \<Longrightarrow>
  sources as s u = sources as t u"
  by(rule sources_eq'[rule_format], simp)


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(rule UnI2)
  apply blast
  done

lemma sources_unwinding_step:
  "\<lbrakk>s \<approx>(sources (a#as) s u)\<approx> t; s \<sim>schedDomain\<sim> t; confidentiality_u;
    (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(subst (asm) confidentiality_u_def)
  apply(drule_tac x=a in spec)
  apply(drule_tac x=ua in spec)
  apply(drule_tac x=s in spec)
  apply(drule_tac x=t in spec)
  apply(fastforce intro: sameFor_sources_dom)
  done

lemma ipurge_eq'_helper:
  "\<lbrakk>s \<in> ss; dom a s \<in> sources (a # as) s u; \<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u;
   (\<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t);
   t \<in> ts; confidentiality_u\<rbrakk> \<Longrightarrow>
  False"
  apply(cut_tac s=s and t=t and as=as and u=u in sources_eq, simp+)
  apply(clarsimp  simp: sources_Cons | safe)+
  apply(rename_tac s')
   apply(drule_tac x=t in bspec, simp)
   apply clarsimp
   apply(cut_tac s=t in enabled_Step, simp)
   apply(erule exE, rename_tac t')
   apply(drule_tac x="sources as t' u" in spec)
   apply(cut_tac s=s' and t=t' and u=u in sources_eq, simp+)
      apply(fastforce elim: sched_equiv_preserved)
     apply(fastforce intro: reachable_Step)
    apply(fastforce intro: reachable_Step)
   apply(fastforce simp: schedIncludesCurrentDom)
  apply(drule_tac x=t in bspec, simp)
  apply clarsimp
  apply(rename_tac v s')
  apply(drule_tac x=v in spec, erule impE, fastforce simp: schedIncludesCurrentDom)
  apply(cut_tac s=t in enabled_Step[where a=a], simp, clarsimp, rename_tac t')
  apply(cut_tac s=s' and t=t' and u=u in sources_eq, simp+)
     apply(fastforce elim: sched_equiv_preserved)
    apply(fastforce intro: reachable_Step)
   apply(fastforce intro: reachable_Step)
  apply(fastforce simp: schedIncludesCurrentDom)
  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) \<and> (\<exists> t. t \<in> ts) \<and> confidentiality_u
    \<longrightarrow> ipurge u as ss = ipurge u as ts"
  proof (induct as arbitrary: ss ts)
  case Nil show ?case
   apply(simp add: ipurge_def)
   done
  next
  case (Cons a as) show ?case
   apply(clarsimp simp: ipurge_Cons schedIncludesCurrentDom)
   apply(intro conjI impI)
      apply(rule "Cons.hyps"[rule_format])
      apply clarsimp
      apply(metis sched_equiv_preserved reachable_Step enabled_Step)
     apply clarsimp
     apply(drule ipurge_eq'_helper, simp+)[1]
    apply clarsimp
    apply(drule ipurge_eq'_helper, (simp add: uwr_sym)+)[1]
   apply(rule "Cons.hyps"[rule_format], auto)
   done
  qed

lemma ipurge_eq:
  "\<lbrakk>s \<sim>schedDomain\<sim> t; reachable s; reachable t;
    confidentiality_u\<rbrakk> \<Longrightarrow>
   ipurge u as {s} = ipurge u as {t}"
  by(rule ipurge_eq'[rule_format], simp)

lemma Noninfluence_uwr_Noninfluence_strong_uwr:
  "\<lbrakk>confidentiality_u; Noninfluence_uwr\<rbrakk> \<Longrightarrow> Noninfluence_strong_uwr"
  apply(clarsimp simp: Noninfluence_uwr_def Noninfluence_strong_uwr_def)
  apply(frule_tac s=s and t=t and as=as and u=u in ipurge_eq)
     apply assumption+
  apply(frule_tac s=s and t=t and as=bs and u=u in ipurge_eq)
     apply assumption+
  apply clarsimp
  apply(drule_tac x=u in spec)
  apply(frule_tac x=as in spec)
  apply(drule_tac x=s in spec, drule_tac x=t in spec)
  apply(drule_tac x=bs in spec)
  apply(drule_tac x=t in spec, drule_tac x=t in spec)
  apply clarsimp
  apply(rule_tac t=t in uwr_equiv_trans)
    apply assumption
   apply assumption
  apply(rule uwr_equiv_sym)
  apply(clarsimp simp: sameFor_dom_def uwr_refl)
  done

lemma Noninfluence_Noninfluence_strong:
  "\<lbrakk>confidentiality_u; Noninfluence\<rbrakk> \<Longrightarrow> Noninfluence_strong"
  apply(clarsimp simp: Noninfluence_def Noninfluence_strong_def)
  apply(frule_tac s=s and t=t and as=as and u=u in ipurge_eq)
     apply assumption+
  apply(frule_tac s=s and t=t and as=bs and u=u in ipurge_eq)
     apply assumption+
  apply clarsimp
  apply(drule_tac x=u in spec)
  apply(frule_tac x=as in spec)
  apply(drule_tac x=s in spec, drule_tac x=t in spec)
  apply(drule_tac x=bs in spec)
  apply(drule_tac x=t in spec, drule_tac x=t in spec)
  apply clarsimp
  apply(rule_tac t=t in obs_equiv_trans)
    apply assumption
   apply assumption
  apply(rule obs_equiv_sym)
  apply(clarsimp simp: sameFor_dom_def uwr_refl)
  done


lemma dom_in_sources_Cons:
  "\<lbrakk>confidentiality_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 uwr_equiv_Cons_bothI:
   "\<lbrakk>reachable s; reachable t;
     \<forall> s' t'. (s,s') \<in> Step a \<and> (t,t') \<in> Step b \<longrightarrow> uwr_equiv s' as t' bs u\<rbrakk> \<Longrightarrow>
    uwr_equiv s (a # as) t (b # bs) u"
  apply(clarsimp simp: uwr_equiv_def)
  apply(clarsimp simp: execution_Run)
  apply(fastforce simp: execution_Run reachable_Step)
  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"
  by(fastforce simp: uwr_equiv_def execution_Run reachable_Step)


lemma notin_policyI':
  "\<lbrakk>reachable s;
    dom a s \<notin> sources (a # list) s u; (s,s') \<in> Step a; ua \<in> sources list s' u\<rbrakk> \<Longrightarrow>
   (dom a s,ua) \<notin> policy"
  apply(rule notin_policyI)
  apply auto
  done

lemma sources_eq_Step:
  "\<lbrakk>integrity_u; confidentiality_u; reachable s; (s,s') \<in> Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow>
   (sources as s' u) = (sources as s u)"
  apply(rule sources_eq, simp+)
    apply(rule_tac t=s and s=s and a=a in sched_equiv_preserved_left,
          (simp add: uwr_refl reachable_Step)+)
  done

lemma sources_equiv_preserved_left:
  "\<lbrakk>integrity_u; confidentiality_u; reachable s; reachable t; s \<sim>schedDomain\<sim> t;
    dom a s \<notin> sources (a#as) s u; s \<approx>sources (a#as) s u\<approx> t; (s,s') \<in> Step a; dom a s \<noteq> schedDomain\<rbrakk>
    \<Longrightarrow> s' \<approx>sources as s' u\<approx> t"
  apply(clarsimp simp: sameFor_dom_def)
  apply(rename_tac v)
  apply(case_tac "(dom a s, v) \<in> policy")
   apply(fastforce simp: sources_Cons)
  apply(fastforce dest: integrity_uD simp: sources_Cons)
  done

lemma Noninfluence_gen:
  "\<lbrakk>confidentiality_u; integrity_u\<rbrakk> \<Longrightarrow> Noninfluence_gen"
  apply(subst Noninfluence_gen_def)
  apply(intro allI)
  proof -
  assume conf: "confidentiality_u"
  assume integ: "integrity_u"
  fix u as s ts
  show "reachable s \<and> Ball ts reachable \<longrightarrow>
          Ball ts (sameFor_dom s (sources as s u)) \<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)"
    proof(induct as arbitrary: s ts)
    case Nil
    show ?case
      apply(clarsimp simp: sameFor_dom_def ipurge_Nil sources_Nil uwr_equiv_def)
      apply(clarsimp simp: execution_Run)
      done
    next
    case (Cons a as)
    show ?case
  apply(clarsimp simp: ipurge_Cons | safe)+
   apply(rule uwr_equiv_Cons_bothI)
     apply assumption
    apply blast
   apply(clarify)
   apply(rename_tac ta tb s' tb')
   apply(rule Cons.hyps[rule_format])
      apply(blast intro: reachable_Step)
     apply(clarsimp)
     apply(rename_tac tc' tc)
     using conf apply(rule_tac s=s and t=tc and a=a in sources_unwinding_step, simp+)[1]
    apply(clarsimp, rename_tac tc' tc)
    apply(rule sched_equiv_preserved[OF conf], (auto simp: sources_refl))[1]
   apply blast
  apply(rename_tac ta)
  apply(rule uwr_equiv_Cons_leftI, blast)
  apply(clarsimp, rename_tac s')
  apply(case_tac "dom a s = schedDomain")
   apply(cut_tac s=s and a=a and as=as and u=u in schedDomain_in_sources_Cons, assumption+)
   apply(metis schedIncludesCurrentDom sources_eq[OF conf])
  apply(rule Cons.hyps[rule_format])
     apply(blast intro: reachable_Step)
    apply(rename_tac tb)
    apply(rule_tac a=a in sources_equiv_preserved_left[OF integ conf], simp+)
       apply(fastforce simp: schedIncludesCurrentDom sources_eq[OF conf])
      apply blast
     apply assumption
    apply assumption
   apply(rule_tac s=s and a=a in sched_equiv_preserved_left[OF integ], simp+)
  done
  qed
  qed

lemma Nonleakage_gen:
  "\<lbrakk>confidentiality_u\<rbrakk> \<Longrightarrow> Nonleakage_gen"
  apply(subst Nonleakage_gen_def)
  apply(rule allI)
  apply(induct_tac as)
   apply(simp add: sources_Nil uwr_equiv_def execution_Run sameFor_dom_def)
  apply(clarsimp)
  apply(rule uwr_equiv_Cons_bothI)
    apply assumption
   apply assumption
  apply clarsimp
  apply(drule_tac x=s' in spec, drule_tac x=u in spec, drule_tac x=t' in spec)
  apply(clarsimp simp: reachable_Step)
  apply(erule impE)
   apply(blast intro: sched_equiv_preserved)
  apply(erule mp)
  apply(blast intro: sources_unwinding_step)
  done



lemma Noninterference:
  "\<lbrakk>confidentiality_u_weak; output_consistent; integrity_u\<rbrakk> \<Longrightarrow>
   Noninterference"
  apply(rule Noninfluence_gen_Noninterference)
   apply assumption
  apply(blast intro: Noninfluence_gen confidentiality_u_weak)
  done

lemma Noninterference_strong:
  "\<lbrakk>confidentiality_u_weak; output_consistent; integrity_u\<rbrakk> \<Longrightarrow>
   Noninterference_strong"
  apply(rule Noninfluence_gen_Noninterference_strong)
   apply assumption
  apply(blast intro: Noninfluence_gen confidentiality_u_weak)
  done



lemma Noninfluence:
  "\<lbrakk>confidentiality_u_weak; output_consistent; integrity_u\<rbrakk> \<Longrightarrow>
   Noninfluence"
  apply(rule Noninfluence_gen_Noninfluence)
   apply assumption
  apply(blast intro: Noninfluence_gen confidentiality_u_weak)
  done

lemma Noninfluence_strong:
  "\<lbrakk>confidentiality_u_weak; output_consistent; integrity_u\<rbrakk> \<Longrightarrow>
   Noninfluence_strong"
  apply(rule Noninfluence_Noninfluence_strong)
   apply(blast intro: confidentiality_u_weak)
  apply(blast intro: Noninfluence)
  done


lemma Noninfluence_uwr:
  "\<lbrakk>confidentiality_u_weak; integrity_u\<rbrakk> \<Longrightarrow>
   Noninfluence_uwr"
  apply(rule Noninfluence_gen_Noninfluence_uwr)
  apply(blast intro: Noninfluence_gen confidentiality_u_weak)
  done

lemma Noninfluence_strong_uwr:
  "\<lbrakk>confidentiality_u_weak; integrity_u\<rbrakk> \<Longrightarrow>
   Noninfluence_strong_uwr"
  apply(rule Noninfluence_uwr_Noninfluence_strong_uwr)
   apply(blast intro: confidentiality_u_weak)
  apply(blast intro: Noninfluence_uwr)
  done

lemma sources_Step:
  "\<lbrakk>reachable s; (dom a s, u) \<notin> policy\<rbrakk> \<Longrightarrow>
  sources [a] s u = {u}"
  apply(auto simp: sources_Cons sources_Nil enabled_Step dest: enabled_Step)
  done

lemma sources_Step_2:
  "\<lbrakk>reachable s; (dom a s, u) \<in> policy\<rbrakk> \<Longrightarrow>
  sources [a] s u = {dom a s,u}"
  apply(auto simp: sources_Cons sources_Nil enabled_Step dest: enabled_Step)
  done

lemma execution_Nil:
  "reachable s \<Longrightarrow> execution A s [] = {s}"
  apply(simp add: execution_Run)
  done

lemma Noninfluence_gen_confidentiality_u_weak:
  "Noninfluence_gen \<Longrightarrow> confidentiality_u_weak"
  apply(clarsimp simp: Noninfluence_gen_def confidentiality_u_weak_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
           split: if_splits
             add: schedIncludesCurrentDom)
  done

lemma Noninfluence_strong_uwr_confidentiality_u_weak:
  "Noninfluence_strong_uwr \<Longrightarrow> confidentiality_u_weak"
  apply(clarsimp simp: Noninfluence_strong_uwr_def confidentiality_u_weak_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

lemma Nonleakage_gen_confidentiality_u:
  "Nonleakage_gen \<Longrightarrow> confidentiality_u"
  apply(clarsimp simp: Nonleakage_gen_def confidentiality_u_def)
  apply(drule_tac x="[a]" in spec, drule_tac x=s in spec)
  apply(drule_tac x=u in spec, drule_tac x=t in spec)
  apply(case_tac "dom a s \<leadsto> u")
   apply(simp add: sources_Step_2 uwr_equiv_def sameFor_dom_def Step_def)
  apply(simp add: sources_Step uwr_equiv_def sameFor_dom_def Step_def)
  done

lemma Nonleakage_gen_equiv_confidentiality_u:
  "Nonleakage_gen = confidentiality_u"
  apply(blast intro: Nonleakage_gen_confidentiality_u Nonleakage_gen)
  done

lemma non_sched_doms_cannot_schedule:
  "\<lbrakk>integrity_u; reachable s; dom a s \<noteq> schedDomain; (s,s') \<in> Step a\<rbrakk> \<Longrightarrow> s \<sim>schedDomain\<sim> s'"
  apply(drule_tac u=schedDomain in integrity_uD)
      apply assumption
     apply(erule contrapos_nn)
     apply(erule schedNotGlobalChannel)
    apply(rule uwr_refl)
   apply assumption
  apply(erule uwr_sym)
  done


text {*
   In systems with just a single event, @{prop integrity_u} is a very strong
   condition. It implies that once the scheduler is not
   running, it can never run again.

   This is one explanation for why seL4 (whose automaton has only a single
   event) doesn't satisfy @{prop integrity_u}.
*}
lemma integrity_u_and_single_event_systems:
  "\<lbrakk>integrity_u; reachable s; dom a s \<noteq> schedDomain; s' \<in> execution A s as;
    \<forall> y::'e. y = a\<rbrakk> \<Longrightarrow> dom e s' \<noteq> schedDomain"
  apply(frule_tac x=e in spec)
  apply(erule ssubst)
  apply(rule_tac P="\<lambda>x. x \<noteq> schedDomain" in subst[rotated])
   apply assumption
  apply(induct as arbitrary: s s' a rule: rev_induct)
   apply(simp add: execution_Run)
  apply(simp add: execution_Run)
  apply(drule Run_mid)
  apply(erule exE, rename_tac t)
  apply(drule_tac x=s in meta_spec)
  apply(drule_tac x=t in meta_spec)
  apply(drule_tac x=a in meta_spec)
  apply simp
  apply(rule schedIncludesCurrentDom)
  apply(rule non_sched_doms_cannot_schedule)
     apply assumption
    apply(rule reachable_execution)
     apply assumption
    apply(fastforce simp: execution_Run)
   apply assumption
  apply(drule_tac x=x in spec)
  apply blast
  done

end


subsection {* Complete unwinding system *}

text {* The unwinding conditions are not only sound but also complete when policy is reflexive *}
locale complete_unwinding_system = unwinding_system +
  assumes  policy_refl:
  "(u,u) \<in> policy"
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
           split: if_splits add: uwr_refl policy_refl execution_Nil 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
           split: if_splits)
   apply(simp add: policy_refl)
  apply(simp add: execution_Nil)
  apply(blast intro: uwr_sym)
  done

text {*
   @{prop Noninfluence_gen} actually turns out to be equivalent to @{prop Noninfluence_strong_uwr},
   when the policy is reflexive. So the two unwinding conditions for integrity
   and confidentiality actually turn out to be sound and sufficient for the
   condition we were using them to prove in the first place.
*}
lemma Noninfluence_gen_equiv_Noninfluence_strong_uwr:
  "Noninfluence_gen = Noninfluence_strong_uwr"
  apply(rule iffI)
   apply(rule Noninfluence_strong_uwr)
    apply(erule Noninfluence_gen_confidentiality_u_weak)
   apply(erule Noninfluence_gen_integrity_u)
  apply(rule Noninfluence_gen)
   apply(rule confidentiality_u_weak)
    apply(erule Noninfluence_strong_uwr_confidentiality_u_weak)
   apply(erule Noninfluence_strong_uwr_integrity_u)+
  done

end

end