Re: [isabelle] instantiating typedecls with datatypes?



* Thomas Bleher <bleher at informatik.uni-muenchen.de> [2006-11-06 13:01]:
> Hi all,
> 
> I'm currently playing with David von Oheimb's Noninterference package
> (see http://david.von-oheimb.de/cs/HOL/NI/, all the files are attached)

Sorry, forgot to attach the files, fixed now.

Thomas

theory Test imports Noninfluence begin

primrec
"dom (INPUTHIGH x) = H"
"dom (INPUTLOW x) = L"
"dom OUTPUTHIGH = H"
"dom OUTPUTLOW = L"

primrec
"step (INPUTHIGH x) S = S\<lparr> HighData := x \<rparr>"
"step (INPUTLOW x) S = S\<lparr> LowData := x \<rparr>"
"step OUTPUTHIGH S = S"
"step OUTPUTLOW S = S"

primrec
"output H s = {HighData s, LowData s}"
"output L s = {LowData s}"

(* Information may flow from Low to High *)

recdef policy "measure (\<lambda> x. 0)"
"policy x = (if x = L then (\<lambda> y. True) else (\<lambda> y. x=y))"

primrec
"uwr s1 H s2 = (s1=s2)"
"uwr s1 L s2 = ((LowData s1) = (LowData s2))"

lemma wsc: "weakly_step_consistent"
apply(simp add:weakly_step_consistent_def)
apply(auto)
apply(case_tac a)
apply(auto)
apply(case_tac u)
apply(auto)
apply(case_tac a)
by(auto)

lemma sr: "step_respect"
apply(simp add:step_respect_def)
apply(auto)
apply(case_tac a, auto)
by(case_tac u, auto)


lemma oc: "output_consistent"
apply(simp add:output_consistent_def)
apply(auto)
apply(case_tac u, auto)
by(case_tac u, auto)

theorem "nonleakage"
by(insert nonleakage wsc oc sr, simp)

lemma lr: "local_respect"
apply(simp only:local_respect_def local_respect_left_def local_respect_right_def)
apply(simp)
apply(auto)
apply(case_tac u, auto)
apply(case_tac a, auto)
apply(case_tac a, auto)
apply(case_tac a, auto)
by(case_tac u, auto)

theorem "noninterference"
by(insert noninterference wsc oc sr lr,simp)

end
(*  Title:      NI/System.thy
    Id:         $Id: System.thy,v 1.6 2004/01/29 17:36:47 dvo Exp $
    Author:     David von Oheimb
    License:    (C) 2003 Siemens AG; any non-commercial use is granted

*)
header {* Automata *}

(*<*)
theory System imports Main begin
ML {* Pretty.setmargin 169; quick_and_dirty:=true *}

(*>*)
record "state" =
  HighData :: nat
  LowData :: nat

datatype "action" = INPUTHIGH nat | INPUTLOW nat | OUTPUTHIGH | OUTPUTLOW
types "output" = nat
datatype "domain" = H | L
(*
(* the original system had this: *)
typedecl "state" 
typedecl "action"
typedecl "output"
typedecl "domain"
*)

text {* System described as Moore (rather than Mealy) automaton *}

consts   step :: "action =>  state => state"
         Step :: "action => (state \<times> state) set" --{* non-deterministic step *}
        "output" :: "domain => state => output set" --{* all observations of a domain *}
         run  :: "action list =>  state => state"
         Run  :: "action list => (state \<times> state) set" --{* non-deterministic run *}

primrec "run []     = (\<lambda>s. s)"
        "run (a#as) = run as \<circ> step a" 
primrec "Run []     = Id"
        "Run (a#as) = Run as O Step a" 

consts s0 :: "state"

(*<*)
lemma foldl_init_func [rule_format]:
  "\<forall>g. foldl (\<lambda>f a u. h a (f u)) g as (h a x) = 
       foldl (\<lambda>f a u. h a (f u)) (g o h a) as x"
by (rule induct, auto)

lemma "run = foldl (\<lambda>f a. step a \<circ> f) (\<lambda>s. s)"
apply (rule ext)
apply (rule ext)
apply (rule_tac x = xa in spec)
apply (rule induct, auto simp add: foldl_init_func o_def)
done

lemma run_append [simp]: "run (as @ bs) = run bs \<circ> run as"
by (induct "as", auto)

lemma Run_append [simp]: "Run (as @ bs) = Run bs O Run as"
by (induct "as", auto)

end
(*>*)
(*  Title:      NI/Generics.thy
    Id:         $Id: Generics.thy,v 1.6 2004/01/29 17:36:46 dvo Exp $
    Author:     David von Oheimb
    License:    (C) 2003 Siemens AG; any non-commercial use is granted

*)
header {* Generic notions *}

(*<*)
theory Generics imports System begin

(*>*)

subsection "policies"

(*<*)
hide const dom 
(*>*)
consts dom        :: "action => domain"           --{* security domain *}
       policy     :: "domain => domain => bool"  ("(_\ \<leadsto>\ _)"(*<*) [46,46] 45(*>*))
syntax policy_neg :: "domain => domain => bool"  ("(_\ \<notleadsto>\ _)"(*<*) [46,46] 45(*>*))
translations "u \<notleadsto> v" \<rightleftharpoons> "\<not>(u \<leadsto> v)"

axioms policy_refl: "u \<leadsto> u"

locale policy_trans =
  assumes policy_trans: "\<lbrakk>u \<leadsto> v; v \<leadsto> w\<rbrakk> \<Longrightarrow> u \<leadsto> w"
(*<*)

lemma (in policy_trans) rev_policy_trans: "\<lbrakk>u \<notleadsto> w; v \<leadsto> w\<rbrakk> \<Longrightarrow> u \<notleadsto> v"
by (blast intro: policy_trans)

(*>*)
subsection "allowed source domains"

types sourcef = "action list => domain => domain set"

subsubsection "trivial source functions"

constdefs
  singleton :: "sourcef"
 "singleton as u \<equiv> {u}"

  tsources :: "sourcef"
 "tsources as u \<equiv> {w. w \<leadsto> u}"
(*<*)

declare singleton_def [simp]

lemma singleton_iff [iff]: "v \<in> singleton as u = (v = u)"
by (simp)

(*>*)
subsubsection "chains of domains"

consts gen_chain :: "(domain => action => bool) => sourcef"
primrec 
  Nil:  "gen_chain P []     u = {u}"
  Cons: "gen_chain P (a#as) u = gen_chain P as u \<union> 
                    {w. P w a \<and> (\<exists>v. w \<leadsto> v \<and> v \<in> gen_chain P as u)}"

lemma gen_chain_refl: "u \<in> gen_chain P as u" 
(*<*)
by (induct "as", auto)

(*>*)
lemma gen_chain_trans: 
  "\<lbrakk>w \<leadsto> v; v \<in> gen_chain P as u; P w a\<rbrakk> \<Longrightarrow> w \<in> gen_chain P (a#as) u"
(*<*)
by (induct "as", auto)
lemma rev_gen_chain_trans: 
  "w \<notin> gen_chain P (a#as) u \<Longrightarrow> \<not>(\<exists>u\<in>gen_chain P as u. w \<leadsto> u \<and> P w a)"
by (blast intro: gen_chain_trans)

lemma gen_chain_direct: "\<lbrakk>w \<leadsto> u; P w a\<rbrakk> \<Longrightarrow> w \<in> gen_chain P (a#as) u"
by (blast intro: gen_chain_refl gen_chain_trans)
lemma rev_gen_chain_direct: "w \<notin> gen_chain P (a#as) u \<Longrightarrow> \<not> (w \<leadsto> u \<and> P w a)"
by (blast intro: gen_chain_direct)

(*>*)
lemma gen_chain_subset_Cons: "gen_chain P as u \<subseteq> gen_chain P (a#as) u"
(*<*)
by (induct "as", auto)

lemma singleton_subset_gen_chain: "singleton as u \<subseteq> gen_chain P as u"
by (blast intro!: gen_chain_refl)

lemma gen_chain_append2 [rule_format]: 
  "\<forall>bs. v \<in> gen_chain P bs u \<longrightarrow> v \<in> gen_chain P (as @ bs) u"
by (induct "as", auto)

lemma (in policy_trans) gen_chain_implies_policy_lemma [rule_format]:
  "\<forall>w. w \<in> gen_chain P as u \<longrightarrow> w \<leadsto> u"
apply (induct "as")
apply  (simp_all add: policy_refl)
apply (fast dest: policy_trans)
done
(*>*)
lemma (in policy_trans) gen_chain_implies_policy:  --{* Rushby's Lemma 6 *}
  "w \<in> gen_chain P as u \<Longrightarrow> w \<leadsto> u"
(*<*)
by (erule gen_chain_implies_policy_lemma)

lemma (in policy_trans) gen_chain_subset_tsources:
 "gen_chain P as u \<subseteq> tsources as u"
by (auto simp add: tsources_def elim: gen_chain_implies_policy)

lemma in_gen_chain_Cons_eq_lemma: 
  "P w a \<Longrightarrow> w \<in> gen_chain P (a#as) u <-> (\<exists>v. w \<leadsto> v \<and> v \<in> gen_chain P as u)"
by (auto intro!: policy_refl)
(*>*)
lemma (in policy_trans) in_gen_chain_Cons_eq: 
  "P w a \<Longrightarrow> w \<in> gen_chain P (a#as) u <-> w \<leadsto> u"
(*<*)
apply (rule)
apply  (erule gen_chain_implies_policy)
apply (simp only: in_gen_chain_Cons_eq_lemma)
apply (blast intro: gen_chain_refl)
done

lemma gen_chain_mono: 
  "\<forall>w a. P w a \<longrightarrow> Q w a \<Longrightarrow> gen_chain P as u \<subseteq> gen_chain Q as u"
by (induct "as", auto)

(*>*)

constdefs 
  chain :: "sourcef"
 "chain \<equiv> gen_chain (\<lambda>w a. True)"

lemma (in policy_trans) chain_subset_tsources: "chain as u \<subseteq> tsources as u"
(*<*)
by (simp add: chain_def gen_chain_subset_tsources)

lemma chain_Nil [simp]: "chain [] u = {u}"
by (simp add: chain_def)
(*>*)

constdefs
  sources :: "sourcef"
 "sources \<equiv> gen_chain (\<lambda>w a. w = dom a)"

lemma sources_subset_chain: "sources as u \<subseteq> chain as u"
(*<*)
by (unfold sources_def chain_def, rule gen_chain_mono, blast)

lemma singleton_subset_sources: "singleton as u \<subseteq> sources as u"
by (simp only: sources_def singleton_subset_gen_chain)

lemma sources_Nil [simp]: "sources [] u = {u}"
by (simp add: sources_def)

lemma sources_Cons: "sources (a#as) u = sources as u \<union> 
      (if (\<exists>v. dom a \<leadsto> v \<and> v \<in> sources as u) then {dom a} else {})"
by (auto simp: sources_def)

lemma sources_subset_Cons: "sources as u \<subseteq> sources (a#as) u"
by (auto simp add: sources_Cons)

lemma sources_refl: "u \<in> sources as u" 
by (simp add: sources_def gen_chain_refl)

lemma sources_trans: 
  "dom a \<leadsto> v \<Longrightarrow> v \<in> sources as u \<Longrightarrow> dom a \<in> sources (a#as) u"
by (auto simp only: sources_def intro: gen_chain_trans)
lemma rev_sources_trans: 
 "dom a \<notin> sources (a#as) u \<Longrightarrow> \<not>(\<exists>u\<in>sources as u. dom a \<leadsto> u)"
by (auto simp only: sources_def dest: rev_gen_chain_trans)

lemma rev_sources_direct: "dom a \<notin> sources (a#as) u \<Longrightarrow> (dom a \<notleadsto> u)"
by (auto simp only: sources_def dest: rev_gen_chain_direct)

lemma dom_in_sources_Cons_eq_lemma: 
  "dom a \<in> sources (a#as) u <-> (\<exists>v. dom a \<leadsto> v \<and> v \<in> sources as u)"
by (simp only: sources_def in_gen_chain_Cons_eq_lemma)

lemma (in policy_trans) dom_in_sources_Cons_eq: 
  "dom a \<in> sources (a#as) u <-> dom a \<leadsto> u"
by (simp only: sources_def in_gen_chain_Cons_eq)

(*>*)
--{* \pagebreak *}
subsection "unwinding relations"

consts uwr :: "state => domain => state => bool"  ("(_\ \<sim>_\<sim>\ _)"(*<*) [46,46,46] 45(*>*))

axioms
  uwr_s0: "s0 \<sim>u\<sim> s0"
(*<*)

locale uwr_refl = 
  assumes uwr_refl: "s \<sim>u\<sim> s"
locale uwr_trans =
  assumes uwr_trans: "\<lbrakk>r \<sim>u\<sim> s; s \<sim>u\<sim> t\<rbrakk> \<Longrightarrow> r \<sim>u\<sim> t"
(*>*)

constdefs gen_uwr :: "state => domain set => state => bool" 
 (*<*)("(_\ \<approx>_\<approx>\ _)" [46,46,46] 45) (*>*)
 "s \<approx>us\<approx> t \<equiv> \<forall>u\<in>us. s \<sim>u\<sim> t"
(*<*)
lemma gen_uwrI: "(!!u. u\<in>us \<Longrightarrow> s \<sim>u\<sim> t) \<Longrightarrow> s \<approx>us\<approx> t"
by (simp add: gen_uwr_def)

lemma gen_uwrD: "\<lbrakk>s \<approx>us\<approx> t; u\<in>us\<rbrakk> \<Longrightarrow> s \<sim>u\<sim> t"
by (simp add: gen_uwr_def)

lemma gen_uwr_empty [simp]: "s \<approx>{}\<approx> t"
by (auto simp add: gen_uwr_def)

lemma gen_uwr_insert [simp]: "s \<approx>insert u us\<approx> t <-> s \<sim>u\<sim> t \<and> s \<approx>us\<approx> t"
by (auto simp add: gen_uwr_def)
(*
lemma gen_uwr_singleton [simp]: "s \<approx>{u}\<approx> t <-> s \<sim>u\<sim> t"
by (simp)
*)
lemma gen_uwr_Union [simp]: "s \<approx>us \<union> vs\<approx> t <-> s \<approx>us\<approx> t \<and> s \<approx>vs\<approx> t"
by (blast intro: gen_uwrI dest: gen_uwrD)

lemma gen_uwr_s0: "s0 \<approx>us\<approx> s0"
by (rule gen_uwrI, rule uwr_s0)

lemma (in uwr_refl) gen_uwr_refl: "s \<approx>us\<approx> s"
by (rule gen_uwrI, rule uwr_refl)

lemma (in uwr_trans) gen_uwr_trans: "r \<approx>us\<approx> s \<Longrightarrow> s \<approx>us\<approx> t \<Longrightarrow> r \<approx>us\<approx> t"
by (blast intro: gen_uwrI uwr_trans dest: gen_uwrD)

lemma gen_uwr_mono: "s \<approx>vs\<approx> t \<Longrightarrow> us \<subseteq> vs \<Longrightarrow> s \<approx>us\<approx> t"
by (blast intro: gen_uwrI dest: gen_uwrD)

lemma gen_uwr_uwr: 
  "\<lbrakk>s \<approx>us\<approx> t; (!!u. \<lbrakk>s \<sim>u\<sim> t; u \<in> us\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t')\<rbrakk> \<Longrightarrow> s' \<approx>us\<approx> t'"
by (blast intro: gen_uwrI dest: gen_uwrD)
(*>*)

constdefs nest_uwr :: "state => domain => state => bool" 
  (*<*)("(_\ \<simeq>_\<simeq>\ _)" [46,46,46] 45) (*>*)
  "s \<simeq>u\<simeq> t \<equiv> s \<approx>{v. v \<leadsto> u}\<approx> t"

lemma tsources_uwr_is_nest(*<*) [simp](*>*): "s \<approx>tsources as u\<approx> t <-> s \<simeq>u\<simeq> t"
(*<*)
by (simp add: tsources_def nest_uwr_def)

lemma nest_uwrI: "(!!v. v\<leadsto>u \<Longrightarrow> s \<sim>v\<sim> t) \<Longrightarrow> s \<simeq>u\<simeq> t" 
by (auto simp add: nest_uwr_def intro: gen_uwrI)

lemma nest_uwrD: "\<lbrakk>s \<simeq>u\<simeq> t; v \<leadsto> u\<rbrakk> \<Longrightarrow> s \<sim>v\<sim> t" 
by (auto simp add: nest_uwr_def dest: gen_uwrD)

lemma nest_uwr_s0: "s0 \<simeq>u\<simeq> s0" 
by (blast intro: nest_uwrI uwr_s0)

lemma nest_uwr_implies_uwr: "s \<simeq>u\<simeq> t \<Longrightarrow> s \<sim>u\<sim> t"
by (blast intro: policy_refl nest_uwrD)
(*>*)

lemma (in policy_trans) nesting: "\<lbrakk>s \<simeq>v\<simeq> t; u \<leadsto> v\<rbrakk> \<Longrightarrow> s \<simeq>u\<simeq> t" 
(*<*)
by (blast intro: nest_uwrI dest: nest_uwrD policy_trans)

lemma gen_chain_uwr_ConsD: 
 "s \<approx>gen_chain P (a # as) u\<approx> t \<Longrightarrow> 
  (w \<leadsto> v \<longrightarrow> v \<in> gen_chain P as u \<longrightarrow> P w a \<longrightarrow> s \<sim>w\<sim> t) \<and> 
   s \<approx>gen_chain P as u\<approx> t"
by (auto simp add: dest: gen_uwrD)

lemma chain_uwr_ConsD: 
 "s \<approx>chain (a # as) u\<approx> t \<Longrightarrow> (v \<in> chain as u \<longrightarrow> s \<simeq>v\<simeq> t) \<and> s \<approx>chain as u\<approx> t"
by (unfold chain_def, 
       blast intro!: nest_uwrI dest: gen_chain_uwr_ConsD)

lemma sources_uwr_ConsD: 
  "s \<approx>sources (a#as) u\<approx> t \<Longrightarrow> 
  (dom a \<leadsto> v \<longrightarrow> v \<in> sources as u \<longrightarrow> s \<sim>dom a\<sim> t) \<and> 
   s \<approx>sources as u\<approx> t"
by (unfold sources_def, blast dest: gen_chain_uwr_ConsD)

declare gen_chain.Cons [simp del]

lemma (in policy_trans) nest_uwr_implies_gen_chain_uwr: 
 "s \<simeq>u\<simeq> t \<Longrightarrow> s \<approx>gen_chain P as u\<approx> t"
by (blast intro: gen_uwrI nest_uwrD gen_chain_implies_policy)
(*>*)

constdefs 
  output_consistent :: "bool"
 "output_consistent \<equiv> \<forall>u s t. s \<sim>u\<sim> t \<longrightarrow> output u s = output u t"
(*<*)
lemma output_consistentD:
  "\<lbrakk>output_consistent; s \<sim>u\<sim> t\<rbrakk> \<Longrightarrow> output u s = output u t"
by (simp add: output_consistent_def)

(*>*)
(*--{* \pagebreak *}*)
subsection "the deterministic case"

constdefs 
  obs_equiv :: "state => action list => domain => action list => state => bool"
("(_\ \<simeq>_,_,_\<simeq>\ _)"(*<*) [46,46,46,46,46] 45(*>*))
  "s \<simeq>as,u,bs\<simeq> t \<equiv> output u (run as s) = output u (run bs t)"
(*<*)
lemma obs_equivI: "\<lbrakk>output_consistent; run as s \<sim>u\<sim> run bs t\<rbrakk> \<Longrightarrow> s \<simeq>as,u,bs\<simeq> t"
by (unfold obs_equiv_def, erule (1) output_consistentD)
(*>*)

constdefs 
  weakly_step_consistent :: "bool" --{* sufficient also for transitive policies,
new premise @{term "dom a \<leadsto> u"} *}
 "weakly_step_consistent \<equiv> \<forall>a u s t. dom a \<leadsto> u \<longrightarrow> s \<sim>dom a\<sim> t \<longrightarrow> 
                               s \<sim>u\<sim> t \<longrightarrow> step a s \<sim>u\<sim> step a t"
constdefs 
  step_respect :: "bool" --{* a consequence of @{text "local_respect"} *}
 "step_respect \<equiv> \<forall>a u s t. dom a \<notleadsto> u \<longrightarrow> s \<sim>u\<sim> t \<longrightarrow> step a s \<sim>u\<sim> step a t"
(*<*)
lemma weakly_step_consistentD:  
 "\<lbrakk>weakly_step_consistent; s \<sim>u\<sim> t; dom a \<leadsto> u; s \<sim>dom a\<sim> t\<rbrakk> \<Longrightarrow> step a s \<sim>u\<sim> step a t"
by (simp add: weakly_step_consistent_def)

lemma step_respectD: 
  "\<lbrakk>step_respect; s \<sim>u\<sim> t; dom a \<notleadsto> u\<rbrakk> \<Longrightarrow> step a s \<sim>u\<sim> step a t"
by (simp add: step_respect_def)
(*>*)

constdefs
  gen_weak_step_consistent_respect :: "(domain => action => bool) => bool"
 "gen_weak_step_consistent_respect P \<equiv> \<forall>a u s t. (\<forall>w. P w a \<longrightarrow> w\<leadsto>u \<longrightarrow> s \<sim>w\<sim> t) \<longrightarrow> 
                               s \<sim>u\<sim> t \<longrightarrow> step a s \<sim>u\<sim> step a t"

lemma gen_weak_step_consistent_respect_action:
"\<lbrakk>weakly_step_consistent; step_respect\<rbrakk> \<Longrightarrow> 
  gen_weak_step_consistent_respect (\<lambda>w a. w = dom a)"
(*<*)
apply (clarsimp simp add: gen_weak_step_consistent_respect_def)
apply (case_tac "dom a \<leadsto> u")
apply  (blast dest: weakly_step_consistentD)
apply (blast dest: step_respectD)
done
(*>*)

lemma gen_chain_unwinding_step:
"\<lbrakk>s \<approx>gen_chain P (a#as) u\<approx> t; gen_weak_step_consistent_respect P\<rbrakk> \<Longrightarrow> 
  step a s \<approx>gen_chain P as u\<approx> step a t"
(*<*)
apply (rule gen_uwr_uwr)
apply  (erule gen_chain_uwr_ConsD [THEN conjunct2])
apply (simp add: gen_weak_step_consistent_respect_def)
apply (blast dest: gen_chain_uwr_ConsD [THEN conjunct1])
done
(*>*)

lemma sources_unwinding_step: --{* Rushby's Lemma 3 *}
"\<lbrakk>s \<approx>sources (a#as) u\<approx> t; weakly_step_consistent; step_respect\<rbrakk> \<Longrightarrow> 
  step a s \<approx>sources as u\<approx> step a t"
(*<*) 
apply (unfold sources_def)
apply (erule gen_chain_unwinding_step)
apply (erule (1) gen_weak_step_consistent_respect_action)
done
(*>*)
--{* \pagebreak *}

subsection "the nondeterministic case"

--{* TODO: reachability *}

constdefs 
  obs_PO :: "state => action list => domain => action list => state => bool"  
("(_\ \<lesssim>_,_,_\<lesssim>\ _)"(*<*) [46,46,46,46,46] 45(*>*))
  "s \<lesssim>as,u,bs\<lesssim> t \<equiv> \<forall>s'. (s, s') \<in> Run as \<longrightarrow> 
                    (\<exists>t'. (t, t') \<in> Run bs \<and> output u s' = output u t')"
(*<*)
lemma obs_POI: "\<lbrakk>output_consistent; 
\<forall>s'. (s, s') \<in> Run as \<longrightarrow> (\<exists>t'. (t, t') \<in> Run bs \<and> s' \<sim>u\<sim> t')\<rbrakk> \<Longrightarrow> s \<lesssim>as,u,bs\<lesssim> t"
by (unfold obs_PO_def, fast dest: output_consistentD)

