Theory Noninfluence

(*  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 = Noninterference + Nonleakage:

(*>*)
subsection "the deterministic case"

constdefs
  noninfluence :: "bool" 
 "noninfluence ≡ ∀as u s t. s ≈sources as u≈ t --> s ≅as,u,ipurge u as≅ t"

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

theorem noninfluence:
  "[|weakly_step_consistent; local_respect; output_consistent|] ==> 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 ≡ 
  ∀as bs u s t. s ≈sources as u≈ t --> ipurge u as = ipurge u bs --> s \<lesssim>as,u,bs\<lesssim> t"

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

theorem Noninfluence:
  "[|uni_Step_consistent; uni_Local_respect; output_consistent|] ==> Noninfluence"
(*<*)
apply (drule (1) gen_Noninterference_sources)
apply (unfold gen_Noninterference_def Noninfluence_def obs_PO_def)
apply (blast dest: output_consistentD)
done

end
(*>*)