Theory FlowPolicies

theory FlowPolicies
imports Views
begin

(* 
  Flow policies
*)
record 'domain FlowPolicy_rec = 
  D :: "'domain set"
  v_rel :: "('domain × 'domain) set"
  n_rel :: "('domain × 'domain) set"
  c_rel :: "('domain × 'domain) set"
(*
  The three relations of a flow policy form a partition of DxD.
  Moreover, the relation v_rel is reflexive.
*)
definition FlowPolicy :: "'domain FlowPolicy_rec ⇒ bool"
where
"FlowPolicy fp ≡ 
   ((v_rel fp) ∪ (n_rel fp) ∪ (c_rel fp) = ((D fp) × (D fp)))
 ∧ (v_rel fp) ∩ (n_rel fp) = {}
 ∧ (v_rel fp) ∩ (c_rel fp) = {}
 ∧ (n_rel fp) ∩ (c_rel fp) = {} 
 ∧ (∀d ∈ (D fp). (d, d) ∈ (v_rel fp))"

(* 
  Domain assignments and the view of a domain 
*)
type_synonym ('e, 'domain) dom_type = "'e ⇀ 'domain"

(*
  A domain assignment should only assign domains to actual events.
*)
definition dom :: "('e, 'domain) dom_type ⇒ 'domain set ⇒ 'e set ⇒ bool"
where
"dom domas dset es ≡ 
(∀e. ∀d. ((domas e = Some d) ⟶ (e ∈ es ∧ d ∈ dset)))"

(*
  The combination of a domain assignment and a flow policy
  yields a view for each domain.
*)
definition view_dom :: "'domain FlowPolicy_rec ⇒ 'domain ⇒ ('e, 'domain) dom_type ⇒ 'e V_rec"
where
  "view_dom fp d domas ≡ 
   ⦇ V = {e. ∃d'. (domas e = Some d' ∧ (d', d) ∈ (v_rel fp))}, 
     N = {e. ∃d'. (domas e = Some d' ∧ (d', d) ∈ (n_rel fp))}, 
     C = {e. ∃d'. (domas e = Some d' ∧ (d', d) ∈ (c_rel fp))} ⦈"

end