Theory Noninterference

(*  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 = Generics:

(*>*)
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 ∈ sf (a#as) u then [a] else []) 
                                 @ gen_purge sf u as"

constdefs --{* also for transitive policies *}
  ipurge :: "domain => action list => action list" 
 "ipurge ≡ 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 ∈ sources (ipurge u as) u ==> v ∈ 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 ∈ sources (a#as) u
                          then [a] else []) @ ipurge u as"
by (simp add: ipurge_def)

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

lemma Cons_ipurge_sourcesD: 
 "∀bs. ipurge u as = ipurge u bs --> sources as u = sources bs u ==>
  a # ipurge u as = ipurge u bs --> 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]: 
 "∀bs. ipurge u as = ipurge u bs --> 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 ==> 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 ≡ 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 (λ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 ≡ ∀as u. s0 ≅as,u,ipurge u as≅ s0"

constdefs --{* common structure of @{term "noninterference"} and @{text "noninfluence"} *}
  gen_noninterference :: "sourcef => bool"
 "gen_noninterference sf ≡  
  ∀u as s t. s ≈sf as u≈ t --> run as s ∼u∼ run (ipurge u as) t"

lemma output_consistent_and_gen_noninterference_implies_noninterference:
  "output_consistent ==> gen_noninterference sf ==> 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 ≡ ∀a u s t. dom a \<notleadsto> u --> s ∼u∼ t --> step a s ∼u∼ t"

  local_respect_right :: "bool"
 "local_respect_right ≡ ∀a u s t. dom a \<notleadsto> u --> s ∼u∼ t --> s ∼u∼ step a t"

  local_respect :: "bool"
 "local_respect ≡ local_respect_left ∧ local_respect_right"
(*<*)
lemma local_respect_leftD: 
  "[|local_respect_left; dom a \<notleadsto> u; s ∼u∼ t|] ==> step a s ∼u∼ t"
by (unfold local_respect_left_def, blast)

lemma local_respect_rightD: 
  "[|local_respect_right; dom a \<notleadsto> u; s ∼u∼ t|] ==> s ∼u∼ step a t"
by (unfold local_respect_right_def, blast)

lemma local_respectD: 
  "local_respect ==> local_respect_left ∧ local_respect_right"
by (unfold local_respect_def, blast)

(*>*)

lemma (in uwr_refl) local_respect_classical: 
  "local_respect ==> ∀a u s. dom a \<notleadsto> u --> s ∼u∼ step a s"
(*<*)
by (blast dest: local_respectD local_respect_rightD intro: uwr_refl)
(*>*)
lemma (in uwr_trans) classical_local_respect: 
  "∀s u t. s ∼u∼ t --> t ∼u∼ s ==>
   ∀a u s. dom a \<notleadsto> u --> s ∼u∼ step a s ==> 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 ==> 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 ==> local_respect ==> 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 *}
"[|weakly_step_consistent; local_respect; output_consistent|] ==> 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 ≡ ∀a u s t. dom a \<leadsto> u --> s ∼u∼ t --> step a s ∼u∼ step a t"