(*>*)
subsubsection "simple version"

constdefs 
  Step_consistent :: "bool"
 "Step_consistent \<equiv> \<forall>a u s s' t. dom a \<leadsto> u \<longrightarrow> 
  (s, s') \<in> Step a \<longrightarrow> s \<sim>u\<sim> t \<longrightarrow> (\<exists>t'. (t, t') \<in> Step a \<and> s' \<sim>u\<sim> t')"

  Step_respect :: "bool" --{* a consequence of @{text "Local_respect"} *}
 "Step_respect \<equiv> \<forall>a u s s' t. dom a \<notleadsto> u \<longrightarrow> 
  (s, s') \<in> Step a \<longrightarrow> s \<sim>u\<sim> t \<longrightarrow> (\<exists>t'. (t, t') \<in> Step a \<and> s' \<sim>u\<sim> t')"
(*<*)

lemma Step_consistentD:  
 "\<lbrakk>(s, s') \<in> Step a; Step_consistent; s \<sim>u\<sim> t; dom a \<leadsto> u\<rbrakk> \<Longrightarrow>
  \<exists>t'. (t, t') \<in> Step a \<and> s' \<sim>u\<sim> t'" 
by (simp add: Step_consistent_def)

lemma Step_respectD: 
  "\<lbrakk>Step_respect; (s, s') \<in> Step a; s \<sim>u\<sim> t; dom a \<notleadsto> u\<rbrakk> \<Longrightarrow> 
    \<exists>t'. (t, t') \<in> Step a \<and> s' \<sim>u\<sim> t'" 
by (simp add: Step_respect_def)
(*>*)

lemma simple_unwinding_Step:
      "\<lbrakk>(s, s') \<in> Step a; s \<sim>u\<sim> t; Step_consistent; Step_respect \<rbrakk> \<Longrightarrow> 
  \<exists>t'. (t, t') \<in> Step a \<and> s' \<sim>u\<sim> t'"
(*<*)
apply (case_tac "dom a \<leadsto> u")
apply  (drule (3) Step_consistentD, fast)
apply (blast dest: Step_respectD) 
done
(*>*)

subsubsection "uniform version"

constdefs 
  uni_Step_consistent :: "bool" --{* uniform *}
 "uni_Step_consistent \<equiv> \<forall>a us s s' t. (\<exists>u\<in>us. dom a \<leadsto> u) \<longrightarrow> s \<sim>dom a\<sim> t \<longrightarrow> 
      (s, s') \<in> Step a \<longrightarrow> s \<approx>us\<approx> t \<longrightarrow> 
(\<exists>t'. (t, t') \<in> Step a \<and> s' \<approx>us\<approx> t')"

  uni_Step_respect :: "bool"
 "uni_Step_respect \<equiv> \<forall>a us s t s'.  \<not>(\<exists>u\<in>us. dom a \<leadsto> u) \<longrightarrow> (\<exists>u. u\<in>us) \<longrightarrow>
        (s, s') \<in> Step a \<longrightarrow> s \<approx>us\<approx> t \<longrightarrow> 
  (\<exists>t'. (t, t') \<in> Step a \<and> s' \<approx>us\<approx> t')"
(*<*)
lemma uni_Step_consistentD:  
 "\<lbrakk>(s, s') \<in> Step a; uni_Step_consistent; s \<approx>us\<approx> t; \<exists>u\<in>us. dom a \<leadsto> u; 
   s \<sim>dom a\<sim> t\<rbrakk> \<Longrightarrow> \<exists>t'. (t, t') \<in> Step a \<and> s' \<approx>us\<approx> t'"
