Theory Nonleakage

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

(*>*)
subsection "the deterministic case"

constdefs --{* generic nonleakage *}
  gen_nonleakage :: "sourcef => bool" 
 "gen_nonleakage sf ≡ ∀as s u t. s ≈sf as u≈ t --> run as s ∼u∼ run as t"
(*<*)
lemma gen_nonleakage: 
  "gen_weak_step_consistent_respect P ==> 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 ≡ ∀as s u t. s ≈sources as u≈ t --> s ≅as,u,as≅ t"

theorem nonleakage:
   "[|weakly_step_consistent; step_respect; output_consistent|] ==> 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 ≡ ∀as s u t. s ≈chain as u≈ t --> s ≅as,u,as≅ t"

lemma nonleakage_implies_weak_nonleakage: "nonleakage ==> 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 ≡ ∀s u t. s \<simeq>u\<simeq> t --> (∀a. step a s ∼u∼ step a t)"

lemma weak_step_consistent_respect_is_gen_weak_step_consistent_respect_True:
 "weak_step_consistent_respect = gen_weak_step_consistent_respect (λ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 *)
 "[|s ≈chain (a # as) u≈ t; weak_step_consistent_respect|] ==> 
   step a s ≈chain as u≈ 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: 
  "[|weak_step_consistent_respect; output_consistent|] ==> 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 ≡ ∀s u t. s \<simeq>u\<simeq> t --> (∀as. s ≅as,u,as≅ t)"

lemma (in policy_trans) weak_nonleakage_implies_trans_weak_nonleakage:
  "weak_nonleakage ==> 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 *)
 "[|weak_step_consistent_respect; s \<simeq>u\<simeq> t|] ==> 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: 
  "[|weak_step_consistent_respect; output_consistent|] ==> 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 ≡ ∀u as s s' t.
        (s, s') ∈ Run as --> s ≈sf as u≈ t --> 
  (∃t'. (t, t') ∈ Run as ∧ s' ∼u∼ t')"

lemma gen_Nonleakage:
 "gen_uni_Step_consistent_respect P ==> 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 ≡ ∀as s u t. s ≈sources as u≈ t --> s \<lesssim>as,u,as\<lesssim> t"

theorem Nonleakage:
 "[|uni_Step_consistent; uni_Step_respect; output_consistent|] ==> 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 ≡ ∀as s u t. s ≈chain as u≈ t --> s \<lesssim>as,u,as\<lesssim> t"

lemma Nonleakage_implies_weak_Nonleakage: "Nonleakage ==> 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 ≡ ∀a s s' us t. (∃u. u∈us) --> 
         (s, s') ∈ Step a --> (∀u∈us. s \<simeq>u\<simeq> t) --> 
   (∃t'. (t, t') ∈ Step a ∧ s' ≈us≈ t')"

lemma weak_uni_Step_consistent_respect_is_gen_uni_Step_consistent_respect_True:
  "weak_uni_Step_consistent_respect = gen_uni_Step_consistent_respect (λ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 *)
       "[|(s, s') ∈ Step a; s ≈chain (a # as) u≈ t; 
         weak_uni_Step_consistent_respect|] ==> 
   ∃t'. (t, t') ∈ Step a ∧ s' ≈chain as u≈ 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: 
  "[|weak_uni_Step_consistent_respect; output_consistent|] ==> 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 ≡ ∀s u t. s \<simeq>u\<simeq> t --> (∀as. s \<lesssim>as,u,as\<lesssim> t)"

lemma (in policy_trans) weak_Nonleakage_implies_trans_weak_Nonleakage:
  "weak_Nonleakage ==> 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: 
"[|weak_uni_Step_consistent_respect; output_consistent|] ==> trans_weak_Nonleakage"
(*<*)
by (blast intro: weak_Nonleakage weak_Nonleakage_implies_trans_weak_Nonleakage)

end
(*>*)