theorem simple_noninterference: --{* Rushby's Theorem 1 *}
 "step_consistent ==> local_respect ==> 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 ==> 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 ≡ ∀u as s t bs. s ≈sf as u≈ t --> 
   gen_purge sf u as = gen_purge sf u bs --> run as s ∼u∼ run bs t"

lemma gen_purge_nilD [rule_format]: "local_respect_right ==> 
  [] = gen_purge sf u bs --> (∀t. s ∼u∼ t --> s ∼u∼ 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 ==> a # as = ipurge u bs  -->
  (∃bsa bsc. bs = bsa @ a # bsc ∧ (∀t. s ≈sources (a#as) u≈ t --> s ≈sources (a#as) u≈ run bsa t) ∧ 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 ==> local_respect ==> strong_noninterference"
apply (subgoal_tac "∀u as bs s t. ipurge u as = ipurge u bs --> 
                    s ≈sources as u≈ t --> run as s ∼u∼ 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 ≡ ∀as u bs. ipurge u as = ipurge u bs --> s0 ≅as,u,bs≅ s0"

lemma strong_noninterference_implies_noninterference:
 "strong_noninterference ==> 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 ==> local_respect ==> 
∀u as s t. s ≈sources as u≈ t --> run (ipurge u as) s ∼u∼ 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:
"[|weakly_step_consistent; local_respect; output_consistent|] ==> 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 ==> gen_noninterference sources ==> 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 ==> 
  [] = ipurge u bs --> (∀t. s ∼u∼ t --> s ∼u∼ 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 ==> a # as = ipurge u bs --> 
   (∃bsa bsc. bs = bsa @ a # bsc ∧ as = ipurge u bsc ∧ 
   (∀t. s ∼u∼ t --> s ∼u∼ 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 ==> a # as = ipurge u bs  -->
  (∃bsa bsc. bs = bsa @ a # bsc ∧ as = ipurge u bsc ∧ 
(∀t. s ≈sources (a#as) u≈ t --> s ≈sources (a#as) u≈ 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:
 "[|weakly_step_consistent; local_respect; output_consistent|] ==> strong_noninterference"
(*<*)
apply (subgoal_tac "∀u as bs s t. ipurge u as = ipurge u bs --> 
                    s ≈sources as u≈ t --> run as s ∼u∼ 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 ∼u∼ t ≡ ∀n∈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 ≡ {value2output (contents s n) |n. n ∈ 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 ≡ output_consistent"

  RMA2 :: "bool" --{* new premises @{term "dom a \<leadsto> u"}, @{term "s ∼u∼ t"}, and @{term "n ∈ observe u"} *}
 "RMA2 ≡ ∀a u s t n. s ∼dom a∼ t --> dom a \<leadsto> u --> s ∼u∼ t --> n ∈ observe u --> 
                      (contents (step a s) n ≠ contents s n ∨ 
                       contents (step a t) n ≠ contents t n) --> 
                       contents (step a s) n = contents (step a t) n"

  RMA3 :: "bool"
 "RMA3 ≡ ∀a s n. contents (step a s) n ≠ contents s n --> n ∈ alter (dom a)"

  AC_policy_consistent :: "bool"
 "AC_policy_consistent ≡ ∀u v. alter u ∩ observe v ≠ {} --> u \<leadsto> v"
(*<*)
lemma AC_policy_consistent_revD: 
  "AC_policy_consistent ==> n ∈ observe v ==> u \<notleadsto> v ==> n ∉ alter u"
by (unfold AC_policy_consistent_def, blast)

lemma AC_unwinding_weakly_step_consistentI:
  "(!!a u s t n. [|dom a \<leadsto> u; s ∼dom a∼ t; s ∼u∼ t; n ∈ observe u; 
                  contents (step a s) n ≠ contents s n ∨ 
                  contents (step a t) n ≠ contents t n|] ==> 
                  contents (step a s) n = contents (step a t) n)
 ==> weakly_step_consistent"
apply (clarsimp simp add: weakly_step_consistent_def uwr_def)
apply (case_tac "contents (step a s) n = contents s n ∧ 
                 contents (step a t) n = contents t n")
apply  (auto)
done
(*>*)

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

lemma RMA3_AC_policy_consistent_implies_local_respect: 
  "RMA3 ==> AC_policy_consistent ==> 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: 
  "[|RMA1; RMA2; RMA3; AC_policy_consistent|] ==> 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 ≡ ∀as u bs. ipurge u as = ipurge u bs --> s0 \<lesssim>as,u,bs\<lesssim> s0"

  gen_Noninterference :: "sourcef => bool"
 "gen_Noninterference sf ≡ ∀as bs s s' u t. ipurge u as = ipurge u bs --> 
         (s, s') ∈ Run as --> s ≈sf as u≈ t --> 
   (∃t'. (t, t') ∈ Run bs ∧ s' ∼u∼ t')"
lemma 
  output_consistent_and_gen_Noninterference_implies_Noninterference:
  "output_consistent ==> gen_Noninterference sf ==> 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 ≡ ∀a u s t s'. dom a \<notleadsto> u --> 
  s ∼u∼ t --> (s, s') ∈ Step a --> s' ∼u∼ t"

  Local_respect_right :: "bool"
 "Local_respect_right ≡ ∀a u s t. dom a \<notleadsto> u --> 
  s ∼u∼ t --> (∃t'. (t, t') ∈ Step a ∧ s ∼u∼ t')"
(*<*)
lemma Local_respect_leftD: 
 "[|Local_respect_left; dom a \<notleadsto> u; (s, s') ∈ Step a; s ∼u∼ t|] ==> s' ∼u∼ t" 
by (unfold Local_respect_left_def, blast)

lemma Local_respect_rightD: 
  "[|Local_respect_right; dom a \<notleadsto> u; s ∼u∼ t|] ==> ∃t'. (t, t') ∈ Step a ∧ s ∼u∼ t'"
by (unfold Local_respect_right_def, blast)
(*>*)

lemma Local_respect_implies_Step_respect:
 "[|Local_respect_left; Local_respect_right|] ==> 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 ==> 
   ∀a u s t s'. dom a \<notleadsto> u --> (s, s') ∈ Step a --> s' ∼u∼ s"
(*<*)
by (blast dest: Local_respect_leftD intro: uwr_refl)
(*>*)

lemma (in uwr_refl) Local_respect_right_Mantel: 
  "Local_respect_right ==> 
   ∀a u s t. dom a \<notleadsto> u --> (∃t'. (t, t') ∈ Step a ∧ t ∼u∼ t')"
(*<*)
by (blast dest: Local_respect_rightD intro: uwr_refl)
(*>*)

lemma (in uwr_trans) Mantel_Local_respect_left: 
  "∀a u s t s'. dom a \<notleadsto> u --> (s, s') ∈ Step a --> s' ∼u∼ s ==> 
   Local_respect_left"
(*<*)
by (unfold Local_respect_left_def, blast dest: uwr_trans)
(*>*)

lemma (in uwr_trans) Mantel_Local_respect_right: 
  "∀a u s t. dom a \<notleadsto> u --> (∃t'. (t, t') ∈ Step a ∧ t ∼u∼ t') ==> 
   Local_respect_right"
(*<*)
by (unfold Local_respect_right_def, blast dest: uwr_trans)
(*>*)

lemma ipurge_NilD [rule_format]: "Local_respect_right ==> 
  [] = ipurge u bs --> (∀t. s ∼u∼ t --> (∃t'. (t, t') ∈ Run bs ∧ s ∼u∼ 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 ==> 
  a # as = ipurge u bs --> (∃bsa bsc. bs = bsa @ a # bsc ∧ as = ipurge u bsc ∧
  (∀t. s ∼u∼ t --> (∃ta. (t, ta) ∈ Run bsa ∧ s ∼u∼ 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 ==> Local_respect_left ==> Local_respect_right ==> 
  gen_Noninterference singleton"
apply (subgoal_tac "∀u as s' s bs t. (s, s')∈Run as --> 
                    ipurge u as = ipurge u bs --> s ∼u∼ t --> 
                  (∃t'. (t, t')∈Run bs ∧ s' ∼u∼ 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 ∼u∼ t")
apply  (drule (3) simple_unwinding_Step, blast)
apply (blast dest: rev_sources_direct Local_respect_leftD)
done
(*>*)

theorem simple_Noninterference: 
 "Step_consistent ==> Local_respect_left ==> Local_respect_right ==> 
  output_consistent ==> 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 ≡ ∀a us s t. ¬(∃u∈us. dom a \<leadsto> u) --> (∃u. u∈us) -->
  s ≈us≈ t --> (∃t'. (t, t') ∈ Step a ∧ s ≈us≈ t')"
 
  uni_Local_respect :: "bool"
 "uni_Local_respect ≡ Local_respect_left ∧ uni_Local_respect_right"

lemma uni_Local_respect_leftD: "[|Local_respect_left; 
  (s, s') ∈ Step a; ¬(∃u∈us. dom a \<leadsto> u); s ≈us≈ t|] ==> s' ≈us≈ t" 
(*<*)
apply (rule gen_uwrI)
apply (drule (1) gen_uwrD)
apply (blast dest: Local_respect_leftD)
done

lemma uni_Local_respect_rightD: 
  "[|uni_Local_respect_right; ¬(∃u∈us. dom a \<leadsto> u); u∈us; s ≈us≈ t|] ==> 
    ∃t'. (t, t') ∈ Step a ∧ s ≈us≈ t'"
by (unfold uni_Local_respect_right_def, blast)

lemma uni_Local_respectD: 
  "uni_Local_respect ==> Local_respect_left ∧ uni_Local_respect_right"
by (unfold uni_Local_respect_def, blast)
(*>*)

lemma uni_Local_respect_right_implies_Local_respect_right: 
  "uni_Local_respect_right ==> 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 ==> 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 ==> 
  a # as = ipurge u bs --> (∃bsa bsc. bs = bsa @ a # bsc ∧ as = ipurge u bsc ∧ 
  (∀t. s ≈sources (a#as) u≈ t --> (∃ta. (t, ta) ∈ Run bsa ∧ s ≈sources (a#as) u≈ 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 ==> uni_Local_respect ==> gen_Noninterference sources"
(*<*)
apply (subgoal_tac "∀u as s' s bs t. (s, s')∈Run as --> 
                    ipurge u as = ipurge u bs --> s ≈sources as u≈ t --> 
                  (∃t'. (t, t')∈Run bs ∧ s' ∼u∼ 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 ≈sources (a # list) u≈ 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 ==> 
 uni_Local_respect ==> output_consistent ==> Noninterference"
(*<*)
by (blast intro: gen_Noninterference_sources 
    output_consistent_and_gen_Noninterference_implies_Noninterference)

end
(*>*)