by (unfold uni_Step_consistent_def, blast)

lemma uni_Step_respectD [rule_format]: 
  "\<lbrakk>uni_Step_respect; s \<approx>us\<approx> t; \<not>(\<exists>u\<in>us. dom a \<leadsto> u); 
    (s, s') \<in> Step a; u\<in>us\<rbrakk> \<Longrightarrow> \<exists>t'. (t, t') \<in> Step a \<and> s' \<approx>us\<approx> t'" 
by (unfold uni_Step_respect_def, blast)
(*>*)

constdefs
  gen_uni_Step_consistent_respect :: "(domain => action => bool) => bool"
 "gen_uni_Step_consistent_respect P \<equiv> \<forall>a s us t s'. 
   (\<forall>w. P w a \<longrightarrow> (\<exists>u\<in>us. w \<leadsto> u) \<longrightarrow> s \<sim>w\<sim> t) \<longrightarrow> (\<exists>u. u\<in>us) \<longrightarrow> 
         (s, s') \<in> Step a \<longrightarrow> s \<approx>us\<approx> t \<longrightarrow> 
   (\<exists>t'. (t, t') \<in> Step a \<and> s' \<approx>us\<approx> t')"

lemma gen_chain_unwinding_Step:
      "\<lbrakk>(s, s') \<in> Step a; s \<approx>gen_chain P (a#as) u\<approx> t; 
        gen_uni_Step_consistent_respect P\<rbrakk> \<Longrightarrow> 
  \<exists>t'. (t, t') \<in> Step a \<and> s' \<approx>gen_chain P as u\<approx> t'"
(*<*)
apply (frule gen_chain_uwr_ConsD [THEN conjunct2])
apply (simp add: gen_uni_Step_consistent_respect_def)
apply (blast dest: gen_chain_uwr_ConsD [THEN conjunct1] 
       intro: gen_chain_refl)
done

lemma gen_uni_Step_consistent_respect_action:
"\<lbrakk>uni_Step_consistent; uni_Step_respect\<rbrakk> \<Longrightarrow> 
  gen_uni_Step_consistent_respect (\<lambda>w a. w = dom a)"
apply (clarsimp simp add: gen_uni_Step_consistent_respect_def)
apply (case_tac "\<exists>v\<in>us. dom a \<leadsto> v")
apply  (blast dest: uni_Step_consistentD)
apply (blast dest: uni_Step_respectD)
done
(*>*)

lemma sources_unwinding_Step:
      "\<lbrakk>(s, s') \<in> Step a; s \<approx>sources (a#as) u\<approx> t;
        uni_Step_consistent; uni_Step_respect\<rbrakk> \<Longrightarrow> 
  \<exists>t'. (t, t') \<in> Step a \<and> s' \<approx>sources as u\<approx> t'"
