Theory Analysis
section‹Properties on Policies›
theory
Analysis
imports
ParallelComposition
SeqComposition
begin
text ‹
In this theory, several standard policy properties are paraphrased in UPF terms.
›
subsection‹Basic Properties›
subsubsection‹A Policy Has no Gaps›
definition gap_free :: "('a ↦ 'b) ⇒ bool"
where "gap_free p = (dom p = UNIV)"
subsubsection‹Comparing Policies›
text ‹Policy p is more defined than q:›
definition more_defined :: "('a ↦ 'b) ⇒('a ↦ 'b) ⇒bool"
where "more_defined p q = (dom q ⊆ dom p)"
definition strictly_more_defined :: "('a ↦ 'b) ⇒('a ↦ 'b) ⇒bool"
where "strictly_more_defined p q = (dom q ⊂ dom p)"
lemma strictly_more_vs_more: "strictly_more_defined p q ⟹ more_defined p q"
unfolding more_defined_def strictly_more_defined_def
by auto
text‹Policy p is more permissive than q:›
definition more_permissive :: "('a ↦ 'b) ⇒ ('a ↦ 'b) ⇒ bool" (infixl "⊑⇩A" 60)
where " p ⊑⇩A q = (∀ x. (case q x of ⌊allow y⌋ ⇒ (∃ z. (p x = ⌊allow z⌋))
| ⌊deny y⌋ ⇒ True
| ⊥ ⇒ True))"
lemma more_permissive_refl : "p ⊑⇩A p "
unfolding more_permissive_def
by(auto split : option.split decision.split)
lemma more_permissive_trans : "p ⊑⇩A p' ⟹ p' ⊑⇩A p'' ⟹ p ⊑⇩A p''"
unfolding more_permissive_def
apply(auto split : option.split decision.split)
subgoal for x y
apply(erule_tac x = x and
P = "λx. case p'' x of ⊥ ⇒ True
| ⌊allow y⌋ ⇒ ∃z. p' x = ⌊allow z⌋
| ⌊deny y⌋ ⇒ True" in allE)
apply(simp, elim exE)
by(erule_tac x = x in allE, simp)
done
text‹Policy p is more rejective than q:›
definition more_rejective :: "('a ↦ 'b) ⇒ ('a ↦ 'b) ⇒ bool" (infixl "⊑⇩D" 60)
where " p ⊑⇩D q = (∀ x. (case q x of ⌊deny y⌋ ⇒ (∃ z. (p x = ⌊deny z⌋))
| ⌊allow y⌋ ⇒ True
| ⊥ ⇒ True))"
lemma more_rejective_trans : "p ⊑⇩D p' ⟹ p' ⊑⇩D p'' ⟹ p ⊑⇩D p''"
unfolding more_rejective_def
apply(auto split : option.split decision.split)
subgoal for x y
apply(erule_tac x = x and
P = "λx. case p'' x of ⊥ ⇒ True
| ⌊allow y⌋ ⇒ True
| ⌊deny y⌋ ⇒ ∃z. p' x = ⌊deny z⌋" in allE)
apply(simp, elim exE)
by(erule_tac x = x in allE, simp)
done
lemma more_rejective_refl : "p ⊑⇩D p "
unfolding more_rejective_def
by(auto split : option.split decision.split)
lemma "A⇩f f ⊑⇩A p"
unfolding more_permissive_def allow_all_fun_def allow_pfun_def
by(auto split: option.split decision.split)
lemma "A⇩I ⊑⇩A p"
unfolding more_permissive_def allow_all_fun_def allow_pfun_def allow_all_id_def
by(auto split: option.split decision.split)
subsection‹Combined Data-Policy Refinement›
definition policy_refinement ::
"('a ↦ 'b) ⇒ ('a' ⇒ 'a) ⇒('b' ⇒ 'b) ⇒ ('a' ↦ 'b') ⇒ bool"
("_ ⊑⇘_⇙⇩,⇘_⇙ _" [50,50,50,50]50)
where "p ⊑⇘abs⇩a⇙⇩,⇘abs⇩b⇙ q ≡
(∀ a. case p a of
⊥ ⇒ True
| ⌊allow y⌋ ⇒ (∀ a'∈{x. abs⇩a x=a}.
∃ b'. q a' = ⌊allow b'⌋
∧ abs⇩b b' = y)
| ⌊deny y⌋ ⇒ (∀ a'∈{x. abs⇩a x=a}.
∃ b'. q a' = ⌊deny b'⌋
∧ abs⇩b b' = y))"
theorem polref_refl: "p ⊑⇘id⇙⇩,⇘id⇙ p"
unfolding policy_refinement_def
by(auto split: option.split decision.split)
theorem polref_trans:
assumes A: "p ⊑⇘f⇙⇩,⇘g⇙ p'"
and B: "p' ⊑⇘f'⇙⇩,⇘g'⇙ p''"
shows "p ⊑⇘f o f'⇙⇩,⇘g o g'⇙ p''"
apply(insert A B)
unfolding policy_refinement_def
apply(auto split: option.split decision.split simp: o_def)[1]
subgoal for a a'
apply(erule_tac x="f (f' a')" in allE, simp)[1]
apply(erule_tac x="f' a'" in allE, auto)[1]
apply(erule_tac x=" (f' a')" in allE, auto)[1]
done
subgoal for a a'
apply(erule_tac x="f (f' a')" in allE, simp)[1]
apply(erule_tac x="f' a'" in allE, auto)[1]
apply(erule_tac x=" (f' a')" in allE, auto)[1]
done
done
subsection ‹Equivalence of Policies›
subsubsection‹Equivalence over domain D›
definition p_eq_dom :: "('a ↦ 'b) ⇒ 'a set ⇒ ('a ↦ 'b) ⇒bool" ("_ ≈⇘_⇙ _" [60,60,60]60)
where "p ≈⇘D⇙ q = (∀x∈D. p x = q x)"
text‹p and q have no conflicts›
definition no_conflicts :: "('a ↦ 'b) ⇒('a ↦ 'b) ⇒bool" where
"no_conflicts p q = (dom p = dom q ∧ (∀x∈(dom p).
(case p x of ⌊allow y⌋ ⇒ (∃z. q x = ⌊allow z⌋)
| ⌊deny y⌋ ⇒ (∃z. q x = ⌊deny z⌋))))"
lemma policy_eq:
assumes p_over_qA: "p ⊑⇩A q "
and q_over_pA: "q ⊑⇩A p"
and p_over_qD: "q ⊑⇩D p"
and q_over_pD: "p ⊑⇩D q"
and dom_eq: "dom p = dom q"
shows "no_conflicts p q"
apply (insert p_over_qA q_over_pA p_over_qD q_over_pD dom_eq)
apply (simp add: no_conflicts_def more_permissive_def more_rejective_def
split: option.splits decision.splits)
apply (safe)
apply (metis domI domIff dom_eq)
apply (metis)+
done
subsubsection‹Miscellaneous›
lemma dom_inter: "⟦dom p ∩ dom q = {}; p x = ⌊y⌋⟧ ⟹ q x = ⊥"
by (auto)
lemma dom_eq: "dom p ∩ dom q = {} ⟹ p ⨁⇩A q = p ⨁⇩D q"
unfolding override_A_def override_D_def
by (rule ext, auto simp: dom_def split: prod.splits option.splits decision.splits )
lemma dom_split_alt_def : "(f, g) Δ p = (dom(p ▹ Allow) ◃ (A⇩f f)) ⨁ (dom(p ▹ Deny) ◃ (D⇩f g))"
apply (rule ext)
apply (simp add: dom_split2_def Allow_def Deny_def dom_restrict_def
deny_all_fun_def allow_all_fun_def map_add_def)
apply (simp split: option.splits decision.splits)
apply (auto simp: map_add_def o_def deny_pfun_def ran_restrict_def image_def)
done
end