(*  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
(*>*)