Theory InformationFlowProperties

theory InformationFlowProperties
imports BasicSecurityPredicates
begin

(* Security Predicates are sets of basic security predicates *)
type_synonym 'e SP = "('e BSP) set"

(* structurally, information flow properties consist of a set of views 
 and a security predicate. *)
type_synonym 'e IFP_type = "('e V_rec set) × 'e SP"

(* side condition for information flow properties *)
definition IFP_valid :: "'e set ⇒ 'e IFP_type ⇒ bool"
where
"IFP_valid E ifp ≡  
  ∀𝒱 ∈ (fst ifp). isViewOn 𝒱 E  
                    ∧ (∀BSP ∈ (snd ifp). BSP_valid BSP)"

(* An information flow property is an instance of IFP_type that 
 satisfies IFP_valid. *)
definition IFPIsSatisfied :: "'e IFP_type ⇒ ('e list) set  ⇒ bool"
where 
"IFPIsSatisfied ifp Tr ≡ 
  ∀ 𝒱∈(fst ifp). ∀ BSP∈(snd ifp). BSP 𝒱 Tr"

end