(*<*)
apply (unfold sources_def)
apply (erule (1) gen_chain_unwinding_Step)
apply (erule (1) gen_uni_Step_consistent_respect_action)
done
(*>*)

locale Step_functional =
  assumes Step_functional: "\<lbrakk>(x, y) \<in> Step a; (x, z) \<in> Step a\<rbrakk> \<Longrightarrow> y = z"

lemma (in Step_functional) uni_Step_consistent: 
  "Step_respect \<Longrightarrow> Step_consistent \<Longrightarrow> uni_Step_consistent"
(*<*)
apply (simp add: uni_Step_consistent_def, safe)
(*
apply  (clarsimp simp add: Step_consistent_def)
apply  (drule spec, drule_tac x = "{u}" in spec, force)
*)
apply (frule (1) gen_uwrD)
apply (frule (3) Step_consistentD)
apply (clarify, rule exI, rule conjI, assumption)
apply (thin_tac "x \<in> us")
apply (thin_tac "s \<sim>x\<sim> t")
apply (thin_tac "s' \<sim>x\<sim> t'")
apply (thin_tac "dom a \<leadsto> x")
apply (erule gen_uwr_uwr)
apply (case_tac "dom a \<leadsto> u")
apply  (fast dest: Step_consistentD Step_functional)
apply (fast dest: Step_respectD Step_functional)
done
(*>*)

lemma (in Step_functional) uni_Step_respect: "uni_Step_respect = Step_respect"
(*<*)
apply (unfold uni_Step_respect_def, safe)
apply  (clarsimp simp add: Step_respect_def)
apply  (drule spec, drule_tac x = "{u}" in spec, force)
apply (frule (1) gen_uwrD)
apply (frule (2) Step_respectD, blast, clarify)
apply (rule exI, rule conjI, assumption)
apply (erule gen_uwr_uwr)
apply (drule (2) Step_respectD, blast, fast dest: Step_functional)
done

end
(*>*)
(*  Title:      NI/Noninterference.thy
    Id:         $Id: Noninterference.thy,v 1.15 2004/03/03 16:22:59 dvo Exp $
    Author:     David von Oheimb
    License:    (C) 2003 Siemens AG; any non-commercial use is granted

*)
header {* Noninterference *}
(*<*)
theory Noninterference imports Generics begin

(*>*)
subsection "purging"

consts gen_purge :: "sourcef => domain => action list => action list" 
primrec 
  Nil : "gen_purge sf u []     = []"
  Cons: "gen_purge sf u (a#as) = (if dom a \<in> sf (a#as) u then [a] else []) 
                                 @ gen_purge sf u as"

constdefs --{* also for transitive policies *}
  ipurge :: "domain => action list => action list" 
 "ipurge \<equiv> gen_purge sources"
lemma sources_ipurge(*<*) [simp](*>*): "sources (ipurge u as) u = sources as u"
(*<*)
by (unfold sources_def, induct "as", auto simp add: sources_def ipurge_def gen_chain.Cons)

lemma sources_Cons_ipurge: "sources (a # ipurge u as) u = sources (a#as) u"
by (simp add: sources_Cons)

lemma sources_ipurgeD: 
  "v \<in> sources (ipurge u as) u \<Longrightarrow> v \<in> sources as u"
by (simp)

lemma ipurge_Nil [simp]: "ipurge u [] = []"
by (simp add: ipurge_def)

lemma ipurge_Cons [simp]: "ipurge u (a#as) = (if dom a \<in> sources (a#as) u
                          then [a] else []) @ ipurge u as"
by (simp add: ipurge_def)

lemma Nil_ipurge_sourcesD [rule_format]: 
  "[] = ipurge u bs \<longrightarrow> x \<in> sources bs u \<longrightarrow> x = u"
apply (induct "bs")
apply  (auto simp add: ipurge_def sources_Cons)
done

lemma Cons_ipurge_sourcesD: 
 "\<forall>bs. ipurge u as = ipurge u bs \<longrightarrow> sources as u = sources bs u \<Longrightarrow>
  a # ipurge u as = ipurge u bs \<longrightarrow> sources (a # as) u = sources bs u"
apply (induct "bs")
apply  (auto elim!: sources_subset_Cons [THEN subsetD])
apply    (drule spec, erule impE, rule refl, 
          simp add: sources_Cons split add: split_if_asm)+
done

lemma ipurge_sources_cong_lemma [rule_format]: 
 "\<forall>bs. ipurge u as = ipurge u bs \<longrightarrow> sources as u = sources bs u"
apply (induct "as")
apply  (auto simp add: intro: sources_refl dest: Nil_ipurge_sourcesD)
apply     (blast dest: Cons_ipurge_sourcesD)
apply    (blast dest: Cons_ipurge_sourcesD)
apply  (auto simp add: sources_Cons split add: split_if_asm)
done
(*>*)
lemma ipurge_sources_cong: 
  "ipurge u as = ipurge u bs \<Longrightarrow> sources as u = sources bs u"
(*<*)
by (erule ipurge_sources_cong_lemma)
(*>*)
lemma ipurge_idempotent(*<*) [simp](*>*): "ipurge u (ipurge u as) = ipurge u as"
(*<*)
apply (induct "as")
apply (simp_all)
apply clarify
apply (erule swap)
apply (simp add: dom_in_sources_Cons_eq_lemma)
done
(*>*)

constdefs --{* specical case of @{term ipurge} for transitive policies *}
  tpurge   :: "domain => action list => action list"
 "tpurge \<equiv> gen_purge tsources"
lemma tpurge_idempotent(*<*) [simp](*>*): "tpurge u (tpurge u as) = tpurge u as"
(*<*)
by (induct "as", simp_all add: tpurge_def tsources_def)
(*>*)
lemma "tpurge u = filter (\<lambda>a. (dom a \<leadsto> u))" 
(*<*)
by (rule ext, induct_tac "x", auto simp add: tpurge_def tsources_def)
(*>*)
lemma (in policy_trans) tpurge_conincides: "tpurge = ipurge"
(*<*)
apply (unfold ipurge_def tpurge_def)
apply (rule ext)+
apply (induct_tac "xa")
apply  (simp_all only: gen_purge.Nil gen_purge.Cons 
                 tsources_def dom_in_sources_Cons_eq mem_Collect_eq)
done
(*>*)
subsection "the deterministic case"

subsubsection "general version"

constdefs 
  noninterference :: "bool"
 "noninterference \<equiv> \<forall>as u. s0 \<simeq>as,u,ipurge u as\<simeq> s0"

constdefs --{* common structure of @{term "noninterference"} and @{text "noninfluence"} *}
  gen_noninterference :: "sourcef => bool"
 "gen_noninterference sf \<equiv>  
  \<forall>u as s t. s \<approx>sf as u\<approx> t \<longrightarrow> run as s \<sim>u\<sim> run (ipurge u as) t"

lemma output_consistent_and_gen_noninterference_implies_noninterference:
  "output_consistent \<Longrightarrow> gen_noninterference sf \<Longrightarrow> noninterference"
(*<*)
apply (simp add: gen_noninterference_def noninterference_def)
apply (blast intro: gen_uwr_s0 dest: output_consistentD obs_equivI)
done
(*>*)

constdefs 
  local_respect_left :: "bool"
 "local_respect_left \<equiv> \<forall>a u s t. dom a \<notleadsto> u \<longrightarrow> s \<sim>u\<sim> t \<longrightarrow> step a s \<sim>u\<sim> t"

  local_respect_right :: "bool"
 "local_respect_right \<equiv> \<forall>a u s t. dom a \<notleadsto> u \<longrightarrow> s \<sim>u\<sim> t \<longrightarrow> s \<sim>u\<sim> step a t"

  local_respect :: "bool"
 "local_respect \<equiv> local_respect_left \<and> local_respect_right"
(*<*)
lemma local_respect_leftD: 
  "\<lbrakk>local_respect_left; dom a \<notleadsto> u; s \<sim>u\<sim> t\<rbrakk> \<Longrightarrow> step a s \<sim>u\<sim> t"
by (unfold local_respect_left_def, blast)

lemma local_respect_rightD: 
  "\<lbrakk>local_respect_right; dom a \<notleadsto> u; s \<sim>u\<sim> t\<rbrakk> \<Longrightarrow> s \<sim>u\<sim> step a t"
by (unfold local_respect_right_def, blast)

lemma local_respectD: 
  "local_respect \<Longrightarrow> local_respect_left \<and> local_respect_right"
by (unfold local_respect_def, blast)

(*>*)

lemma (in uwr_refl) local_respect_classical: 
  "local_respect \<Longrightarrow> \<forall>a u s. dom a \<notleadsto> u \<longrightarrow> s \<sim>u\<sim> step a s"
(*<*)
by (blast dest: local_respectD local_respect_rightD intro: uwr_refl)
(*>*)
lemma (in uwr_trans) classical_local_respect: 
  "\<forall>s u t. s \<sim>u\<sim> t \<longrightarrow> t \<sim>u\<sim> s \<Longrightarrow>
   \<forall>a u s. dom a \<notleadsto> u \<longrightarrow> s \<sim>u\<sim> step a s \<Longrightarrow> local_respect"
(*<*)
by (unfold local_respect_def local_respect_left_def local_respect_right_def,
    blast dest: uwr_trans)
(*>*)

lemma local_respect_implies_step_respect: "local_respect \<Longrightarrow> step_respect"
(*<*)
apply (unfold step_respect_def)
apply (clarify dest!: local_respectD)
apply (frule (2) local_respect_leftD)
apply (erule (2) local_respect_rightD)
done
(*>*)

lemma gen_noninterference_sources: --{* Rushby's Lemma 5 *}
 "weakly_step_consistent \<Longrightarrow> local_respect \<Longrightarrow> gen_noninterference sources"
(*<*)
apply (unfold gen_noninterference_def, rule, rule)
apply (induct_tac "as")
apply  (auto split del: split_if)
apply (drule spec, drule spec, erule mp)
apply (auto)
apply  (drule local_respect_implies_step_respect)
apply  (erule (2) sources_unwinding_step)
apply (rule gen_uwr_uwr)
apply  (erule sources_uwr_ConsD [THEN conjunct2])
apply (blast dest: local_respectD local_respect_leftD sources_trans)
done
(*>*)

theorem noninterference: --{* Rushby's Theorem 7 *}
"\<lbrakk>weakly_step_consistent; local_respect; output_consistent\<rbrakk> \<Longrightarrow> noninterference"
(*<*)
by (blast intro: gen_noninterference_sources
    output_consistent_and_gen_noninterference_implies_noninterference)

(*>*)
subsubsection "simple version"

constdefs
 step_consistent :: "bool" --{* new premise @{term "dom a \<leadsto> u"} *}
"step_consistent \<equiv> \<forall>a u s t. dom a \<leadsto> u \<longrightarrow> s \<sim>u\<sim> t \<longrightarrow> step a s \<sim>u\<sim> step a t"

theorem simple_noninterference: --{* Rushby's Theorem 1 *}
 "step_consistent \<Longrightarrow> local_respect \<Longrightarrow> gen_noninterference singleton"
(*<*)
apply (simp add: gen_noninterference_def, rule, rule)
apply (induct_tac "as")
apply  (auto split del: split_if)
apply (drule spec, drule spec, erule mp)
apply (auto)
apply  (case_tac "dom a \<leadsto> u")
apply   (simp add: step_consistent_def)
apply  (blast 
         dest: local_respect_implies_step_respect [THEN step_respectD])
apply (blast dest: rev_sources_direct local_respectD local_respect_leftD)
done

lemma simple_noninterference_implies_gen_noninterference_sources:
  "gen_noninterference singleton \<Longrightarrow> gen_noninterference sources"
by (unfold gen_noninterference_def, 
    blast intro: gen_uwr_mono [OF _ singleton_subset_sources])

(*>*)
subsubsection "strong version"
(*
constdefs
  strong_gen_noninterference :: "sourcef => bool"
 "strong_gen_noninterference sf \<equiv> \<forall>u as s t bs. s \<approx>sf as u\<approx> t \<longrightarrow> 
   gen_purge sf u as = gen_purge sf u bs \<longrightarrow> run as s \<sim>u\<sim> run bs t"

lemma gen_purge_nilD [rule_format]: "local_respect_right \<Longrightarrow> 
  [] = gen_purge sf u bs \<longrightarrow> (\<forall>t. s \<sim>u\<sim> t \<longrightarrow> s \<sim>u\<sim> run bs t)"
apply (induct "bs")
apply  (simp_all)
apply (clarify)
apply (drule sym, erule (1) impE)
apply (drule spec, erule mp)
#
apply (blast dest: local_respect_rightD rev_sources_direct)
done

lemma gen_purge_consD [rule_format]: 
 "local_respect_right \<Longrightarrow> a # as = ipurge u bs  \<longrightarrow>
  (\<exists>bsa bsc. bs = bsa @ a # bsc \<and> (\<forall>t. s \<approx>sources (a#as) u\<approx> t \<longrightarrow> s \<approx>sources (a#as) u\<approx> run bsa t) \<and> as = ipurge u bsc)"
apply (induct "bs") 
apply  (simp_all)
apply (rule conjI)
apply  (clarify, rule_tac x = "[]" in exI, simp)
apply (clarsimp)
apply (rule exI)+
apply (rule conjI)
apply  (rule append_Cons [symmetric])
apply (clarsimp)
apply (drule spec, erule mp)
apply (blast dest: local_respect_rightD rev_sources_trans gen_unwindingD
       intro!: gen_unwindingI)
done

lemma strong_noninterference:
 "weakly_step_consistent \<Longrightarrow> local_respect \<Longrightarrow> strong_noninterference"
apply (subgoal_tac "\<forall>u as bs s t. ipurge u as = ipurge u bs \<longrightarrow> 
                    s \<approx>sources as u\<approx> t \<longrightarrow> run as s \<sim>u\<sim> run bs t")
apply  (unfold strong_noninterference_def, blast)
apply (rule, rule, simp)
apply (frule local_respectD, erule conjE)
apply (induct_tac "as")
apply  (auto)
apply   (erule (2) ipurge_nilD)
apply  (frule (1) ipurge_consD, clarify)
apply  (drule spec, erule (1) impE)
apply  (thin_tac "a # ?as = ipurge u ?bs")
apply  (thin_tac "ipurge u list = ipurge u bsc")
apply  (simp add: sources_Cons_ipurge)
apply  (drule spec, drule spec, erule mp)
apply  (drule spec, erule (1) impE)
apply  (drule local_respect_implies_step_respect)
apply  (blast dest: sources_unwinding_step) 
apply (drule spec, erule impE, rule refl)
apply (drule spec, drule spec, erule mp)
apply (drule sources_unwinding_ConsD [THEN conjunct2])
apply (rule gen_unwindingI)
apply (blast dest: local_respect_leftD gen_unwindingD rev_sources_trans)
done
*)
constdefs
  strong_noninterference :: "bool"
 "strong_noninterference \<equiv> \<forall>as u bs. ipurge u as = ipurge u bs \<longrightarrow> s0 \<simeq>as,u,bs\<simeq> s0"

lemma strong_noninterference_implies_noninterference:
 "strong_noninterference \<Longrightarrow> noninterference"
(*<*)
apply (unfold strong_noninterference_def noninterference_def obs_equiv_def)
apply (clarify)
apply (drule spec)+
apply (erule mp)
apply (simp only: ipurge_idempotent)
done

lemma gen_noninterference_sources_left [rule_format]:
"weakly_step_consistent \<Longrightarrow> local_respect \<Longrightarrow> 
\<forall>u as s t. s \<approx>sources as u\<approx> t \<longrightarrow> run (ipurge u as) s \<sim>u\<sim> run as t"
apply (rule, rule)
apply (induct_tac "as")
apply  (auto split del: split_if)
apply (drule spec, drule spec, erule mp)
apply (auto)
apply  (drule local_respect_implies_step_respect)
apply  (erule (2) sources_unwinding_step)
apply (rule gen_uwr_uwr)
apply  (erule sources_uwr_ConsD [THEN conjunct2])
apply (blast dest: local_respectD local_respect_rightD 
             intro: sources_trans)
done

lemma strong_noninterference00:
"\<lbrakk>weakly_step_consistent; local_respect; output_consistent\<rbrakk> \<Longrightarrow> strong_noninterference"
apply (unfold strong_noninterference_def obs_equiv_def, clarify)
apply (rule trans)
defer 1
apply  (erule output_consistentD)
apply  (erule (1) gen_noninterference_sources_left)
apply  (rule gen_uwr_s0)
apply (erule output_consistentD)
apply (drule (1) gen_noninterference_sources)
apply (drule sym)
apply (simp add: gen_noninterference_def gen_uwr_s0)
done

lemma strong_noninterference0:
"output_consistent \<Longrightarrow> gen_noninterference sources \<Longrightarrow> strong_noninterference"
apply (unfold strong_noninterference_def obs_equiv_def gen_noninterference_def)
apply (clarify)
apply (rule trans)
apply  (erule output_consistentD)
apply  (blast intro: gen_uwr_s0)
apply (rule sym)
apply (erule output_consistentD)
apply (simp add: gen_uwr_s0)
done
(*>*)

lemma ipurge_nilD [rule_format]: "local_respect_right \<Longrightarrow> 
  [] = ipurge u bs \<longrightarrow> (\<forall>t. s \<sim>u\<sim> t \<longrightarrow> s \<sim>u\<sim> run bs t)"
(*<*)
apply (induct "bs")
apply  (simp_all)
apply (blast intro: sym 
       dest: local_respect_rightD rev_sources_direct)
done

lemma ipurge_consD0 [rule_format]: --{* unused *}
 "local_respect_right \<Longrightarrow> a # as = ipurge u bs \<longrightarrow> 
   (\<exists>bsa bsc. bs = bsa @ a # bsc \<and> as = ipurge u bsc \<and> 
   (\<forall>t. s \<sim>u\<sim> t \<longrightarrow> s \<sim>u\<sim> run bsa t))"
apply (induct "bs") 
apply  (simp_all)
apply (rule conjI)
apply  (clarify, rule_tac x = "[]" in exI, simp)
apply (clarsimp)
apply (rule exI)+
apply (rule conjI)
apply  (rule append_Cons [symmetric])
apply (simp)
apply (blast dest: local_respect_rightD rev_sources_direct)
done
(*>*)

lemma ipurge_consD [rule_format]: 
 "local_respect_right \<Longrightarrow> a # as = ipurge u bs  \<longrightarrow>
  (\<exists>bsa bsc. bs = bsa @ a # bsc \<and> as = ipurge u bsc \<and> 
(\<forall>t. s \<approx>sources (a#as) u\<approx> t \<longrightarrow> s \<approx>sources (a#as) u\<approx> run bsa t))"
(*<*)
apply (induct "bs") 
apply  (simp_all)
apply (rule conjI)
apply  (clarify, rule_tac x = "[]" in exI, simp)
apply (clarsimp)
apply (rule exI)+
apply (rule conjI)
apply  (rule append_Cons [symmetric])
apply (clarsimp)
apply (drule spec, erule mp)
apply (drule rev_sources_trans)
apply (blast dest: local_respect_rightD gen_uwrD intro!: gen_uwrI)
done
(*>*)

theorem strong_noninterference:
 "\<lbrakk>weakly_step_consistent; local_respect; output_consistent\<rbrakk> \<Longrightarrow> strong_noninterference"
(*<*)
apply (subgoal_tac "\<forall>u as bs s t. ipurge u as = ipurge u bs \<longrightarrow> 
                    s \<approx>sources as u\<approx> t \<longrightarrow> run as s \<sim>u\<sim> run bs t")
apply  (unfold strong_noninterference_def obs_equiv_def)
apply  (fast elim!: output_consistentD intro: gen_uwr_s0)
apply (rule, rule, simp)
apply (frule local_respectD)
apply (induct_tac "as")
apply  (auto)
apply   (erule (2) ipurge_nilD)
apply  (frule (1) ipurge_consD, clarify)
apply  (drule spec, erule (1) impE)
apply  (thin_tac "a # ?as = ipurge u ?bs")
apply  (thin_tac "ipurge u list = ipurge u bsc")
apply  (simp add: sources_Cons_ipurge)
apply  (drule spec, drule spec, erule mp)
apply  (drule spec, erule (1) impE)
apply  (drule local_respect_implies_step_respect)
apply  (blast dest: sources_unwinding_step) 
apply (drule spec, erule impE, rule refl)
apply (drule spec, drule spec, erule mp)
apply (drule sources_uwr_ConsD [THEN conjunct2])
apply (rule gen_uwrI)
apply (blast dest: local_respect_leftD gen_uwrD rev_sources_trans)
done
(*>*)
(*
subsubsection "access control interpretation"

typedecl "name"
typedecl "value"
consts contents :: "state => name => value"

consts observe :: "domain => name set"
       alter   :: "domain => name set"

defs uwr_def: "s \<sim>u\<sim> t \<equiv> \<forall>n\<in>observe u. contents s n = contents t n"

locale canonical_output = --{* special case: all observable values are output *}
  fixes value2output :: "value => output" --{* type coercion *}
  assumes output_def: 
     "output u s \<equiv> {value2output (contents s n) |n. n \<in> observe u}"
lemma (in canonical_output) canonical_output_consistent: "output_consistent"
*)(*<*)
(*apply (auto simp add: output_consistent_def uwr_def output_def)
apply (rule_tac x = "n" in exI)
apply (simp)
done
*)(*>*)
(*
constdefs --{* Reference Monitor Assumptions *}
  RMA1 :: "bool"
 "RMA1 \<equiv> output_consistent"

  RMA2 :: "bool" --{* new premises @{term "dom a \<leadsto> u"}, @{term "s \<sim>u\<sim> t"}, and @{term "n \<in> observe u"} *}
 "RMA2 \<equiv> \<forall>a u s t n. s \<sim>dom a\<sim> t \<longrightarrow> dom a \<leadsto> u \<longrightarrow> s \<sim>u\<sim> t \<longrightarrow> n \<in> observe u \<longrightarrow> 
                      (contents (step a s) n \<noteq> contents s n \<or> 
                       contents (step a t) n \<noteq> contents t n) \<longrightarrow> 
                       contents (step a s) n = contents (step a t) n"

  RMA3 :: "bool"
 "RMA3 \<equiv> \<forall>a s n. contents (step a s) n \<noteq> contents s n \<longrightarrow> n \<in> alter (dom a)"

  AC_policy_consistent :: "bool"
 "AC_policy_consistent \<equiv> \<forall>u v. alter u \<inter> observe v \<noteq> {} \<longrightarrow> u \<leadsto> v"
*)(*<*)
(*lemma AC_policy_consistent_revD: 
  "AC_policy_consistent \<Longrightarrow> n \<in> observe v \<Longrightarrow> u \<notleadsto> v \<Longrightarrow> n \<notin> alter u"
by (unfold AC_policy_consistent_def, blast)

lemma AC_unwinding_weakly_step_consistentI:
  "(!!a u s t n. \<lbrakk>dom a \<leadsto> u; s \<sim>dom a\<sim> t; s \<sim>u\<sim> t; n \<in> observe u; 
                  contents (step a s) n \<noteq> contents s n \<or> 
                  contents (step a t) n \<noteq> contents t n\<rbrakk> \<Longrightarrow> 
                  contents (step a s) n = contents (step a t) n)
 \<Longrightarrow> weakly_step_consistent"
apply (clarsimp simp add: weakly_step_consistent_def uwr_def)
apply (case_tac "contents (step a s) n = contents s n \<and> 
                 contents (step a t) n = contents t n")
apply  (auto)
done
(*>*)

lemma RMA2_implies_weakly_step_consistent: "RMA2 \<Longrightarrow> weakly_step_consistent"
(*<*)
by (rule AC_unwinding_weakly_step_consistentI, simp add: RMA2_def)
(*>*)

lemma RMA3_AC_policy_consistent_implies_local_respect: 
  "RMA3 \<Longrightarrow> AC_policy_consistent \<Longrightarrow> local_respect"
(*<*)
apply (unfold RMA3_def uwr_def
       local_respect_def local_respect_left_def local_respect_right_def)
apply (safe)
apply  (drule (1) bspec, drule sym, simp, blast dest: AC_policy_consistent_revD)
apply (drule (1) bspec, simp, blast dest: sym AC_policy_consistent_revD)
done
(*>*)

theorem access_control_secure: 
  "\<lbrakk>RMA1; RMA2; RMA3; AC_policy_consistent\<rbrakk> \<Longrightarrow> noninterference"
(*<*)
by (auto simp: RMA1_def 
 intro!: noninterference RMA2_implies_weakly_step_consistent
 elim: RMA3_AC_policy_consistent_implies_local_respect)

(*>*)
*)
subsection "the nondeterministic case"

constdefs 
  Noninterference :: "bool"
 "Noninterference \<equiv> \<forall>as u bs. ipurge u as = ipurge u bs \<longrightarrow> s0 \<lesssim>as,u,bs\<lesssim> s0"

  gen_Noninterference :: "sourcef => bool"
 "gen_Noninterference sf \<equiv> \<forall>as bs s s' u t. ipurge u as = ipurge u bs \<longrightarrow> 
         (s, s') \<in> Run as \<longrightarrow> s \<approx>sf as u\<approx> t \<longrightarrow> 
   (\<exists>t'. (t, t') \<in> Run bs \<and> s' \<sim>u\<sim> t')"
lemma 
  output_consistent_and_gen_Noninterference_implies_Noninterference:
  "output_consistent \<Longrightarrow> gen_Noninterference sf \<Longrightarrow> Noninterference"
(*<*)
apply (unfold Noninterference_def gen_Noninterference_def)
apply (blast intro: gen_uwr_s0 dest: output_consistentD obs_POI)
done
(*>*)
subsubsection "simple version"

constdefs 
  Local_respect_left :: "bool"
 "Local_respect_left \<equiv> \<forall>a u s t s'. dom a \<notleadsto> u \<longrightarrow> 
  s \<sim>u\<sim> t \<longrightarrow> (s, s') \<in> Step a \<longrightarrow> s' \<sim>u\<sim> t"

  Local_respect_right :: "bool"
 "Local_respect_right \<equiv> \<forall>a u s t. dom a \<notleadsto> u \<longrightarrow> 
  s \<sim>u\<sim> t \<longrightarrow> (\<exists>t'. (t, t') \<in> Step a \<and> s \<sim>u\<sim> t')"
(*<*)
lemma Local_respect_leftD: 
 "\<lbrakk>Local_respect_left; dom a \<notleadsto> u; (s, s') \<in> Step a; s \<sim>u\<sim> t\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t" 
by (unfold Local_respect_left_def, blast)

lemma Local_respect_rightD: 
  "\<lbrakk>Local_respect_right; dom a \<notleadsto> u; s \<sim>u\<sim> t\<rbrakk> \<Longrightarrow> \<exists>t'. (t, t') \<in> Step a \<and> s \<sim>u\<sim> t'"
by (unfold Local_respect_right_def, blast)
(*>*)

lemma Local_respect_implies_Step_respect:
 "\<lbrakk>Local_respect_left; Local_respect_right\<rbrakk> \<Longrightarrow> Step_respect"
(*<*)
by (unfold Step_respect_def, blast dest: Local_respect_leftD Local_respect_rightD)
(*>*)

lemma (in uwr_refl) Local_respect_left_Mantel: 
  "Local_respect_left \<Longrightarrow> 
   \<forall>a u s t s'. dom a \<notleadsto> u \<longrightarrow> (s, s') \<in> Step a \<longrightarrow> s' \<sim>u\<sim> s"
(*<*)
by (blast dest: Local_respect_leftD intro: uwr_refl)
(*>*)

lemma (in uwr_refl) Local_respect_right_Mantel: 
  "Local_respect_right \<Longrightarrow> 
   \<forall>a u s t. dom a \<notleadsto> u \<longrightarrow> (\<exists>t'. (t, t') \<in> Step a \<and> t \<sim>u\<sim> t')"
(*<*)
by (blast dest: Local_respect_rightD intro: uwr_refl)
(*>*)

lemma (in uwr_trans) Mantel_Local_respect_left: 
  "\<forall>a u s t s'. dom a \<notleadsto> u \<longrightarrow> (s, s') \<in> Step a \<longrightarrow> s' \<sim>u\<sim> s \<Longrightarrow> 
   Local_respect_left"
(*<*)
by (unfold Local_respect_left_def, blast dest: uwr_trans)
(*>*)

lemma (in uwr_trans) Mantel_Local_respect_right: 
  "\<forall>a u s t. dom a \<notleadsto> u \<longrightarrow> (\<exists>t'. (t, t') \<in> Step a \<and> t \<sim>u\<sim> t') \<Longrightarrow> 
   Local_respect_right"
(*<*)
by (unfold Local_respect_right_def, blast dest: uwr_trans)
(*>*)

lemma ipurge_NilD [rule_format]: "Local_respect_right \<Longrightarrow> 
  [] = ipurge u bs \<longrightarrow> (\<forall>t. s \<sim>u\<sim> t \<longrightarrow> (\<exists>t'. (t, t') \<in> Run bs \<and> s \<sim>u\<sim> t'))"
(*<*)
apply (induct "bs")
apply  (simp_all)
apply (blast intro: sym 
       dest: Local_respect_rightD rev_sources_direct)
done
(*>*)

lemma ipurge_ConsD [rule_format]: "Local_respect_right \<Longrightarrow> 
  a # as = ipurge u bs \<longrightarrow> (\<exists>bsa bsc. bs = bsa @ a # bsc \<and> as = ipurge u bsc \<and>
  (\<forall>t. s \<sim>u\<sim> t \<longrightarrow> (\<exists>ta. (t, ta) \<in> Run bsa \<and> s \<sim>u\<sim> ta)))"
(*<*)
apply (induct "bs") 
apply  (simp_all)
apply (rule conjI)
apply  (clarify, rule_tac x = "[]" in exI, simp)
apply (clarsimp)
apply (rule exI)+
apply (rule conjI)
apply  (rule append_Cons [symmetric])
apply (simp)
apply (blast dest: Local_respect_rightD rev_sources_direct)
done

theorem simple_Noninterference_lemma: 
 "Step_consistent \<Longrightarrow> Local_respect_left \<Longrightarrow> Local_respect_right \<Longrightarrow> 
  gen_Noninterference singleton"
apply (subgoal_tac "\<forall>u as s' s bs t. (s, s')\<in>Run as \<longrightarrow> 
                    ipurge u as = ipurge u bs \<longrightarrow> s \<sim>u\<sim> t \<longrightarrow> 
                  (\<exists>t'. (t, t')\<in>Run bs \<and> s' \<sim>u\<sim> t')")
apply  (simp add: gen_Noninterference_def)
apply (rule, rule, rule, simp)
apply (induct_tac "as")
apply (auto split del: split_if)
apply  (fast elim!: ipurge_NilD)
apply (rename_tac sa sb sc bs t)
apply (drule spec, erule (1) impE)
apply (simp split add: split_if_asm)
apply  (frule (1) ipurge_ConsD, clarify)
apply  (drule spec, erule (1) impE)
apply  (thin_tac "a # ?as = ipurge u ?bs")
apply  (thin_tac "ipurge u list = ipurge u bsc")
apply  (simp)
apply  (drule spec, erule (1) impE, clarify)
apply  (drule (1) Local_respect_implies_Step_respect) 
apply  (thin_tac "sa \<sim>u\<sim> t")
apply  (drule (3) simple_unwinding_Step, blast)
apply (blast dest: rev_sources_direct Local_respect_leftD)
done
(*>*)

theorem simple_Noninterference: 
 "Step_consistent \<Longrightarrow> Local_respect_left \<Longrightarrow> Local_respect_right \<Longrightarrow> 
  output_consistent \<Longrightarrow> Noninterference"
(*<*)
apply (drule (2) simple_Noninterference_lemma)
apply (simp add: Noninterference_def gen_Noninterference_def)
apply (blast intro: uwr_s0 dest: output_consistentD obs_POI)
done
(*>*)

subsubsection "uniform version"

constdefs
  uni_Local_respect_right :: "bool"
 "uni_Local_respect_right \<equiv> \<forall>a us s t. \<not>(\<exists>u\<in>us. dom a \<leadsto> u) \<longrightarrow> (\<exists>u. u\<in>us) \<longrightarrow>
  s \<approx>us\<approx> t \<longrightarrow> (\<exists>t'. (t, t') \<in> Step a \<and> s \<approx>us\<approx> t')"
 
  uni_Local_respect :: "bool"
 "uni_Local_respect \<equiv> Local_respect_left \<and> uni_Local_respect_right"

lemma uni_Local_respect_leftD: "\<lbrakk>Local_respect_left; 
  (s, s') \<in> Step a; \<not>(\<exists>u\<in>us. dom a \<leadsto> u); s \<approx>us\<approx> t\<rbrakk> \<Longrightarrow> s' \<approx>us\<approx> t" 
(*<*)
apply (rule gen_uwrI)
apply (drule (1) gen_uwrD)
apply (blast dest: Local_respect_leftD)
done

lemma uni_Local_respect_rightD: 
  "\<lbrakk>uni_Local_respect_right; \<not>(\<exists>u\<in>us. dom a \<leadsto> u); u\<in>us; s \<approx>us\<approx> t\<rbrakk> \<Longrightarrow> 
    \<exists>t'. (t, t') \<in> Step a \<and> s \<approx>us\<approx> t'"
by (unfold uni_Local_respect_right_def, blast)

lemma uni_Local_respectD: 
  "uni_Local_respect \<Longrightarrow> Local_respect_left \<and> uni_Local_respect_right"
by (unfold uni_Local_respect_def, blast)
(*>*)

lemma uni_Local_respect_right_implies_Local_respect_right: 
  "uni_Local_respect_right \<Longrightarrow> Local_respect_right"
(*<*)
apply (unfold Local_respect_right_def uni_Local_respect_right_def, clarify)
apply (drule spec, drule_tac x = "{u}" in spec, auto)
done
(*>*)

lemma uni_Local_respect_implies_uni_Step_respect: 
  "uni_Local_respect \<Longrightarrow> uni_Step_respect"
(*<*)
by (unfold uni_Step_respect_def, blast dest: uni_Local_respectD 
    uni_Local_respect_leftD uni_Local_respect_rightD)
(*>*)

lemma uni_ipurge_ConsD [rule_format]: "uni_Local_respect_right \<Longrightarrow> 
  a # as = ipurge u bs \<longrightarrow> (\<exists>bsa bsc. bs = bsa @ a # bsc \<and> as = ipurge u bsc \<and> 
  (\<forall>t. s \<approx>sources (a#as) u\<approx> t \<longrightarrow> (\<exists>ta. (t, ta) \<in> Run bsa \<and> s \<approx>sources (a#as) u\<approx> ta)))"
(*<*)
apply (induct "bs") 
apply  (simp_all)
apply (rule conjI)
apply  (clarify, rule_tac x = "[]" in exI, simp)
apply (clarsimp)
apply (rule exI)+
apply (rule conjI)
apply  (rule append_Cons [symmetric])
apply (clarsimp)
apply (drule rev_sources_trans)
apply (drule (1) uni_Local_respect_rightD, rule sources_refl, erule asm_rl)
apply (blast)
done
(*>*)

lemma gen_Noninterference_sources: 
 "uni_Step_consistent \<Longrightarrow> uni_Local_respect \<Longrightarrow> gen_Noninterference sources"
(*<*)
apply (subgoal_tac "\<forall>u as s' s bs t. (s, s')\<in>Run as \<longrightarrow> 
                    ipurge u as = ipurge u bs \<longrightarrow> s \<approx>sources as u\<approx> t \<longrightarrow> 
                  (\<exists>t'. (t, t')\<in>Run bs \<and> s' \<sim>u\<sim> t')")
apply  (unfold gen_Noninterference_def, blast)
apply (rule, rule, rule, simp)
apply (frule uni_Local_respectD, erule conjE)
apply (induct_tac "as")
apply  (auto split del: split_if)
apply  (drule uni_Local_respect_right_implies_Local_respect_right)
apply  (fast elim!: ipurge_NilD)
apply (rename_tac sa sb sc bs t)
apply (drule spec, erule (1) impE)
apply (simp split add: split_if_asm)
apply  (frule (1) uni_ipurge_ConsD, clarify)
apply  (drule spec, erule (1) impE)
apply  (thin_tac "a # ?as = ipurge u ?bs")
apply  (thin_tac "ipurge u list = ipurge u bsc")
apply  (simp add: sources_Cons_ipurge)
apply  (drule spec, erule (1) impE, clarify)
apply  (drule uni_Local_respect_implies_uni_Step_respect)
apply  (thin_tac "sa \<approx>sources (a # list) u\<approx> t")
apply  (drule (3) sources_unwinding_Step) 
apply  (blast)
apply (drule spec, erule impE, rule refl) 
apply (drule sources_uwr_ConsD [THEN conjunct2])
apply (blast dest: uni_Local_respect_leftD rev_sources_trans)
done
(*>*)

theorem Noninterference: "uni_Step_consistent \<Longrightarrow> 
 uni_Local_respect \<Longrightarrow> output_consistent \<Longrightarrow> Noninterference"
(*<*)
by (blast intro: gen_Noninterference_sources 
    output_consistent_and_gen_Noninterference_implies_Noninterference)

end
(*>*)
(*  Title:      NI/Nonleakage.thy
    Id:         $Id: Nonleakage.thy,v 1.6 2004/01/29 17:36:47 dvo Exp $
    Author:     David von Oheimb
    License:    (C) 2003 Siemens AG; any non-commercial use is granted

*)
header {* Nonleakage *}

(*<*)
theory Nonleakage imports Generics begin

(*>*)
subsection "the deterministic case"

constdefs --{* generic nonleakage *}
  gen_nonleakage :: "sourcef => bool" 
 "gen_nonleakage sf \<equiv> \<forall>as s u t. s \<approx>sf as u\<approx> t \<longrightarrow> run as s \<sim>u\<sim> run as t"
(*<*)
lemma gen_nonleakage: 
  "gen_weak_step_consistent_respect P \<Longrightarrow> gen_nonleakage (gen_chain P)"
apply (unfold gen_nonleakage_def, rule)
apply (induct_tac "as")
apply  (auto)
apply ((drule spec)+, erule mp)
apply (erule (1) gen_chain_unwinding_step)
done
(*>*)

constdefs
  nonleakage :: "bool" 
 "nonleakage \<equiv> \<forall>as s u t. s \<approx>sources as u\<approx> t \<longrightarrow> s \<simeq>as,u,as\<simeq> t"

theorem nonleakage:
   "\<lbrakk>weakly_step_consistent; step_respect; output_consistent\<rbrakk> \<Longrightarrow> nonleakage"
(*<*)
apply (drule (1) gen_weak_step_consistent_respect_action)
apply (drule gen_nonleakage)
apply (auto simp add: gen_nonleakage_def nonleakage_def sources_def)
apply (blast intro!: obs_equivI)
done
(*>*)

subsubsection "weak nonleakage"

constdefs
  weak_nonleakage :: "bool" 
 "weak_nonleakage \<equiv> \<forall>as s u t. s \<approx>chain as u\<approx> t \<longrightarrow> s \<simeq>as,u,as\<simeq> t"

lemma nonleakage_implies_weak_nonleakage: "nonleakage \<Longrightarrow> weak_nonleakage"
(*<*)
apply (unfold nonleakage_def weak_nonleakage_def)
apply (blast intro: gen_uwr_mono [OF _ sources_subset_chain])
done
(*>*)

constdefs
  weak_step_consistent_respect :: "bool"
 "weak_step_consistent_respect \<equiv> \<forall>s u t. s \<simeq>u\<simeq> t \<longrightarrow> (\<forall>a. step a s \<sim>u\<sim> step a t)"

lemma weak_step_consistent_respect_is_gen_weak_step_consistent_respect_True:
 "weak_step_consistent_respect = gen_weak_step_consistent_respect (\<lambda>w a. True)" 
(*<*)
apply (unfold weak_step_consistent_respect_def gen_weak_step_consistent_respect_def)
apply (blast dest: nest_uwrD nest_uwr_implies_uwr
             intro: nest_uwrI)
done

lemma chain_unwinding_step: (* unused *)
 "\<lbrakk>s \<approx>chain (a # as) u\<approx> t; weak_step_consistent_respect\<rbrakk> \<Longrightarrow> 
   step a s \<approx>chain as u\<approx> step a t"
apply (unfold chain_def)
apply (erule gen_chain_unwinding_step)
apply (simp add:
   weak_step_consistent_respect_is_gen_weak_step_consistent_respect_True)
done
(*>*)

theorem weak_nonleakage: 
  "\<lbrakk>weak_step_consistent_respect; output_consistent\<rbrakk> \<Longrightarrow> weak_nonleakage"
(*<*)
apply (simp only:
       weak_step_consistent_respect_is_gen_weak_step_consistent_respect_True)
apply (drule gen_nonleakage)
apply (unfold gen_nonleakage_def weak_nonleakage_def chain_def)
apply (blast intro!: obs_equivI)
done
(*>*)

subsubsection "transitive weak nonleakage"

constdefs
  trans_weak_nonleakage :: "bool" 
 "trans_weak_nonleakage \<equiv> \<forall>s u t. s \<simeq>u\<simeq> t \<longrightarrow> (\<forall>as. s \<simeq>as,u,as\<simeq> t)"

lemma (in policy_trans) weak_nonleakage_implies_trans_weak_nonleakage:
  "weak_nonleakage \<Longrightarrow> trans_weak_nonleakage"
(*<*)
apply (unfold weak_nonleakage_def trans_weak_nonleakage_def)
apply (force intro: gen_uwr_mono [OF _ chain_subset_tsources])
done

lemma (in policy_trans) nest_uwr_step: (* unnecessary *)
 "\<lbrakk>weak_step_consistent_respect; s \<simeq>u\<simeq> t\<rbrakk> \<Longrightarrow> step a s \<simeq>u\<simeq> step a t"
apply (rule nest_uwrI)
apply (unfold weak_step_consistent_respect_def)
apply (fast dest: nesting)
done
(*>*)

theorem (in policy_trans) trans_weak_nonleakage: 
  "\<lbrakk>weak_step_consistent_respect; output_consistent\<rbrakk> \<Longrightarrow> trans_weak_nonleakage"
(*<*)
(*
apply (unfold trans_weak_nonleakage_def gen_nonleakage_def, rule, rule)
apply (induct_tac "as")
apply  (auto)
apply (erule nest_uwr_implies_uwr)
apply (drule spec, drule spec, erule mp)
apply (erule (1) nest_uwr_step)
*)
by (blast intro: weak_nonleakage weak_nonleakage_implies_trans_weak_nonleakage)

(*>*)
--{* \pagebreak *}
subsection "the nondeterministic case"

constdefs 
  gen_Nonleakage :: "sourcef => bool"
 "gen_Nonleakage sf \<equiv> \<forall>u as s s' t.
        (s, s') \<in> Run as \<longrightarrow> s \<approx>sf as u\<approx> t \<longrightarrow> 
  (\<exists>t'. (t, t') \<in> Run as \<and> s' \<sim>u\<sim> t')"

lemma gen_Nonleakage:
 "gen_uni_Step_consistent_respect P \<Longrightarrow> gen_Nonleakage (gen_chain P)"
(*<*)
apply (unfold gen_Nonleakage_def, rule, rule)
apply (induct_tac "as")
apply  (auto)
apply (rename_tac "s" "ss" "s'")
apply (drule (2) gen_chain_unwinding_Step)
apply (blast)
done
(*>*)

constdefs 
  Nonleakage :: "bool"
 "Nonleakage \<equiv> \<forall>as s u t. s \<approx>sources as u\<approx> t \<longrightarrow> s \<lesssim>as,u,as\<lesssim> t"

theorem Nonleakage:
 "\<lbrakk>uni_Step_consistent; uni_Step_respect; output_consistent\<rbrakk> \<Longrightarrow> Nonleakage"
(*<*)
apply (drule (1) gen_uni_Step_consistent_respect_action)
apply (drule gen_Nonleakage)
apply (unfold gen_Nonleakage_def Nonleakage_def sources_def)
apply (blast intro!: obs_POI)
done
(*>*)

subsubsection "weak Nonleakage"

constdefs
  weak_Nonleakage :: "bool" 
 "weak_Nonleakage \<equiv> \<forall>as s u t. s \<approx>chain as u\<approx> t \<longrightarrow> s \<lesssim>as,u,as\<lesssim> t"

lemma Nonleakage_implies_weak_Nonleakage: "Nonleakage \<Longrightarrow> weak_Nonleakage"
(*<*)
apply (unfold Nonleakage_def weak_Nonleakage_def)
apply (blast intro: gen_uwr_mono [OF _ sources_subset_chain])
done
(*>*)

constdefs
  weak_uni_Step_consistent_respect :: "bool"
 "weak_uni_Step_consistent_respect \<equiv> \<forall>a s s' us t. (\<exists>u. u\<in>us) \<longrightarrow> 
         (s, s') \<in> Step a \<longrightarrow> (\<forall>u\<in>us. s \<simeq>u\<simeq> t) \<longrightarrow> 
   (\<exists>t'. (t, t') \<in> Step a \<and> s' \<approx>us\<approx> t')"

lemma weak_uni_Step_consistent_respect_is_gen_uni_Step_consistent_respect_True:
  "weak_uni_Step_consistent_respect = gen_uni_Step_consistent_respect (\<lambda>w a. True)" 
(*<*)
apply (unfold weak_uni_Step_consistent_respect_def 
              gen_uni_Step_consistent_respect_def)
apply (auto)
apply  (blast intro: nest_uwrI)
apply (drule spec, drule spec, drule_tac x = "us" in spec)
apply (blast dest: nest_uwrD nest_uwr_implies_uwr
             intro: gen_uwrI)
done

lemma chain_unwinding_Step: (* unused *)
       "\<lbrakk>(s, s') \<in> Step a; s \<approx>chain (a # as) u\<approx> t; 
         weak_uni_Step_consistent_respect\<rbrakk> \<Longrightarrow> 
   \<exists>t'. (t, t') \<in> Step a \<and> s' \<approx>chain as u\<approx> t'"
apply (unfold chain_def)
apply (erule (1) gen_chain_unwinding_Step)
apply (simp add:
   weak_uni_Step_consistent_respect_is_gen_uni_Step_consistent_respect_True)
done
(*>*)

theorem weak_Nonleakage: 
  "\<lbrakk>weak_uni_Step_consistent_respect; output_consistent\<rbrakk> \<Longrightarrow> weak_Nonleakage"
(*<*)
apply (simp only:
       weak_uni_Step_consistent_respect_is_gen_uni_Step_consistent_respect_True)
apply (drule gen_Nonleakage)
apply (unfold gen_Nonleakage_def weak_Nonleakage_def chain_def)
apply (blast intro!: obs_POI)
done
(*>*)

subsubsection "transitive weak Nonleakage"

constdefs
  trans_weak_Nonleakage :: "bool" 
 "trans_weak_Nonleakage \<equiv> \<forall>s u t. s \<simeq>u\<simeq> t \<longrightarrow> (\<forall>as. s \<lesssim>as,u,as\<lesssim> t)"

lemma (in policy_trans) weak_Nonleakage_implies_trans_weak_Nonleakage:
  "weak_Nonleakage \<Longrightarrow> trans_weak_Nonleakage"
(*<*)
apply (unfold weak_Nonleakage_def trans_weak_Nonleakage_def)
apply (force intro: gen_uwr_mono [OF _ chain_subset_tsources])
done
(*>*)

theorem (in policy_trans) trans_weak_Nonleakage: 
"\<lbrakk>weak_uni_Step_consistent_respect; output_consistent\<rbrakk> \<Longrightarrow> trans_weak_Nonleakage"
(*<*)
by (blast intro: weak_Nonleakage weak_Nonleakage_implies_trans_weak_Nonleakage)

end
(*>*)
(*  Title:      NI/Noninfluence.thy
    Id:         $Id: Noninfluence.thy,v 1.6 2004/01/29 17:36:47 dvo Exp $
    Author:     David von Oheimb
    License:    (C) 2003 Siemens AG; any non-commercial use is granted

*)
header {* Noninfluence *}

(*<*)
theory Noninfluence imports Noninterference Nonleakage begin

(*>*)
subsection "the deterministic case"

constdefs
  noninfluence :: "bool" 
 "noninfluence \<equiv> \<forall>as u s t. s \<approx>sources as u\<approx> t \<longrightarrow> s \<simeq>as,u,ipurge u as\<simeq> t"

lemma noninfluence_implies_noninterference: "noninfluence \<Longrightarrow> noninterference"
(*<*)
apply (unfold noninfluence_def noninterference_def)
apply (blast intro: gen_uwr_s0)
done
(*>*)

theorem noninfluence:
  "\<lbrakk>weakly_step_consistent; local_respect; output_consistent\<rbrakk> \<Longrightarrow> noninfluence"
(*<*)
apply (drule (1) gen_noninterference_sources)
apply (unfold gen_noninterference_def noninfluence_def obs_equiv_def)
apply (blast dest: output_consistentD)
done
(*>*)

subsection "the nondeterministic case"

constdefs
  Noninfluence :: "bool" 
 "Noninfluence \<equiv> 
  \<forall>as bs u s t. s \<approx>sources as u\<approx> t \<longrightarrow> ipurge u as = ipurge u bs \<longrightarrow> s \<lesssim>as,u,bs\<lesssim> t"

lemma Noninfluence_implies_Noninterference: "Noninfluence \<Longrightarrow> Noninterference"
(*<*)
apply (unfold Noninfluence_def Noninterference_def)
apply (blast intro: gen_uwr_s0)
done
(*>*)

theorem Noninfluence:
  "\<lbrakk>uni_Step_consistent; uni_Local_respect; output_consistent\<rbrakk> \<Longrightarrow> Noninfluence"
(*<*)
apply (drule (1) gen_Noninterference_sources)
apply (unfold gen_Noninterference_def Noninfluence_def obs_PO_def)
apply (blast dest: output_consistentD)
done

end
(*>*)


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.