afp-mirror
/
UPF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Import of UPF release afp-UPF-2014-11-30 (Isabelle 2014).

This commit is contained in:
Achim D. Brucker 2016-08-10 10:11:02 +01:00
parent 1fb8d8ad7d
commit 38468e46bb
19 changed files with 4356 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

210
Analysis.thy Normal file
View File

@ -0,0 +1,210 @@
(*****************************************************************************
* HOL-TestGen --- theorem-prover based test case generation
* http://www.brucker.ch/projects/hol-testgen/
*
* UPF
* This file is part of HOL-TestGen.
*
* Copyright (c) 2005-2012 ETH Zurich, Switzerland
* 2008-2014 Achim D. Brucker, Germany
* 2009-2014 Université Paris-Sud, France
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* * Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above
* copyright notice, this list of conditions and the following
* disclaimer in the documentation and/or other materials provided
* with the distribution.
*
* * Neither the name of the copyright holders nor the names of its
* contributors may be used to endorse or promote products derived
* from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
******************************************************************************)
(* $Id: Analysis.thy 10953 2014-11-24 11:23:40Z wolff $ *)
header{* Properties on Policies *}
theory
Analysis
imports
ParallelComposition
SeqComposition
begin
text {*
In this theory, several standard policy properties are paraphrased in UPF terms.
*}
section{* Basic Properties *}
subsection{* A Policy Has no Gaps *}
definition gap_free :: "('a \<mapsto> 'b) \<Rightarrow> bool"
where "gap_free p = (dom p = UNIV)"
subsection{* Comparing Policies *}
text {* Policy p is more defined than q: *}
definition more_defined :: "('a \<mapsto> 'b) \<Rightarrow>('a \<mapsto> 'b) \<Rightarrow>bool"
where "more_defined p q = (dom q \<subseteq> dom p)"
definition strictly_more_defined :: "('a \<mapsto> 'b) \<Rightarrow>('a \<mapsto> 'b) \<Rightarrow>bool"
where "strictly_more_defined p q = (dom q \<subset> dom p)"
lemma strictly_more_vs_more: "strictly_more_defined p q \<Longrightarrow> 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 \<mapsto> 'b) \<Rightarrow> ('a \<mapsto> 'b) \<Rightarrow> bool" (infixl "\<sqsubseteq>\<^sub>A" 60)
where " p \<sqsubseteq>\<^sub>A q = (\<forall> x. (case q x of \<lfloor>allow y\<rfloor> \<Rightarrow> (\<exists> z. (p x = \<lfloor>allow z\<rfloor>))
| \<lfloor>deny y\<rfloor> \<Rightarrow> True
| \<bottom> \<Rightarrow> True))"
lemma more_permissive_refl : "p \<sqsubseteq>\<^sub>A p "
unfolding more_permissive_def
by(auto split : option.split decision.split)
lemma more_permissive_trans : "p \<sqsubseteq>\<^sub>A p' \<Longrightarrow> p' \<sqsubseteq>\<^sub>A p'' \<Longrightarrow> p \<sqsubseteq>\<^sub>A p''"
unfolding more_permissive_def
apply(auto split : option.split decision.split)
apply(erule_tac x = x and
P = "\<lambda>x. case p'' x of \<bottom> \<Rightarrow> True
| \<lfloor>allow y\<rfloor> \<Rightarrow> \<exists>z. p' x = \<lfloor>allow z\<rfloor>
| \<lfloor>deny y\<rfloor> \<Rightarrow> True" in allE)
apply(simp, elim exE)
by(erule_tac x = x in allE, simp)
text{* Policy p is more rejective than q: *}
definition more_rejective :: "('a \<mapsto> 'b) \<Rightarrow> ('a \<mapsto> 'b) \<Rightarrow> bool" (infixl "\<sqsubseteq>\<^sub>D" 60)
where " p \<sqsubseteq>\<^sub>D q = (\<forall> x. (case q x of \<lfloor>deny y\<rfloor> \<Rightarrow> (\<exists> z. (p x = \<lfloor>deny z\<rfloor>))
| \<lfloor>allow y\<rfloor> \<Rightarrow> True
| \<bottom> \<Rightarrow> True))"
lemma more_rejective_trans : "p \<sqsubseteq>\<^sub>D p' \<Longrightarrow> p' \<sqsubseteq>\<^sub>D p'' \<Longrightarrow> p \<sqsubseteq>\<^sub>D p''"
unfolding more_rejective_def
apply(auto split : option.split decision.split)
apply(erule_tac x = x and
P = "\<lambda>x. case p'' x of \<bottom> \<Rightarrow> True
| \<lfloor>allow y\<rfloor> \<Rightarrow> True
| \<lfloor>deny y\<rfloor> \<Rightarrow> \<exists>z. p' x = \<lfloor>deny z\<rfloor>" in allE)
apply(simp, elim exE)
by(erule_tac x = x in allE, simp)
lemma more_rejective_refl : "p \<sqsubseteq>\<^sub>D p "
unfolding more_rejective_def
by(auto split : option.split decision.split)
lemma "A\<^sub>f f \<sqsubseteq>\<^sub>A p"
unfolding more_permissive_def allow_all_fun_def allow_pfun_def
by(auto split: option.split decision.split)
lemma "A\<^sub>I \<sqsubseteq>\<^sub>A p"
unfolding more_permissive_def allow_all_fun_def allow_pfun_def allow_all_id_def
by(auto split: option.split decision.split)
section{* Combined Data-Policy Refinement *}
definition policy_refinement ::
"('a \<mapsto> 'b) \<Rightarrow> ('a' \<Rightarrow> 'a) \<Rightarrow>('b' \<Rightarrow> 'b) \<Rightarrow> ('a' \<mapsto> 'b') \<Rightarrow> bool"
("_ \<sqsubseteq>\<^bsub>_\<^esub>\<^sub>,\<^bsub>_\<^esub> _" [50,50,50,50]50)
where "p \<sqsubseteq>\<^bsub>abs\<^sub>a\<^esub>\<^sub>,\<^bsub>abs\<^sub>b\<^esub> q \<equiv>
(\<forall> a. case p a of
\<bottom> \<Rightarrow> True
| \<lfloor>allow y\<rfloor> \<Rightarrow> (\<forall> a'\<in>{x. abs\<^sub>a x=a}.
\<exists> b'. q a' = \<lfloor>allow b'\<rfloor>
\<and> abs\<^sub>b b' = y)
| \<lfloor>deny y\<rfloor> \<Rightarrow> (\<forall> a'\<in>{x. abs\<^sub>a x=a}.
\<exists> b'. q a' = \<lfloor>deny b'\<rfloor>
\<and> abs\<^sub>b b' = y))"
theorem polref_refl: "p \<sqsubseteq>\<^bsub>id\<^esub>\<^sub>,\<^bsub>id\<^esub> p"
unfolding policy_refinement_def
by(auto split: option.split decision.split)
theorem polref_trans:
assumes A: "p \<sqsubseteq>\<^bsub>f\<^esub>\<^sub>,\<^bsub>g\<^esub> p'"
and B: "p' \<sqsubseteq>\<^bsub>f'\<^esub>\<^sub>,\<^bsub>g'\<^esub> p''"
shows "p \<sqsubseteq>\<^bsub>f o f'\<^esub>\<^sub>,\<^bsub>g o g'\<^esub> p''"
apply(insert A B)
unfolding policy_refinement_def
apply(auto split: option.split decision.split simp: o_def)
apply(erule_tac x="f (f' a')" in allE, simp)
apply(erule_tac x="f' a'" in allE, auto)
apply(erule_tac x=" (f' a')" in allE, auto)
apply(erule_tac x="f (f' a')" in allE, simp)
apply(erule_tac x="f' a'" in allE, auto)
apply(erule_tac x=" (f' a')" in allE, auto)
done
section {* Equivalence of Policies *}
subsubsection{* Equivalence over domain D *}
definition p_eq_dom :: "('a \<mapsto> 'b) \<Rightarrow> 'a set \<Rightarrow> ('a \<mapsto> 'b) \<Rightarrow>bool" ("_ \<approx>\<^bsub>_\<^esub> _" [60,60,60]60)
where "p \<approx>\<^bsub>D\<^esub> q = (\<forall>x\<in>D. p x = q x)"
text{* p and q have no conflicts *}
definition no_conflicts :: "('a \<mapsto> 'b) \<Rightarrow>('a \<mapsto> 'b) \<Rightarrow>bool" where
"no_conflicts p q = (dom p = dom q \<and> (\<forall>x\<in>(dom p).
(case p x of \<lfloor>allow y\<rfloor> \<Rightarrow> (\<exists>z. q x = \<lfloor>allow z\<rfloor>)
| \<lfloor>deny y\<rfloor> \<Rightarrow> (\<exists>z. q x = \<lfloor>deny z\<rfloor>))))"
lemma policy_eq:
assumes p_over_qA: "p \<sqsubseteq>\<^sub>A q "
and q_over_pA: "q \<sqsubseteq>\<^sub>A p"
and p_over_qD: "q \<sqsubseteq>\<^sub>D p"
and q_over_pD: "p \<sqsubseteq>\<^sub>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
subsection{* Miscellaneous *}
lemma dom_inter: "\<lbrakk>dom p \<inter> dom q = {}; p x = \<lfloor>y\<rfloor>\<rbrakk> \<Longrightarrow> q x = \<bottom>"
by (auto)
lemma dom_eq: "dom p \<inter> dom q = {} \<Longrightarrow> p \<Oplus>\<^sub>A q = p \<Oplus>\<^sub>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) \<Delta> p = (dom(p \<triangleright> Allow) \<triangleleft> (A\<^sub>f f)) \<Oplus> (dom(p \<triangleright> Deny) \<triangleleft> (D\<^sub>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

338
ElementaryPolicies.thy Normal file
View File

@ -0,0 +1,338 @@
(*****************************************************************************
* HOL-TestGen --- theorem-prover based test case generation
* http://www.brucker.ch/projects/hol-testgen/
*
* UPF
* This file is part of HOL-TestGen.
*
* Copyright (c) 2005-2012 ETH Zurich, Switzerland
* 2008-2014 Achim D. Brucker, Germany
* 2009-2014 Université Paris-Sud, France
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* * Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above
* copyright notice, this list of conditions and the following
* disclaimer in the documentation and/or other materials provided
* with the distribution.
*
* * Neither the name of the copyright holders nor the names of its
* contributors may be used to endorse or promote products derived
* from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
******************************************************************************)
(* $Id: ElementaryPolicies.thy 10945 2014-11-21 12:50:43Z wolff $ *)
header{* Elementary Policies *}
theory
ElementaryPolicies
imports
UPFCore
begin
text{*
In this theory, we introduce the elementary policies of UPF that build the basis
for more complex policies. These complex policies, respectively, embedding of
well-known access control or security models, are build by composing the elementary
policies defined in this theory.
*}
section{* The Core Policy Combinators: Allow and Deny Everything *}
definition
deny_pfun :: "('\<alpha> \<rightharpoonup>'\<beta>) \<Rightarrow> ('\<alpha> \<mapsto> '\<beta>)" ("AllD")
where
"deny_pfun pf \<equiv> (\<lambda> x. case pf x of
\<lfloor>y\<rfloor> \<Rightarrow> \<lfloor>deny (y)\<rfloor>
|\<bottom> \<Rightarrow> \<bottom>)"
definition
allow_pfun :: "('\<alpha> \<rightharpoonup>'\<beta>) \<Rightarrow> ('\<alpha> \<mapsto> '\<beta>)" ( "AllA")
where
"allow_pfun pf \<equiv> (\<lambda> x. case pf x of
\<lfloor>y\<rfloor> \<Rightarrow> \<lfloor>allow (y)\<rfloor>
|\<bottom> \<Rightarrow> \<bottom>)"
syntax (xsymbols)
"_allow_pfun" :: "('\<alpha> \<rightharpoonup>'\<beta>) \<Rightarrow> ('\<alpha> \<mapsto> '\<beta>)" ("A\<^sub>p")
translations
"A\<^sub>p f" \<rightleftharpoons> "AllA f"
syntax (xsymbols)
"_deny_pfun" :: "('\<alpha> \<rightharpoonup>'\<beta>) \<Rightarrow> ('\<alpha> \<mapsto> '\<beta>)" ("D\<^sub>p")
translations
"D\<^sub>p f" \<rightleftharpoons> "AllD f"
notation (xsymbols)
"deny_pfun" (binder "\<forall>D" 10) and
"allow_pfun" (binder "\<forall>A" 10)
lemma AllD_norm[simp]: "deny_pfun (id o (\<lambda>x. \<lfloor>x\<rfloor>)) = (\<forall>Dx. \<lfloor>x\<rfloor>)"
by(simp add:id_def comp_def)
lemma AllD_norm2[simp]: "deny_pfun (Some o id) = (\<forall>Dx. \<lfloor>x\<rfloor>)"
by(simp add:id_def comp_def)
lemma AllA_norm[simp]: "allow_pfun (id o Some) = (\<forall>Ax. \<lfloor>x\<rfloor>)"
by(simp add:id_def comp_def)
lemma AllA_norm2[simp]: "allow_pfun (Some o id) = (\<forall>Ax. \<lfloor>x\<rfloor>)"
by(simp add:id_def comp_def)
lemma AllA_apply[simp]: "(\<forall>Ax. Some (P x)) x = \<lfloor>allow (P x)\<rfloor>"
by(simp add:allow_pfun_def)
lemma AllD_apply[simp]: "(\<forall>Dx. Some (P x)) x = \<lfloor>deny (P x)\<rfloor>"
by(simp add:deny_pfun_def)
lemma neq_Allow_Deny: "pf \<noteq> \<emptyset> \<Longrightarrow> (deny_pfun pf) \<noteq> (allow_pfun pf)"
apply (erule contrapos_nn)
apply (rule ext)
apply (drule_tac x=x in fun_cong)
apply (auto simp: deny_pfun_def allow_pfun_def)
apply (case_tac "pf x = \<bottom>")
apply (auto)
done
section{* Common Instances *}
definition allow_all_fun :: "('\<alpha> \<Rightarrow> '\<beta>) \<Rightarrow> ('\<alpha> \<mapsto> '\<beta>)" ("A\<^sub>f")
where "allow_all_fun f = allow_pfun (Some o f)"
definition deny_all_fun :: "('\<alpha> \<Rightarrow> '\<beta>) \<Rightarrow> ('\<alpha> \<mapsto> '\<beta>)" ("D\<^sub>f")
where "deny_all_fun f \<equiv> deny_pfun (Some o f)"
definition
deny_all_id :: "'\<alpha> \<mapsto> '\<alpha>" ("D\<^sub>I") where
"deny_all_id \<equiv> deny_pfun (id o Some)"
definition
allow_all_id :: "'\<alpha> \<mapsto> '\<alpha>" ("A\<^sub>I") where
"allow_all_id \<equiv> allow_pfun (id o Some)"
definition
allow_all :: "('\<alpha> \<mapsto> unit)" ("A\<^sub>U") where
"allow_all p = \<lfloor>allow ()\<rfloor>"
definition
deny_all :: "('\<alpha> \<mapsto> unit)" ("D\<^sub>U") where
"deny_all p = \<lfloor>deny ()\<rfloor>"
text{* ... and resulting properties: *}
lemma "A\<^sub>I \<Oplus> empty = A\<^sub>I"
apply simp
done
lemma "A\<^sub>f f \<Oplus> empty = A\<^sub>f f"
apply simp
done
lemma "allow_pfun empty = empty"
apply (rule ext)
apply (simp add: allow_pfun_def)
done
lemma allow_left_cancel :"dom pf = UNIV \<Longrightarrow> (allow_pfun pf) \<Oplus> x = (allow_pfun pf)"
apply (rule ext)+
apply (auto simp: allow_pfun_def option.splits)
done
lemma deny_left_cancel :"dom pf = UNIV \<Longrightarrow> (deny_pfun pf) \<Oplus> x = (deny_pfun pf)"
apply (rule ext)+
apply (auto simp: deny_pfun_def option.splits)
done
section{* Domain, Range, and Restrictions *}
text{*
Since policies are essentially maps, we inherit the basic definitions for
domain and range on Maps: \\
\verb+Map.dom_def+ : @{thm Map.dom_def} \\
whereas range is just an abrreviation for image:
\begin{verbatim}
abbreviation range :: "('a => 'b) => 'b set"
where -- "of function" "range f == f ` UNIV"
\end{verbatim}
As a consequence, we inherit the following properties on
policies:
\begin{itemize}
\item \verb+Map.domD+ @{thm Map.domD}
\item\verb+Map.domI+ @{thm Map.domI}
\item\verb+Map.domIff+ @{thm Map.domIff}
\item\verb+Map.dom_const+ @{thm Map.dom_const}
\item\verb+Map.dom_def+ @{thm Map.dom_def}
\item\verb+Map.dom_empty+ @{thm Map.dom_empty}
\item\verb+Map.dom_eq_empty_conv+ @{thm Map.dom_eq_empty_conv}
\item\verb+Map.dom_eq_singleton_conv+ @{thm Map.dom_eq_singleton_conv}
\item\verb+Map.dom_fun_upd+ @{thm Map.dom_fun_upd}
\item\verb+Map.dom_if+ @{thm Map.dom_if}
\item\verb+Map.dom_map_add+ @{thm Map.dom_map_add}
\end{itemize}
*}
text{*
However, some properties are specific to policy concepts:
*}
lemma sub_ran : "ran p \<subseteq> Allow \<union> Deny"
apply (auto simp: Allow_def Deny_def ran_def full_SetCompr_eq[symmetric])
apply (case_tac "x")
apply (simp_all)
apply (erule_tac x="\<alpha>" in allE)
apply (simp)
done
lemma dom_allow_pfun [simp]:"dom(allow_pfun f) = dom f"
apply (auto simp: allow_pfun_def)
apply (case_tac "f x", simp_all)
done
lemma dom_allow_all: "dom(A\<^sub>f f) = UNIV"
by(auto simp: allow_all_fun_def o_def)
lemma dom_deny_pfun [simp]:"dom(deny_pfun f) = dom f"
apply (auto simp: deny_pfun_def)
apply (case_tac "f x")
apply (simp_all)
done
lemma dom_deny_all: " dom(D\<^sub>f f) = UNIV"
by(auto simp: deny_all_fun_def o_def)
lemma ran_allow_pfun [simp]:"ran(allow_pfun f) = allow `(ran f)"
apply (simp add: allow_pfun_def ran_def)
apply (rule set_eqI)
apply (auto)
apply (case_tac "f a")
apply (auto simp: image_def)
apply (rule_tac x=a in exI)
apply (simp)
done
lemma ran_allow_all: "ran(A\<^sub>f id) = Allow"
apply (simp add: allow_all_fun_def Allow_def o_def)
apply (rule set_eqI)
apply (auto simp: image_def ran_def)
done
lemma ran_deny_pfun[simp]: "ran(deny_pfun f) = deny ` (ran f)"
apply (simp add: deny_pfun_def ran_def)
apply (rule set_eqI)
apply (auto)
apply (case_tac "f a")
apply (auto simp: image_def)
apply (rule_tac x=a in exI)
apply (simp)
done
lemma ran_deny_all: "ran(D\<^sub>f id) = Deny"
apply (simp add: deny_all_fun_def Deny_def o_def)
apply (rule set_eqI)
apply (auto simp: image_def ran_def)
done
text{*
Reasoning over \verb+dom+ is most crucial since it paves the way for simplification and
reordering of policies composed by override (i.e. by the normal left-to-right rule composition
method.
\begin{itemize}
\item \verb+Map.dom_map_add+ @{thm Map.dom_map_add}
\item \verb+Map.inj_on_map_add_dom+ @{thm Map.inj_on_map_add_dom}
\item \verb+Map.map_add_comm+ @{thm Map.map_add_comm}
\item \verb+Map.map_add_dom_app_simps(1)+ @{thm Map.map_add_dom_app_simps(1)}
\item \verb+Map.map_add_dom_app_simps(2)+ @{thm Map.map_add_dom_app_simps(2)}
\item \verb+Map.map_add_dom_app_simps(3)+ @{thm Map.map_add_dom_app_simps(3)}
\item \verb+Map.map_add_upd_left+ @{thm Map.map_add_upd_left}
\end{itemize}
The latter rule also applies to allow- and deny-override.
*}
definition dom_restrict :: "['\<alpha> set, '\<alpha>\<mapsto>'\<beta>] \<Rightarrow> '\<alpha>\<mapsto>'\<beta>" (infixr "\<triangleleft>" 55)
where "S \<triangleleft> p \<equiv> (\<lambda>x. if x \<in> S then p x else \<bottom>)"
lemma dom_dom_restrict[simp] : "dom(S \<triangleleft> p) = S \<inter> dom p"
apply (auto simp: dom_restrict_def)
apply (case_tac "x \<in> S")
apply (simp_all)
apply (case_tac "x \<in> S")
apply (simp_all)
done
lemma dom_restrict_idem[simp] : "(dom p) \<triangleleft> p = p"
apply (rule ext)
apply (auto simp: dom_restrict_def
dest: neq_commute[THEN iffD1,THEN not_None_eq [THEN iffD1]])
done
lemma dom_restrict_inter[simp] : "T \<triangleleft> S \<triangleleft> p = T \<inter> S \<triangleleft> p"
apply (rule ext)
apply (auto simp: dom_restrict_def
dest: neq_commute[THEN iffD1,THEN not_None_eq [THEN iffD1]])
done
definition ran_restrict :: "['\<alpha>\<mapsto>'\<beta>,'\<beta> decision set] \<Rightarrow> '\<alpha> \<mapsto>'\<beta>" (infixr "\<triangleright>" 55)
where "p \<triangleright> S \<equiv> (\<lambda>x. if p x \<in> (Some`S) then p x else \<bottom>)"
definition ran_restrict2 :: "['\<alpha>\<mapsto>'\<beta>,'\<beta> decision set] \<Rightarrow> '\<alpha> \<mapsto>'\<beta>" (infixr "\<triangleright>2" 55)
where "p \<triangleright>2 S \<equiv> (\<lambda>x. if (the (p x)) \<in> (S) then p x else \<bottom>)"
lemma "ran_restrict = ran_restrict2"
apply (rule ext)+
apply (simp add: ran_restrict_def ran_restrict2_def)
apply (case_tac "x xb")
apply simp_all
apply (metis inj_Some inj_image_mem_iff)
done
lemma ran_ran_restrict[simp] : "ran(p \<triangleright> S) = S \<inter> ran p"
by(auto simp: ran_restrict_def image_def ran_def)
lemma ran_restrict_idem[simp] : "p \<triangleright> (ran p) = p"
apply (rule ext)
apply (auto simp: ran_restrict_def image_def Ball_def ran_def)
apply (erule contrapos_pp)
apply (auto dest!: neq_commute[THEN iffD1,THEN not_None_eq [THEN iffD1]])
done
lemma ran_restrict_inter[simp] : "(p \<triangleright> S) \<triangleright> T = p \<triangleright> T \<inter> S"
apply (rule ext)
apply (auto simp: ran_restrict_def
dest: neq_commute[THEN iffD1,THEN not_None_eq [THEN iffD1]])
done
lemma ran_gen_A[simp] : "(\<forall>Ax. \<lfloor>P x\<rfloor>) \<triangleright> Allow = (\<forall>Ax. \<lfloor>P x\<rfloor>)"
apply (rule ext)
apply (auto simp: Allow_def ran_restrict_def)
done
lemma ran_gen_D[simp] : "(\<forall>Dx. \<lfloor>P x\<rfloor>) \<triangleright> Deny = (\<forall>Dx. \<lfloor>P x\<rfloor>)"
apply (rule ext)
apply (auto simp: Deny_def ran_restrict_def)
done
lemmas ElementaryPoliciesDefs = deny_pfun_def allow_pfun_def allow_all_fun_def deny_all_fun_def
allow_all_id_def deny_all_id_def allow_all_def deny_all_def
dom_restrict_def ran_restrict_def
end

576
Monads.thy Normal file
View File

@ -0,0 +1,576 @@
(*****************************************************************************
* HOL-TestGen --- theorem-prover based test case generation
* http://www.brucker.ch/projects/hol-testgen/
*
* Monads.thy --- a base testing theory for sequential computations.
* This file is part of HOL-TestGen.
*
* Copyright (c) 2005-2012 ETH Zurich, Switzerland
* 2009-2014 Univ. Paris-Sud, France
* 2009-2014 Achim D. Brucker, Germany
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* * Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above
* copyright notice, this list of conditions and the following
* disclaimer in the documentation and/or other materials provided
* with the distribution.
*
* * Neither the name of the copyright holders nor the names of its
* contributors may be used to endorse or promote products derived
* from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
******************************************************************************)
(* $Id: Monads.thy 10922 2014-11-10 15:41:49Z wolff $ *)
header {* Basic Monad Theory for Sequential Computations *}
theory
Monads
imports
Main
begin
section{* General Framework for Monad-based Sequence-Test *}
text{*
As such, Higher-order Logic as a purely functional specification formalism has no built-in
mechanism for state and state-transitions. Forms of testing involving state require therefore
explicit mechanisms for their treatment inside the logic; a well-known technique to model
states inside purely functional languages are \emph{monads} made popular by Wadler and Moggi
and extensively used in Haskell. \HOL is powerful enough to represent the most important
standard monads; however, it is not possible to represent monads as such due to well-known
limitations of the Hindley-Milner type-system.
Here is a variant for state-exception monads, that models precisely transition functions with
preconditions. Next, we declare the state-backtrack-monad. In all of them, our concept of
i/o-stepping functions can be formulated; these are functions mapping input to a given monad.
Later on, we will build the usual concepts of:
\begin{enumerate}
\item deterministic i/o automata,
\item non-deterministic i/o automata, and
\item labelled transition systems (LTS)
\end{enumerate}
*}
subsection{* State Exception Monads *}
type_synonym ('o, '\<sigma>) MON\<^sub>S\<^sub>E = "'\<sigma> \<rightharpoonup> ('o \<times> '\<sigma>)"
definition bind_SE :: "('o,'\<sigma>)MON\<^sub>S\<^sub>E \<Rightarrow> ('o \<Rightarrow> ('o','\<sigma>)MON\<^sub>S\<^sub>E) \<Rightarrow> ('o','\<sigma>)MON\<^sub>S\<^sub>E"
where "bind_SE f g = (\<lambda>\<sigma>. case f \<sigma> of None \<Rightarrow> None
| Some (out, \<sigma>') \<Rightarrow> g out \<sigma>')"
notation bind_SE ("bind\<^sub>S\<^sub>E")
syntax (xsymbols)
"_bind_SE" :: "[pttrn,('o,'\<sigma>)MON\<^sub>S\<^sub>E,('o','\<sigma>)MON\<^sub>S\<^sub>E] \<Rightarrow> ('o','\<sigma>)MON\<^sub>S\<^sub>E"
("(2 _ \<leftarrow> _; _)" [5,8,8]8)
translations
"x \<leftarrow> f; g" \<rightleftharpoons> "CONST bind_SE f (% x . g)"
definition unit_SE :: "'o \<Rightarrow> ('o, '\<sigma>)MON\<^sub>S\<^sub>E" ("(return _)" 8)
where "unit_SE e = (\<lambda>\<sigma>. Some(e,\<sigma>))"
notation unit_SE ("unit\<^sub>S\<^sub>E")
definition fail\<^sub>S\<^sub>E :: "('o, '\<sigma>)MON\<^sub>S\<^sub>E"
where "fail\<^sub>S\<^sub>E = (\<lambda>\<sigma>. None)"
notation fail\<^sub>S\<^sub>E ("fail\<^sub>S\<^sub>E")
definition assert_SE :: "('\<sigma> \<Rightarrow> bool) \<Rightarrow> (bool, '\<sigma>)MON\<^sub>S\<^sub>E"
where "assert_SE P = (\<lambda>\<sigma>. if P \<sigma> then Some(True,\<sigma>) else None)"
notation assert_SE ("assert\<^sub>S\<^sub>E")
definition assume_SE :: "('\<sigma> \<Rightarrow> bool) \<Rightarrow> (unit, '\<sigma>)MON\<^sub>S\<^sub>E"
where "assume_SE P = (\<lambda>\<sigma>. if \<exists>\<sigma> . P \<sigma> then Some((), SOME \<sigma> . P \<sigma>) else None)"
notation assume_SE ("assume\<^sub>S\<^sub>E")
definition if_SE :: "['\<sigma> \<Rightarrow> bool, ('\<alpha>, '\<sigma>)MON\<^sub>S\<^sub>E, ('\<alpha>, '\<sigma>)MON\<^sub>S\<^sub>E] \<Rightarrow> ('\<alpha>, '\<sigma>)MON\<^sub>S\<^sub>E"
where "if_SE c E F = (\<lambda>\<sigma>. if c \<sigma> then E \<sigma> else F \<sigma>)"
notation if_SE ("if\<^sub>S\<^sub>E")
text{*
The standard monad theorems about unit and associativity:
*}
lemma bind_left_unit : "(x \<leftarrow> return a; k) = k"
apply (simp add: unit_SE_def bind_SE_def)
done
lemma bind_right_unit: "(x \<leftarrow> m; return x) = m"
apply (simp add: unit_SE_def bind_SE_def)
apply (rule ext)
apply (case_tac "m \<sigma>")
apply ( simp_all)
done
lemma bind_assoc: "(y \<leftarrow> (x \<leftarrow> m; k); h) = (x \<leftarrow> m; (y \<leftarrow> k; h))"
apply (simp add: unit_SE_def bind_SE_def)
apply (rule ext)
apply (case_tac "m \<sigma>", simp_all)
apply (case_tac "a", simp_all)
done
text{*
In order to express test-sequences also on the object-level and to make our theory amenable to
formal reasoning over test-sequences, we represent them as lists of input and generalize the
bind-operator of the state-exception monad accordingly. The approach is straightforward, but
comes with a price: we have to encapsulate all input and output data into one type. Assume that
we have a typed interface to a module with the operations $op_1$, $op_2$, \ldots, $op_n$ with
the inputs $\iota_1$, $\iota_2$, \ldots, $\iota_n$ (outputs are treated analogously). Then we
can encode for this interface the general input - type:
\begin{displaymath}
\texttt{datatype}\ \texttt{in}\ =\ op_1\ ::\ \iota_1\ |\ ...\ |\ \iota_n
\end{displaymath}
Obviously, we loose some type-safety in this approach; we have to express that in traces only
\emph{corresponding} input and output belonging to the same operation will occur; this form
of side-conditions have to be expressed inside \HOL. From the user perspective, this will not
make much difference, since junk-data resulting from too weak typing can be ruled out by adopted
front-ends.
*}
text{*
In order to express test-sequences also on the object-level and to make our theory amenable to
formal reasoning over test-sequences, we represent them as lists of input and generalize the
bind-operator of the state-exception monad accordingly. Thus, the notion of test-sequence
is mapped to the notion of a \emph{computation}, a semantic notion; at times we will use
reifications of computations, \ie{} a data-type in order to make computation amenable to
case-splitting and meta-theoretic reasoning. To this end, we have to encapsulate all input
and output data into one type. Assume that we have a typed interface to a module with
the operations $op_1$, $op_2$, \ldots, $op_n$ with the inputs $\iota_1$, $\iota_2$, \ldots,
$\iota_n$ (outputs are treated analogously).
Then we can encode for this interface the general input - type:
\begin{displaymath}
\texttt{datatype}\ \texttt{in}\ =\ op_1\ ::\ \iota_1\ |\ ...\ |\ \iota_n
\end{displaymath}
Obviously, we loose some type-safety in this approach; we have to express
that in traces only \emph{corresponding} input and output belonging to the
same operation will occur; this form of side-conditions have to be expressed
inside \HOL. From the user perspective, this will not make much difference,
since junk-data resulting from too weak typing can be ruled out by adopted
front-ends. *}
text{* Note that the subsequent notion of a test-sequence allows the io stepping
function (and the special case of a program under test) to stop execution
\emph{within} the sequence; such premature terminations are characterized by an
output list which is shorter than the input list. Note that our primary
notion of multiple execution ignores failure and reports failure
steps only by missing results ... *}
fun mbind :: "'\<iota> list \<Rightarrow> ('\<iota> \<Rightarrow> ('o,'\<sigma>) MON\<^sub>S\<^sub>E) \<Rightarrow> ('o list,'\<sigma>) MON\<^sub>S\<^sub>E"
where "mbind [] iostep \<sigma> = Some([], \<sigma>)" |
"mbind (a#H) iostep \<sigma> =
(case iostep a \<sigma> of
None \<Rightarrow> Some([], \<sigma>)
| Some (out, \<sigma>') \<Rightarrow> (case mbind H iostep \<sigma>' of
None \<Rightarrow> Some([out],\<sigma>')
| Some(outs,\<sigma>'') \<Rightarrow> Some(out#outs,\<sigma>'')))"
text{* As mentioned, this definition is fail-safe; in case of an exception,
the current state is maintained, no result is reported.
An alternative is the fail-strict variant @{text "mbind'"} defined below. *}
lemma mbind_unit [simp]: "mbind [] f = (return [])"
by(rule ext, simp add: unit_SE_def)
lemma mbind_nofailure [simp]: "mbind S f \<sigma> \<noteq> None"
apply (rule_tac x=\<sigma> in spec)
apply (induct S)
apply (auto simp:unit_SE_def)
apply (case_tac "f a x")
apply ( auto)
apply (erule_tac x="b" in allE)
apply (erule exE)
apply (erule exE)
apply (simp)
done
text{* The fail-strict version of @{text mbind'} looks as follows: *}
fun mbind' :: "'\<iota> list \<Rightarrow> ('\<iota> \<Rightarrow> ('o,'\<sigma>) MON\<^sub>S\<^sub>E) \<Rightarrow> ('o list,'\<sigma>) MON\<^sub>S\<^sub>E"
where "mbind' [] iostep \<sigma> = Some([], \<sigma>)" |
"mbind' (a#H) iostep \<sigma> =
(case iostep a \<sigma> of
None \<Rightarrow> None
| Some (out, \<sigma>') \<Rightarrow> (case mbind H iostep \<sigma>' of
None \<Rightarrow> None (* fail-strict *)
| Some(outs,\<sigma>'') \<Rightarrow> Some(out#outs,\<sigma>'')))"
text{*
mbind' as failure strict operator can be seen as a foldr on bind---if the types would
match \ldots
*}
definition try_SE :: "('o,'\<sigma>) MON\<^sub>S\<^sub>E \<Rightarrow> ('o option,'\<sigma>) MON\<^sub>S\<^sub>E"
where "try_SE ioprog = (\<lambda>\<sigma>. case ioprog \<sigma> of
None \<Rightarrow> Some(None, \<sigma>)
| Some(outs, \<sigma>') \<Rightarrow> Some(Some outs, \<sigma>'))"
text{* In contrast @{term mbind} as a failure safe operator can roughly be seen
as a @{term foldr} on bind - try:
@{text "m1 ; try m2 ; try m3; ..."}. Note, that the rough equivalence only holds for
certain predicates in the sequence - length equivalence modulo None,
for example. However, if a conditional is added, the equivalence
can be made precise: *}
lemma mbind_try:
"(x \<leftarrow> mbind (a#S) F; M x) =
(a' \<leftarrow> try_SE(F a);
if a' = None
then (M [])
else (x \<leftarrow> mbind S F; M (the a' # x)))"
apply (rule ext)
apply (simp add: bind_SE_def try_SE_def)
apply (case_tac "F a x")
apply (auto)
apply (simp add: bind_SE_def try_SE_def)
apply (case_tac "mbind S F b")
apply (auto)
done
text{* On this basis, a symbolic evaluation scheme can be established
that reduces @{term mbind}-code to @{term try_SE}-code and If-cascades. *}
definition alt_SE :: "[('o, '\<sigma>)MON\<^sub>S\<^sub>E, ('o, '\<sigma>)MON\<^sub>S\<^sub>E] \<Rightarrow> ('o, '\<sigma>)MON\<^sub>S\<^sub>E" (infixl "\<sqinter>\<^sub>S\<^sub>E" 10)
where "(f \<sqinter>\<^sub>S\<^sub>E g) = (\<lambda> \<sigma>. case f \<sigma> of None \<Rightarrow> g \<sigma>
| Some H \<Rightarrow> Some H)"
definition malt_SE :: "('o, '\<sigma>)MON\<^sub>S\<^sub>E list \<Rightarrow> ('o, '\<sigma>)MON\<^sub>S\<^sub>E"
where "malt_SE S = foldr alt_SE S fail\<^sub>S\<^sub>E"
notation malt_SE ("\<Sqinter>\<^sub>S\<^sub>E")
lemma malt_SE_mt [simp]: "\<Sqinter>\<^sub>S\<^sub>E [] = fail\<^sub>S\<^sub>E"
by(simp add: malt_SE_def)
lemma malt_SE_cons [simp]: "\<Sqinter>\<^sub>S\<^sub>E (a # S) = (a \<sqinter>\<^sub>S\<^sub>E (\<Sqinter>\<^sub>S\<^sub>E S))"
by(simp add: malt_SE_def)
subsection{* State-Backtrack Monads *}
text{*This subsection is still rudimentary and as such an interesting
formal analogue to the previous monad definitions. It is doubtful that it is
interesting for testing and as a computational structure at all.
Clearly more relevant is ``sequence'' instead of ``set,'' which would
rephrase Isabelle's internal tactic concept.
*}
type_synonym ('o, '\<sigma>) MON\<^sub>S\<^sub>B = "'\<sigma> \<Rightarrow> ('o \<times> '\<sigma>) set"
definition bind_SB :: "('o, '\<sigma>)MON\<^sub>S\<^sub>B \<Rightarrow> ('o \<Rightarrow> ('o', '\<sigma>)MON\<^sub>S\<^sub>B) \<Rightarrow> ('o', '\<sigma>)MON\<^sub>S\<^sub>B"
where "bind_SB f g \<sigma> = \<Union> ((\<lambda>(out, \<sigma>). (g out \<sigma>)) ` (f \<sigma>))"
notation bind_SB ("bind\<^sub>S\<^sub>B")
definition unit_SB :: "'o \<Rightarrow> ('o, '\<sigma>)MON\<^sub>S\<^sub>B" ("(returns _)" 8)
where "unit_SB e = (\<lambda>\<sigma>. {(e,\<sigma>)})"
notation unit_SB ("unit\<^sub>S\<^sub>B")
syntax (xsymbols) "_bind_SB" :: "[pttrn,('o,'\<sigma>)MON\<^sub>S\<^sub>B,('o','\<sigma>)MON\<^sub>S\<^sub>B] \<Rightarrow> ('o','\<sigma>)MON\<^sub>S\<^sub>B"
("(2 _ := _; _)" [5,8,8]8)
translations
"x := f; g" \<rightleftharpoons> "CONST bind_SB f (% x . g)"
lemma bind_left_unit_SB : "(x := returns a; m) = m"
apply (rule ext)
apply (simp add: unit_SB_def bind_SB_def)
done
lemma bind_right_unit_SB: "(x := m; returns x) = m"
apply (rule ext)
apply (simp add: unit_SB_def bind_SB_def)
done
lemma bind_assoc_SB: "(y := (x := m; k); h) = (x := m; (y := k; h))"
apply (rule ext)
apply (simp add: unit_SB_def bind_SB_def split_def)
done
subsection{* State Backtrack Exception Monad *}
text{*
The following combination of the previous two Monad-Constructions allows for the semantic
foundation of a simple generic assertion language in the style of Schirmer's Simpl-Language or
Rustan Leino's Boogie-PL language. The key is to use the exceptional element None for violations
of the assert-statement.
*}
type_synonym ('o, '\<sigma>) MON\<^sub>S\<^sub>B\<^sub>E = "'\<sigma> \<Rightarrow> (('o \<times> '\<sigma>) set) option"
definition bind_SBE :: "('o,'\<sigma>)MON\<^sub>S\<^sub>B\<^sub>E \<Rightarrow> ('o \<Rightarrow> ('o','\<sigma>)MON\<^sub>S\<^sub>B\<^sub>E) \<Rightarrow> ('o','\<sigma>)MON\<^sub>S\<^sub>B\<^sub>E"
where "bind_SBE f g = (\<lambda>\<sigma>. case f \<sigma> of None \<Rightarrow> None
| Some S \<Rightarrow> (let S' = (\<lambda>(out, \<sigma>'). g out \<sigma>') ` S
in if None \<in> S' then None
else Some(\<Union> (the ` S'))))"
syntax (xsymbols) "_bind_SBE" :: "[pttrn,('o,'\<sigma>)MON\<^sub>S\<^sub>B\<^sub>E,('o','\<sigma>)MON\<^sub>S\<^sub>B\<^sub>E] \<Rightarrow> ('o','\<sigma>)MON\<^sub>S\<^sub>B\<^sub>E"
("(2 _ :\<equiv> _; _)" [5,8,8]8)
translations
"x :\<equiv> f; g" \<rightleftharpoons> "CONST bind_SBE f (% x . g)"
definition unit_SBE :: "'o \<Rightarrow> ('o, '\<sigma>)MON\<^sub>S\<^sub>B\<^sub>E" ("(returning _)" 8)
where "unit_SBE e = (\<lambda>\<sigma>. Some({(e,\<sigma>)}))"
definition assert_SBE :: "('\<sigma> \<Rightarrow> bool) \<Rightarrow> (unit, '\<sigma>)MON\<^sub>S\<^sub>B\<^sub>E"
where "assert_SBE e = (\<lambda>\<sigma>. if e \<sigma> then Some({((),\<sigma>)})
else None)"
notation assert_SBE ("assert\<^sub>S\<^sub>B\<^sub>E")
definition assume_SBE :: "('\<sigma> \<Rightarrow> bool) \<Rightarrow> (unit, '\<sigma>)MON\<^sub>S\<^sub>B\<^sub>E"
where "assume_SBE e = (\<lambda>\<sigma>. if e \<sigma> then Some({((),\<sigma>)})
else Some {})"
notation assume_SBE ("assume\<^sub>S\<^sub>B\<^sub>E")
definition havoc_SBE :: " (unit, '\<sigma>)MON\<^sub>S\<^sub>B\<^sub>E"
where "havoc_SBE = (\<lambda>\<sigma>. Some({x. True}))"
notation havoc_SBE ("havoc\<^sub>S\<^sub>B\<^sub>E")
lemma bind_left_unit_SBE : "(x :\<equiv> returning a; m) = m"
apply (rule ext)
apply (simp add: unit_SBE_def bind_SBE_def)
done
lemma bind_right_unit_SBE: "(x :\<equiv> m; returning x) = m"
apply (rule ext)
apply (simp add: unit_SBE_def bind_SBE_def)
apply (case_tac "m x")
apply (simp_all add:Let_def)
apply (rule HOL.ccontr)
apply (simp add: Set.image_iff)
done
lemmas aux = trans[OF HOL.neq_commute,OF Option.not_None_eq]
lemma bind_assoc_SBE: "(y :\<equiv> (x :\<equiv> m; k); h) = (x :\<equiv> m; (y :\<equiv> k; h))"
proof (rule ext, simp add: unit_SBE_def bind_SBE_def,
case_tac "m x", simp_all add: Let_def Set.image_iff, safe)
case goal1 then show ?case
by(rule_tac x="(a, b)" in bexI, simp_all)
next
case goal2 then show ?case
apply (rule_tac x="(aa, b)" in bexI, simp_all add:split_def)
apply (erule_tac x="(aa,b)" in ballE)
apply (auto simp: aux image_def split_def intro!: rev_bexI)
done
next
case goal3 then show ?case
by(rule_tac x="(a, b)" in bexI, simp_all)
next
case goal4 then show ?case
apply (erule_tac Q="None = ?X" in contrapos_pp)
apply (erule_tac x="(aa,b)" and P="\<lambda> x. None \<noteq> split (\<lambda>out. k) x" in ballE)
apply (auto simp: aux (*Option.not_None_eq*) image_def split_def intro!: rev_bexI)
done
next
case goal5 then show ?case
apply simp apply ((erule_tac x="(ab,ba)" in ballE)+)
apply (simp_all add: aux (* Option.not_None_eq *), (erule exE)+, simp add:split_def)
apply (erule rev_bexI, case_tac "None\<in>(\<lambda>p. h(snd p))`y",auto simp:split_def)
done
next
case goal6 then show ?case
apply simp apply ((erule_tac x="(a,b)" in ballE)+)
apply (simp_all add: aux (* Option.not_None_eq *), (erule exE)+, simp add:split_def)
apply (erule rev_bexI, case_tac "None\<in>(\<lambda>p. h(snd p))`y",auto simp:split_def)
done
qed
section{* Valid Test Sequences in the State Exception Monad *}
text{*
This is still an unstructured merge of executable monad concepts and specification oriented
high-level properties initiating test procedures.
*}
definition valid_SE :: "'\<sigma> \<Rightarrow> (bool,'\<sigma>) MON\<^sub>S\<^sub>E \<Rightarrow> bool" (infix "\<Turnstile>" 15)
where "(\<sigma> \<Turnstile> m) = (m \<sigma> \<noteq> None \<and> fst(the (m \<sigma>)))"
text{*
This notation consideres failures as valid---a definition inspired by I/O conformance.
Note that it is not possible to define this concept once and for all in a Hindley-Milner
type-system. For the moment, we present it only for the state-exception monad, although for
the same definition, this notion is applicable to other monads as well.
*}
lemma syntax_test :
"\<sigma> \<Turnstile> (os \<leftarrow> (mbind \<iota>s ioprog); return(length \<iota>s = length os))"
oops
lemma valid_true[simp]: "(\<sigma> \<Turnstile> (s \<leftarrow> return x ; return (P s))) = P x"
by(simp add: valid_SE_def unit_SE_def bind_SE_def)
text{* Recall mbind\_unit for the base case. *}
lemma valid_failure: "ioprog a \<sigma> = None \<Longrightarrow>
(\<sigma> \<Turnstile> (s \<leftarrow> mbind (a#S) ioprog ; M s)) =
(\<sigma> \<Turnstile> (M []))"
by(simp add: valid_SE_def unit_SE_def bind_SE_def)
lemma valid_failure': "A \<sigma> = None \<Longrightarrow> \<not>(\<sigma> \<Turnstile> ((s \<leftarrow> A ; M s)))"
by(simp add: valid_SE_def unit_SE_def bind_SE_def)
lemma valid_successElem: (* atomic boolean Monad "Query Functions" *)
"M \<sigma> = Some(f \<sigma>,\<sigma>) \<Longrightarrow> (\<sigma> \<Turnstile> M) = f \<sigma>"
by(simp add: valid_SE_def unit_SE_def bind_SE_def )
lemma valid_success: "ioprog a \<sigma> = Some(b,\<sigma>') \<Longrightarrow>
(\<sigma> \<Turnstile> (s \<leftarrow> mbind (a#S) ioprog ; M s)) =
(\<sigma>' \<Turnstile> (s \<leftarrow> mbind S ioprog ; M (b#s)))"
apply (simp add: valid_SE_def unit_SE_def bind_SE_def )
apply (cases "mbind S ioprog \<sigma>'", auto)
done
lemma valid_success'': "ioprog a \<sigma> = Some(b,\<sigma>') \<Longrightarrow>
(\<sigma> \<Turnstile> (s \<leftarrow> mbind (a#S) ioprog ; return (P s))) =
(\<sigma>' \<Turnstile> (s \<leftarrow> mbind S ioprog ; return (P (b#s))))"
apply (simp add: valid_SE_def unit_SE_def bind_SE_def )
apply (cases "mbind S ioprog \<sigma>'")
apply (simp_all)
apply (auto)
done
lemma valid_success': "A \<sigma> = Some(b,\<sigma>') \<Longrightarrow> (\<sigma> \<Turnstile> ((s \<leftarrow> A ; M s))) = (\<sigma>' \<Turnstile> (M b))"
by(simp add: valid_SE_def unit_SE_def bind_SE_def )
lemma valid_both: "(\<sigma> \<Turnstile> (s \<leftarrow> mbind (a#S) ioprog ; return (P s))) =
(case ioprog a \<sigma> of
None \<Rightarrow> (\<sigma> \<Turnstile> (return (P [])))
| Some(b,\<sigma>') \<Rightarrow> (\<sigma>' \<Turnstile> (s \<leftarrow> mbind S ioprog ; return (P (b#s)))))"
apply (case_tac "ioprog a \<sigma>")
apply (simp_all add: valid_failure valid_success'' split: prod.splits)
done
lemma valid_propagate_1 [simp]: "(\<sigma> \<Turnstile> (return P)) = (P)"
by(auto simp: valid_SE_def unit_SE_def)
lemma valid_propagate_2: "\<sigma> \<Turnstile> ((s \<leftarrow> A ; M s)) \<Longrightarrow> \<exists> v \<sigma>'. the(A \<sigma>) = (v,\<sigma>') \<and> \<sigma>' \<Turnstile> (M v)"
apply (auto simp: valid_SE_def unit_SE_def bind_SE_def)
apply (cases "A \<sigma>")
apply (simp_all)
apply (drule_tac x="A \<sigma>" and f=the in arg_cong)
apply (simp)
apply (rule_tac x="fst aa" in exI)
apply (rule_tac x="snd aa" in exI)
apply (auto)
done
lemma valid_propagate_2': "\<sigma> \<Turnstile> ((s \<leftarrow> A ; M s)) \<Longrightarrow> \<exists> a. (A \<sigma>) = Some a \<and> (snd a) \<Turnstile> (M (fst a))"
apply (auto simp: valid_SE_def unit_SE_def bind_SE_def)
apply (cases "A \<sigma>")
apply (simp_all)
apply (simp_all split: prod.splits)
apply (drule_tac x="A \<sigma>" and f=the in arg_cong)
apply (simp)
apply (rule_tac x="fst aa" in exI)
apply (rule_tac x="snd aa" in exI)
apply (auto)
done
lemma valid_propagate_2'': "\<sigma> \<Turnstile> ((s \<leftarrow> A ; M s)) \<Longrightarrow> \<exists> v \<sigma>'. A \<sigma> = Some(v,\<sigma>') \<and> \<sigma>' \<Turnstile> (M v)"
apply (auto simp: valid_SE_def unit_SE_def bind_SE_def)
apply (cases "A \<sigma>")
apply (simp_all)
apply (drule_tac x="A \<sigma>" and f=the in arg_cong)
apply (simp)
apply (rule_tac x="fst aa" in exI)
apply (rule_tac x="snd aa" in exI)
apply (auto)
done
lemma valid_propoagate_3[simp]: "(\<sigma>\<^sub>0 \<Turnstile> (\<lambda>\<sigma>. Some (f \<sigma>, \<sigma>))) = (f \<sigma>\<^sub>0)"
by(simp add: valid_SE_def )
lemma valid_propoagate_3'[simp]: "\<not>(\<sigma>\<^sub>0 \<Turnstile> (\<lambda>\<sigma>. None))"
by(simp add: valid_SE_def )
lemma assert_disch1 :" P \<sigma> \<Longrightarrow> (\<sigma> \<Turnstile> (x \<leftarrow> assert\<^sub>S\<^sub>E P; M x)) = (\<sigma> \<Turnstile> (M True))"
by(auto simp: bind_SE_def assert_SE_def valid_SE_def)
lemma assert_disch2 :" \<not> P \<sigma> \<Longrightarrow> \<not> (\<sigma> \<Turnstile> (x \<leftarrow> assert\<^sub>S\<^sub>E P ; M s))"
by(auto simp: bind_SE_def assert_SE_def valid_SE_def)
lemma assert_disch3 :" \<not> P \<sigma> \<Longrightarrow> \<not> (\<sigma> \<Turnstile> (assert\<^sub>S\<^sub>E P))"
by(auto simp: bind_SE_def assert_SE_def valid_SE_def)
lemma assert_D : "(\<sigma> \<Turnstile> (x \<leftarrow> assert\<^sub>S\<^sub>E P; M x)) \<Longrightarrow> P \<sigma> \<and> (\<sigma> \<Turnstile> (M True))"
by(auto simp: bind_SE_def assert_SE_def valid_SE_def split: HOL.split_if_asm)
lemma assume_D : "(\<sigma> \<Turnstile> (x \<leftarrow> assume\<^sub>S\<^sub>E P; M x)) \<Longrightarrow> \<exists> \<sigma>. (P \<sigma> \<and> \<sigma> \<Turnstile> (M ()))"
apply (auto simp: bind_SE_def assume_SE_def valid_SE_def split: HOL.split_if_asm)
apply (rule_tac x="Eps P" in exI)
apply (auto)
apply (rule_tac x="True" in exI, rule_tac x="b" in exI)
apply (subst Hilbert_Choice.someI)
apply (assumption)
apply (simp)
apply (subst Hilbert_Choice.someI,assumption)
apply (simp)
done
text{*
These two rule prove that the SE Monad in connection with the notion of valid sequence is
actually sufficient for a representation of a Boogie-like language. The SBE monad with explicit
sets of states---to be shown below---is strictly speaking not necessary (and will therefore
be discontinued in the development).
*}
lemma if_SE_D1 : "P \<sigma> \<Longrightarrow> (\<sigma> \<Turnstile> if\<^sub>S\<^sub>E P B\<^sub>1 B\<^sub>2) = (\<sigma> \<Turnstile> B\<^sub>1)"
by(auto simp: if_SE_def valid_SE_def)
lemma if_SE_D2 : "\<not> P \<sigma> \<Longrightarrow> (\<sigma> \<Turnstile> if\<^sub>S\<^sub>E P B\<^sub>1 B\<^sub>2) = (\<sigma> \<Turnstile> B\<^sub>2)"
by(auto simp: if_SE_def valid_SE_def)
lemma if_SE_split_asm : " (\<sigma> \<Turnstile> if\<^sub>S\<^sub>E P B\<^sub>1 B\<^sub>2) = ((P \<sigma> \<and> (\<sigma> \<Turnstile> B\<^sub>1)) \<or> (\<not> P \<sigma> \<and> (\<sigma> \<Turnstile> B\<^sub>2)))"
by(cases "P \<sigma>",auto simp: if_SE_D1 if_SE_D2)
lemma if_SE_split : " (\<sigma> \<Turnstile> if\<^sub>S\<^sub>E P B\<^sub>1 B\<^sub>2) = ((P \<sigma> \<longrightarrow> (\<sigma> \<Turnstile> B\<^sub>1)) \<and> (\<not> P \<sigma> \<longrightarrow> (\<sigma> \<Turnstile> B\<^sub>2)))"
by(cases "P \<sigma>", auto simp: if_SE_D1 if_SE_D2)
lemma [code]: "(\<sigma> \<Turnstile> m) = (case (m \<sigma>) of None \<Rightarrow> False | (Some (x,y)) \<Rightarrow> x)"
apply (simp add: valid_SE_def)
apply (cases "m \<sigma> = None")
apply (simp_all)
apply (insert not_None_eq)
apply (auto)
done
section{* Valid Test Sequences in the State Exception Backtrack Monad *}
text{*
This is still an unstructured merge of executable monad concepts and specification oriented
high-level properties initiating test procedures.
*}
definition valid_SBE :: "'\<sigma> \<Rightarrow> ('a,'\<sigma>) MON\<^sub>S\<^sub>B\<^sub>E \<Rightarrow> bool" (infix "\<Turnstile>\<^sub>S\<^sub>B\<^sub>E" 15)
where "\<sigma> \<Turnstile>\<^sub>S\<^sub>B\<^sub>E m \<equiv> (m \<sigma> \<noteq> None)"
text{*
This notation considers all non-failures as valid.
*}
lemma assume_assert: "(\<sigma> \<Turnstile>\<^sub>S\<^sub>B\<^sub>E ( _ :\<equiv> assume\<^sub>S\<^sub>B\<^sub>E P ; assert\<^sub>S\<^sub>B\<^sub>E Q)) = (P \<sigma> \<longrightarrow> Q \<sigma>)"
by(simp add: valid_SBE_def assume_SBE_def assert_SBE_def bind_SBE_def)
lemma assert_intro: "Q \<sigma> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>S\<^sub>B\<^sub>E (assert\<^sub>S\<^sub>B\<^sub>E Q)"
by(simp add: valid_SBE_def assume_SBE_def assert_SBE_def bind_SBE_def)
(* legacy : lemmas valid_failure''=valid_failure *)
end

428
Normalisation.thy Normal file
View File

@ -0,0 +1,428 @@
(*****************************************************************************
* HOL-TestGen --- theorem-prover based test case generation
* http://www.brucker.ch/projects/hol-testgen/
*
* This file is part of HOL-TestGen.
*
* Copyright (c) 2005-2012 ETH Zurich, Switzerland
* 2008-2014 Achim D. Brucker, Germany
* 2009-2014 Université Paris-Sud, France
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* * Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above
* copyright notice, this list of conditions and the following
* disclaimer in the documentation and/or other materials provided
* with the distribution.
*
* * Neither the name of the copyright holders nor the names of its
* contributors may be used to endorse or promote products derived
* from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
******************************************************************************)
(* $Id: Normalisation.thy 10879 2014-10-26 11:35:31Z brucker $ *)
header{* Policy Transformations *}
theory
Normalisation
imports
SeqComposition
ParallelComposition
begin
text{*
This theory provides the formalisations required for the transformation of UPF policies.
A typical usage scenario can be observed in the firewall case
study~\cite{brucker.ea:formal-fw-testing:2014}.
*}
section{* Elementary Operators *}
text{*
We start by providing several operators and theorems useful when reasoning about a list of
rules which should eventually be interpreted as combined using the standard override operator.
*}
text{*
The following definition takes as argument a list of rules and returns a policy where the
rules are combined using the standard override operator.
*}
definition list2policy::"('a \<mapsto> 'b) list \<Rightarrow> ('a \<mapsto> 'b)" where
"list2policy l = foldr (\<lambda> x y. (x \<Oplus> y)) l \<emptyset>"
text{*
Determine the position of element of a list.
*}
fun position :: "'\<alpha> \<Rightarrow> '\<alpha> list \<Rightarrow> nat" where
"position a [] = 0"
|"(position a (x#xs)) = (if a = x then 1 else (Suc (position a xs)))"
text{*
Provides the first applied rule of a policy given as a list of rules.
*}
fun applied_rule where
"applied_rule C a (x#xs) = (if a \<in> dom (C x) then (Some x)
else (applied_rule C a xs))"
|"applied_rule C a [] = None"
text {*
The following is used if the list is constructed backwards.
*}
definition applied_rule_rev where
"applied_rule_rev C a x = applied_rule C a (rev x)"
text{*
The following is a typical policy transformation. It can be applied to any type of policy and
removes all the rules from a policy with an empty domain. It takes two arguments: a semantic
interpretation function and a list of rules.
*}
fun rm_MT_rules where
"rm_MT_rules C (x#xs) = (if dom (C x)= {}
then rm_MT_rules C xs
else x#(rm_MT_rules C xs))"
|"rm_MT_rules C [] = []"
text {*
The following invariant establishes that there are no rules with an empty domain in a list
of rules.
*}
fun none_MT_rules where
"none_MT_rules C (x#xs) = (dom (C x) \<noteq> {} \<and> (none_MT_rules C xs))"
|"none_MT_rules C [] = True"
text{*
The following related invariant establishes that the policy has not a completely empty domain.
*}
fun not_MT where
"not_MT C (x#xs) = (if (dom (C x) = {}) then (not_MT C xs) else True)"
|"not_MT C [] = False"
text{*
Next, a few theorems about the two invariants and the transformation:
*}
lemma none_MT_rules_vs_notMT: "none_MT_rules C p \<Longrightarrow> p \<noteq> [] \<Longrightarrow> not_MT C p"
apply (induct p)
apply (simp_all)
done
lemma rmnMT: "none_MT_rules C (rm_MT_rules C p)"
apply (induct p)
apply (simp_all)
done
lemma rmnMT2: "none_MT_rules C p \<Longrightarrow> (rm_MT_rules C p) = p"
apply (induct p)
apply (simp_all)
done
lemma nMTcharn: "none_MT_rules C p = (\<forall> r \<in> set p. dom (C r) \<noteq> {})"
apply (induct p)
apply (simp_all)
done
lemma nMTeqSet: "set p = set s \<Longrightarrow> none_MT_rules C p = none_MT_rules C s"
apply (simp add: nMTcharn)
done
lemma notMTnMT: "\<lbrakk>a \<in> set p; none_MT_rules C p\<rbrakk> \<Longrightarrow> dom (C a) \<noteq> {}"
apply (simp add: nMTcharn)
done
lemma none_MT_rulesconc: "none_MT_rules C (a@[b]) \<Longrightarrow> none_MT_rules C a"
apply (induct a)
apply (simp_all)
done
lemma nMTtail: "none_MT_rules C p \<Longrightarrow> none_MT_rules C (tl p)"
apply (induct p)
apply (simp_all)
done
lemma not_MTimpnotMT[simp]: "not_MT C p \<Longrightarrow> p \<noteq> []"
apply (auto)
done
lemma SR3nMT: "\<not> not_MT C p \<Longrightarrow> rm_MT_rules C p = []"
apply (induct p)
apply (auto simp: if_splits)
done
lemma NMPcharn: "\<lbrakk>a \<in> set p; dom (C a) \<noteq> {}\<rbrakk> \<Longrightarrow> not_MT C p"
apply (induct p)
apply (auto simp: if_splits)
done
lemma NMPrm: "not_MT C p \<Longrightarrow> not_MT C (rm_MT_rules C p)"
apply (induct p)
apply (simp_all)
done
text{* Next, a few theorems about applied\_rule: *}
lemma mrconc: "applied_rule_rev C x p = Some a \<Longrightarrow> applied_rule_rev C x (b#p) = Some a"
proof (induct p rule: rev_induct)
case Nil show ?case using Nil
by (simp add: applied_rule_rev_def)
next
case (snoc xs x) show ?case using snoc
apply (simp add: applied_rule_rev_def if_splits)
by (metis option.inject)
qed
lemma mreq_end: "\<lbrakk>applied_rule_rev C x b = Some r; applied_rule_rev C x c = Some r\<rbrakk> \<Longrightarrow>
applied_rule_rev C x (a#b) = applied_rule_rev C x (a#c)"
by (simp add: mrconc)
lemma mrconcNone: "applied_rule_rev C x p = None \<Longrightarrow>
applied_rule_rev C x (b#p) = applied_rule_rev C x [b]"
proof (induct p rule: rev_induct)
case Nil show ?case
by (simp add: applied_rule_rev_def)
next
case (snoc ys y) show ?case using snoc
proof (cases "x \<in> dom (C ys)")
case True show ?thesis using True snoc
by (auto simp: applied_rule_rev_def)
next
case False show ?thesis using False snoc
by (auto simp: applied_rule_rev_def)
qed
qed
lemma mreq_endNone: "\<lbrakk>applied_rule_rev C x b = None; applied_rule_rev C x c = None\<rbrakk> \<Longrightarrow>
applied_rule_rev C x (a#b) = applied_rule_rev C x (a#c)"
by (metis mrconcNone)
lemma mreq_end2: "applied_rule_rev C x b = applied_rule_rev C x c \<Longrightarrow>
applied_rule_rev C x (a#b) = applied_rule_rev C x (a#c)"
apply (case_tac "applied_rule_rev C x b = None")
apply (auto intro: mreq_end mreq_endNone)
done
lemma mreq_end3: "applied_rule_rev C x p \<noteq> None \<Longrightarrow>
applied_rule_rev C x (b # p) = applied_rule_rev C x (p)"
by (auto simp: mrconc)
lemma mrNoneMT: "\<lbrakk>r \<in> set p; applied_rule_rev C x p = None\<rbrakk> \<Longrightarrow>
x \<notin> dom (C r)"
proof (induct p rule: rev_induct)
case Nil show ?case using Nil
by (simp add: applied_rule_rev_def)
next
case (snoc y ys) show ?case using snoc
proof (cases "r \<in> set ys")
case True show ?thesis using snoc True
by (simp add: applied_rule_rev_def split: split_if_asm)
next
case False show ?thesis using snoc False
by (simp add: applied_rule_rev_def split: split_if_asm)
qed
qed
section{* Distributivity of the Transformation. *}
text{*
The scenario is the following (can be applied iteratively):
\begin{itemize}
\item Two policies are combined using one of the parallel combinators
\item (e.g. P = P1 P2) (At least) one of the constituent policies has
\item a normalisation procedures, which as output produces a list of
\item policies that are semantically equivalent to the original policy if
\item combined from left to right using the override operator.
\end{itemize}
*}
text{*
The following function is crucial for the distribution. Its arguments are a policy, a list
of policies, a parallel combinator, and a range and a domain coercion function.
*}
fun prod_list :: "('\<alpha> \<mapsto>'\<beta>) \<Rightarrow> (('\<gamma> \<mapsto>'\<delta>) list) \<Rightarrow>
(('\<alpha> \<mapsto>'\<beta>) \<Rightarrow> ('\<gamma> \<mapsto>'\<delta>) \<Rightarrow> (('\<alpha> \<times> '\<gamma>) \<mapsto> ('\<beta> \<times> '\<delta>))) \<Rightarrow>
(('\<beta> \<times> '\<delta>) \<Rightarrow> 'y) \<Rightarrow> ('x \<Rightarrow> ('\<alpha> \<times> '\<gamma>)) \<Rightarrow>
(('x \<mapsto> 'y) list)" (infixr "\<Otimes>\<^sub>L" 54) where
"prod_list x (y#ys) par_comb ran_adapt dom_adapt =
((ran_adapt o_f ((par_comb x y) o dom_adapt))#(prod_list x ys par_comb ran_adapt dom_adapt))"
| "prod_list x [] par_comb ran_adapt dom_adapt = []"
text{*
An instance, as usual there are four of them.
*}
definition prod_2_list :: "[('\<alpha> \<mapsto>'\<beta>), (('\<gamma> \<mapsto>'\<delta>) list)] \<Rightarrow>
(('\<beta> \<times> '\<delta>) \<Rightarrow> 'y) \<Rightarrow> ('x \<Rightarrow> ('\<alpha> \<times> '\<gamma>)) \<Rightarrow>
(('x \<mapsto> 'y) list)" (infixr "\<Otimes>\<^sub>2\<^sub>L" 55) where
"x \<Otimes>\<^sub>2\<^sub>L y = (\<lambda> d r. (x \<Otimes>\<^sub>L y) (op \<Otimes>\<^sub>2) d r)"
lemma list2listNMT: "x \<noteq> [] \<Longrightarrow> map sem x \<noteq> []"
apply (case_tac x)
apply (simp_all)
done
lemma two_conc: "(prod_list x (y#ys) p r d) = ((r o_f ((p x y) o d))#(prod_list x ys p r d))"
by simp
text{*
The following two invariants establish if the law of distributivity holds for a combinator
and if an operator is strict regarding undefinedness.
*}
definition is_distr where
"is_distr p = (\<lambda> g f. (\<forall> N P1 P2. ((g o_f ((p N (P1 \<Oplus> P2)) o f)) =
((g o_f ((p N P1) o f)) \<Oplus> (g o_f ((p N P2) o f))))))"
definition is_strict where
"is_strict p = (\<lambda> r d. \<forall> P1. (r o_f (p P1 \<emptyset> \<circ> d)) = \<emptyset>)"
lemma is_distr_orD: "is_distr (op \<Otimes>\<^sub>\<or>\<^sub>D) d r"
apply (simp add: is_distr_def)
apply (rule allI)+
apply (rule distr_orD)
apply (simp)
done
lemma is_strict_orD: "is_strict (op \<Otimes>\<^sub>\<or>\<^sub>D) d r"
apply (simp add: is_strict_def)
apply (simp add: policy_range_comp_def)
done
lemma is_distr_2: "is_distr (op \<Otimes>\<^sub>2) d r"
apply (simp add: is_distr_def)
apply (rule allI)+
apply (rule distr_or2)
by simp
lemma is_strict_2: "is_strict (op \<Otimes>\<^sub>2) d r"
apply (simp only: is_strict_def)
apply simp
apply (simp add: policy_range_comp_def)
done
lemma domStart: "t \<in> dom p1 \<Longrightarrow> (p1 \<Oplus> p2) t = p1 t"
apply (simp add: map_add_dom_app_simps)
done
lemma notDom: "x \<in> dom A \<Longrightarrow> \<not> A x = None"
apply auto
done
text{*
The following theorems are crucial: they establish the correctness of the distribution.
*}
lemma Norm_Distr_1: "((r o_f (((op \<Otimes>\<^sub>1) P1 (list2policy P2)) o d)) x =
((list2policy ((P1 \<Otimes>\<^sub>L P2) (op \<Otimes>\<^sub>1) r d)) x))"
proof (induct P2)
case Nil show ?case
by (simp add: policy_range_comp_def list2policy_def)
next
case (Cons p ps) show ?case using Cons
proof (cases "x \<in> dom (r o_f ((P1 \<Otimes>\<^sub>1 p) \<circ> d))")
case True show ?thesis using True
by (auto simp: list2policy_def policy_range_comp_def prod_1_def
split: option.splits decision.splits prod.splits)
next
case False show ?thesis using Cons False
by (auto simp: list2policy_def policy_range_comp_def map_add_dom_app_simps(3) prod_1_def
split: option.splits decision.splits prod.splits)
qed
qed
lemma Norm_Distr_2: "((r o_f (((op \<Otimes>\<^sub>2) P1 (list2policy P2)) o d)) x =
((list2policy ((P1 \<Otimes>\<^sub>L P2) (op \<Otimes>\<^sub>2) r d)) x))"proof (induct P2)
case Nil show ?case
by (simp add: policy_range_comp_def list2policy_def)
next
case (Cons p ps) show ?case using Cons
proof (cases "x \<in> dom (r o_f ((P1 \<Otimes>\<^sub>2 p) \<circ> d))")
case True show ?thesis using True
by (auto simp: list2policy_def prod_2_def policy_range_comp_def
split: option.splits decision.splits prod.splits)
next
case False show ?thesis using Cons False
by (auto simp: policy_range_comp_def list2policy_def map_add_dom_app_simps(3) prod_2_def
split: option.splits decision.splits prod.splits)
qed
qed
lemma Norm_Distr_A: "((r o_f (((op \<Otimes>\<^sub>\<or>\<^sub>A) P1 (list2policy P2)) o d)) x =
((list2policy ((P1 \<Otimes>\<^sub>L P2) (op \<Otimes>\<^sub>\<or>\<^sub>A) r d)) x))"
proof (induct P2)
case Nil show ?case
by (simp add: policy_range_comp_def list2policy_def)
next
case (Cons p ps) show ?case using Cons
proof (cases "x \<in> dom (r o_f ((P1 \<Otimes>\<^sub>\<or>\<^sub>A p) \<circ> d))")
case True show ?thesis using True
by (auto simp: policy_range_comp_def list2policy_def prod_orA_def
split: option.splits decision.splits prod.splits)
next
case False show ?thesis using Cons False
by (auto simp: policy_range_comp_def list2policy_def map_add_dom_app_simps(3) prod_orA_def
split: option.splits decision.splits prod.splits)
qed
qed
lemma Norm_Distr_D: "((r o_f (((op \<Otimes>\<^sub>\<or>\<^sub>D) P1 (list2policy P2)) o d)) x =
((list2policy ((P1 \<Otimes>\<^sub>L P2) (op \<Otimes>\<^sub>\<or>\<^sub>D) r d)) x))"
proof (induct P2)
case Nil show ?case
by (simp add: policy_range_comp_def list2policy_def)
next
case (Cons p ps) show ?case using Cons
proof (cases "x \<in> dom (r o_f ((P1 \<Otimes>\<^sub>\<or>\<^sub>D p) \<circ> d))")
case True show ?thesis using True
by (auto simp: policy_range_comp_def list2policy_def prod_orD_def
split: option.splits decision.splits prod.splits)
next
case False show ?thesis using Cons False
by (auto simp: policy_range_comp_def list2policy_def map_add_dom_app_simps(3) prod_orD_def
split: option.splits decision.splits prod.splits)
qed
qed
text {* Some domain reasoning *}
lemma domSubsetDistr1: "dom A = UNIV \<Longrightarrow> dom ((\<lambda>(x, y). x) o_f (A \<Otimes>\<^sub>1 B) o (\<lambda> x. (x,x))) = dom B"
apply (rule set_eqI)
apply (rule iffI)
apply (auto simp: prod_1_def policy_range_comp_def dom_def
split: decision.splits option.splits prod.splits)
done
lemma domSubsetDistr2: "dom A = UNIV \<Longrightarrow> dom ((\<lambda>(x, y). x) o_f (A \<Otimes>\<^sub>2 B) o (\<lambda> x. (x,x))) = dom B"
apply (rule set_eqI)
apply (rule iffI)
apply (auto simp: prod_2_def policy_range_comp_def dom_def
split: decision.splits option.splits prod.splits)
done
lemma domSubsetDistrA: "dom A = UNIV \<Longrightarrow> dom ((\<lambda>(x, y). x) o_f (A \<Otimes>\<^sub>\<or>\<^sub>A B) o (\<lambda> x. (x,x))) = dom B"
apply (rule set_eqI)
apply (rule iffI)
apply (auto simp: prod_orA_def policy_range_comp_def dom_def
split: decision.splits option.splits prod.splits)
done
lemma domSubsetDistrD: "dom A = UNIV \<Longrightarrow> dom ((\<lambda>(x, y). x) o_f (A \<Otimes>\<^sub>\<or>\<^sub>D B) o (\<lambda> x. (x,x))) = dom B"
apply (rule set_eqI)
apply (rule iffI)
apply (auto simp: prod_orD_def policy_range_comp_def dom_def
split: decision.splits option.splits prod.splits)
done
end

157
NormalisationTestSpecification.thy Normal file
View File

@ -0,0 +1,157 @@
(*****************************************************************************
* HOL-TestGen --- theorem-prover based test case generation
* http://www.brucker.ch/projects/hol-testgen/
*
* This file is part of HOL-TestGen.
*
* Copyright (c) 2005-2012 ETH Zurich, Switzerland
* 2008-2014 Achim D. Brucker, Germany
* 2009-2014 Université Paris-Sud, France
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* * Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above
* copyright notice, this list of conditions and the following
* disclaimer in the documentation and/or other materials provided
* with the distribution.
*
* * Neither the name of the copyright holders nor the names of its
* contributors may be used to endorse or promote products derived
* from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
******************************************************************************)
(* $Id: NormalisationTestSpecification.thy 10879 2014-10-26 11:35:31Z brucker $ *)
header {* Policy Transformation for Testing *}
theory
NormalisationTestSpecification
imports
Normalisation
begin
text{*
This theory provides functions and theorems which are useful if one wants to test policy
which are transformed. Most exist in two versions: one where the domains of the rules
of the list (which is the result of a transformation) are pairwise disjoint, and one where
this applies not for the last rule in a list (which is usually a default rules).
The examples in the firewall case study provide a good documentation how these theories can
be applied.
*}
text{*
This invariant establishes that the domains of a list of rules are pairwise disjoint.
*}
fun disjDom where
"disjDom (x#xs) = ((\<forall>y\<in>(set xs). dom x \<inter> dom y = {}) \<and> disjDom xs)"
|"disjDom [] = True"
fun PUTList :: "('a \<mapsto> 'b) \<Rightarrow> 'a \<Rightarrow> ('a \<mapsto> 'b) list \<Rightarrow> bool"
where
"PUTList PUT x (p#ps) = ((x \<in> dom p \<longrightarrow> (PUT x = p x)) \<and> (PUTList PUT x ps))"
|"PUTList PUT x [] = True"
lemma distrPUTL1: "x \<in> dom P \<Longrightarrow> (list2policy PL) x = P x
\<Longrightarrow> (PUTList PUT x PL \<Longrightarrow> (PUT x = P x))"
apply (induct PL)
apply (auto simp: list2policy_def dom_def)
done
lemma PUTList_None: "x \<notin> dom (list2policy list) \<Longrightarrow> PUTList PUT x list"
apply (induct list)
apply (auto simp: list2policy_def dom_def)
done
lemma PUTList_DomMT:
"(\<forall>y\<in>set list. dom a \<inter> dom y = {}) \<Longrightarrow> x \<in> (dom a) \<Longrightarrow> x \<notin> dom (list2policy list)"
apply (induct list)
apply (auto simp: dom_def list2policy_def)
done
lemma distrPUTL2:
"x \<in> dom P \<Longrightarrow> (list2policy PL) x = P x \<Longrightarrow> disjDom PL \<Longrightarrow> (PUT x = P x) \<Longrightarrow> PUTList PUT x PL "
apply (induct PL)
apply (simp_all add: list2policy_def)
apply (auto)
apply (case_tac "x \<in> dom a")
apply (case_tac "list2policy PL x = P x")
apply (simp add: list2policy_def)
apply (rule PUTList_None)
apply (rule_tac a = a in PUTList_DomMT)
apply (simp_all add: list2policy_def dom_def)
done
lemma distrPUTL:
"\<lbrakk>x \<in> dom P; (list2policy PL) x = P x; disjDom PL\<rbrakk> \<Longrightarrow> (PUT x = P x) = PUTList PUT x PL "
apply (rule iffI)
apply (rule distrPUTL2)
apply (simp_all)
apply (rule_tac PL = PL in distrPUTL1)
apply (auto)
done
text{*
It makes sense to cater for the common special case where the normalisation returns a list
where the last element is a default-catch-all rule. It seems easier to cater for this globally,
rather than to require the normalisation procedures to do this.
*}
fun gatherDomain_aux where
"gatherDomain_aux (x#xs) = (dom x \<union> (gatherDomain_aux xs))"
|"gatherDomain_aux [] = {}"
definition gatherDomain where "gatherDomain p = (gatherDomain_aux (butlast p))"
definition PUTListGD where "PUTListGD PUT x p =
(((x \<notin> (gatherDomain p) \<and> x \<in> dom (last p)) \<longrightarrow> PUT x = (last p) x) \<and>
(PUTList PUT x (butlast p)))"
definition disjDomGD where "disjDomGD p = disjDom (butlast p)"
lemma distrPUTLG1: "\<lbrakk>x \<in> dom P; (list2policy PL) x = P x; PUTListGD PUT x PL\<rbrakk> \<Longrightarrow> PUT x = P x"
apply (induct PL)
apply (simp_all add: domIff PUTListGD_def disjDomGD_def gatherDomain_def list2policy_def)
apply (auto simp: dom_def domIff split: split_if_asm)
done
lemma distrPUTLG2:
"PL \<noteq> [] \<Longrightarrow> x \<in> dom P \<Longrightarrow> (list2policy (PL)) x = P x \<Longrightarrow> disjDomGD PL \<Longrightarrow>
(PUT x = P x) \<Longrightarrow> PUTListGD PUT x (PL)"
apply (simp add: PUTListGD_def disjDomGD_def gatherDomain_def list2policy_def)
apply (induct PL)
apply (auto)
apply (metis PUTList_DomMT PUTList_None domI)
done
lemma distrPUTLG:
"\<lbrakk>x \<in> dom P; (list2policy PL) x = P x; disjDomGD PL; PL \<noteq> []\<rbrakk> \<Longrightarrow>
(PUT x = P x) = PUTListGD PUT x PL "
apply (rule iffI)
apply (rule distrPUTLG2)
apply (simp_all)
apply (rule_tac PL = PL in distrPUTLG1)
apply (auto)
done
end

330
ParallelComposition.thy Normal file
View File

@ -0,0 +1,330 @@
(*****************************************************************************
* HOL-TestGen --- theorem-prover based test case generation
* http://www.brucker.ch/projects/hol-testgen/
*
* This file is part of HOL-TestGen.
*
* Copyright (c) 2005-2012 ETH Zurich, Switzerland
* 2008-2014 Achim D. Brucker, Germany
* 2009-2014 Université Paris-Sud, France
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* * Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above
* copyright notice, this list of conditions and the following
* disclaimer in the documentation and/or other materials provided
* with the distribution.
*
* * Neither the name of the copyright holders nor the names of its
* contributors may be used to endorse or promote products derived
* from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
******************************************************************************)
(* $Id: ParallelComposition.thy 10879 2014-10-26 11:35:31Z brucker $ *)
header{* Parallel Composition*}
theory
ParallelComposition
imports
ElementaryPolicies
begin
text{*
The following combinators are based on the idea that two policies are executed in parallel.
Since both input and the output can differ, we chose to pair them.
The new input pair will often contain repetitions, which can be reduced using the
domain-restriction and domain-reduction operators. Using additional range-modifying operators
such as $\nabla$, decide which result argument is chosen; this might be the first or the latter
or, in case that $\beta = \gamma$, and $\beta$ underlies a lattice structure, the supremum or
infimum of both, or, an arbitrary combination of them.
In any case, although we have strictly speaking a pairing of decisions and not a nesting of
them, we will apply the same notational conventions as for the latter, i.e. as for
flattening.
*}
section{* Parallel Combinators: Foundations *}
text {*
There are four possible semantics how the decision can be combined, thus there are four
parallel composition operators. For each of them, we prove several properties.
*}
definition prod_orA ::"['\<alpha>\<mapsto>'\<beta>, '\<gamma> \<mapsto>'\<delta>] \<Rightarrow> ('\<alpha>\<times>'\<gamma> \<mapsto> '\<beta>\<times>'\<delta>)" (infixr "\<Otimes>\<^sub>\<or>\<^sub>A" 55)
where "p1 \<Otimes>\<^sub>\<or>\<^sub>A p2 =
(\<lambda>(x,y). (case p1 x of
\<lfloor>allow d1\<rfloor> \<Rightarrow>(case p2 y of
\<lfloor>allow d2\<rfloor> \<Rightarrow> \<lfloor>allow(d1,d2)\<rfloor>
| \<lfloor>deny d2\<rfloor> \<Rightarrow> \<lfloor>allow(d1,d2)\<rfloor>
| \<bottom> \<Rightarrow> \<bottom>)
| \<lfloor>deny d1\<rfloor>\<Rightarrow>(case p2 y of
\<lfloor>allow d2\<rfloor> \<Rightarrow> \<lfloor>allow(d1,d2)\<rfloor>
| \<lfloor>deny d2\<rfloor> \<Rightarrow> \<lfloor>deny (d1,d2)\<rfloor>
| \<bottom> \<Rightarrow> \<bottom>)
| \<bottom> \<Rightarrow> \<bottom>))"
lemma prod_orA_mt[simp]:"p \<Otimes>\<^sub>\<or>\<^sub>A \<emptyset> = \<emptyset>"
apply (rule ext)
apply (simp add: prod_orA_def)
apply (auto)
apply (simp split: option.splits decision.splits)
done
lemma mt_prod_orA[simp]:"\<emptyset> \<Otimes>\<^sub>\<or>\<^sub>A p = \<emptyset>"
apply (rule ext)
apply (simp add: prod_orA_def)
done
lemma prod_orA_quasi_commute: "p2 \<Otimes>\<^sub>\<or>\<^sub>A p1 = (((\<lambda>(x,y). (y,x)) o_f (p1 \<Otimes>\<^sub>\<or>\<^sub>A p2))) o (\<lambda>(a,b).(b,a))"
apply (rule ext)
apply (simp add: prod_orA_def policy_range_comp_def o_def)
apply (auto)
apply (simp split: option.splits decision.splits)
done
definition prod_orD ::"['\<alpha> \<mapsto> '\<beta>, '\<gamma> \<mapsto> '\<delta>] \<Rightarrow> ('\<alpha> \<times> '\<gamma> \<mapsto> '\<beta> \<times> '\<delta> )" (infixr "\<Otimes>\<^sub>\<or>\<^sub>D" 55)
where "p1 \<Otimes>\<^sub>\<or>\<^sub>D p2 =
(\<lambda>(x,y). (case p1 x of
\<lfloor>allow d1\<rfloor> \<Rightarrow>(case p2 y of
\<lfloor>allow d2\<rfloor> \<Rightarrow> \<lfloor>allow(d1,d2)\<rfloor>
| \<lfloor>deny d2\<rfloor> \<Rightarrow> \<lfloor>deny(d1,d2)\<rfloor>
| \<bottom> \<Rightarrow> \<bottom>)
| \<lfloor>deny d1\<rfloor>\<Rightarrow>(case p2 y of
\<lfloor>allow d2\<rfloor> \<Rightarrow> \<lfloor>deny(d1,d2)\<rfloor>
| \<lfloor>deny d2\<rfloor> \<Rightarrow> \<lfloor>deny (d1,d2)\<rfloor>
| \<bottom> \<Rightarrow> \<bottom>)
| \<bottom> \<Rightarrow> \<bottom>))"
lemma prod_orD_mt[simp]:"p \<Otimes>\<^sub>\<or>\<^sub>D \<emptyset> = \<emptyset>"
apply (rule ext)
apply (simp add: prod_orD_def)
apply (auto)
apply (simp split: option.splits decision.splits)
done
lemma mt_prod_orD[simp]:"\<emptyset> \<Otimes>\<^sub>\<or>\<^sub>D p = \<emptyset>"
apply (rule ext)
apply (simp add: prod_orD_def)
done
lemma prod_orD_quasi_commute: "p2 \<Otimes>\<^sub>\<or>\<^sub>D p1 = (((\<lambda>(x,y). (y,x)) o_f (p1 \<Otimes>\<^sub>\<or>\<^sub>D p2))) o (\<lambda>(a,b).(b,a))"
apply (rule ext)
apply (simp add: prod_orD_def policy_range_comp_def o_def)
apply (auto)
apply (simp split: option.splits decision.splits)
done
text{*
The following two combinators are by definition non-commutative, but still strict.
*}
definition prod_1 :: "['\<alpha>\<mapsto>'\<beta>, '\<gamma> \<mapsto>'\<delta>] \<Rightarrow> ('\<alpha>\<times>'\<gamma> \<mapsto> '\<beta>\<times>'\<delta>)" (infixr "\<Otimes>\<^sub>1" 55)
where "p1 \<Otimes>\<^sub>1 p2 \<equiv>
(\<lambda>(x,y). (case p1 x of
\<lfloor>allow d1\<rfloor>\<Rightarrow>(case p2 y of
\<lfloor>allow d2\<rfloor> \<Rightarrow> \<lfloor>allow(d1,d2)\<rfloor>
| \<lfloor>deny d2\<rfloor> \<Rightarrow> \<lfloor>allow(d1,d2)\<rfloor>
| \<bottom> \<Rightarrow> \<bottom>)
| \<lfloor>deny d1\<rfloor> \<Rightarrow>(case p2 y of
\<lfloor>allow d2\<rfloor> \<Rightarrow> \<lfloor>deny(d1,d2)\<rfloor>
| \<lfloor>deny d2\<rfloor> \<Rightarrow> \<lfloor>deny(d1,d2)\<rfloor>
| \<bottom> \<Rightarrow> \<bottom>)
|\<bottom> \<Rightarrow> \<bottom>))"
lemma prod_1_mt[simp]:"p \<Otimes>\<^sub>1 \<emptyset> = \<emptyset>"
apply (rule ext)
apply (simp add: prod_1_def)
apply (auto)
apply (simp split: option.splits decision.splits)
done
lemma mt_prod_1[simp]:"\<emptyset> \<Otimes>\<^sub>1 p = \<emptyset>"
apply (rule ext)
apply (simp add: prod_1_def)
done
definition prod_2 :: "['\<alpha>\<mapsto>'\<beta>, '\<gamma> \<mapsto>'\<delta>] \<Rightarrow> ('\<alpha>\<times>'\<gamma> \<mapsto> '\<beta>\<times>'\<delta>)" (infixr "\<Otimes>\<^sub>2" 55)
where "p1 \<Otimes>\<^sub>2 p2 \<equiv>
(\<lambda>(x,y). (case p1 x of
\<lfloor>allow d1\<rfloor> \<Rightarrow>(case p2 y of
\<lfloor>allow d2\<rfloor> \<Rightarrow> \<lfloor>allow(d1,d2)\<rfloor>
| \<lfloor>deny d2\<rfloor> \<Rightarrow> \<lfloor>deny (d1,d2)\<rfloor>
| \<bottom> \<Rightarrow> \<bottom>)
| \<lfloor>deny d1\<rfloor>\<Rightarrow>(case p2 y of
\<lfloor>allow d2\<rfloor> \<Rightarrow> \<lfloor>allow(d1,d2)\<rfloor>
| \<lfloor>deny d2\<rfloor> \<Rightarrow> \<lfloor>deny (d1,d2)\<rfloor>
| \<bottom> \<Rightarrow> \<bottom>)
|\<bottom> \<Rightarrow>\<bottom>))"
lemma prod_2_mt[simp]:"p \<Otimes>\<^sub>2 \<emptyset> = \<emptyset>"
apply (rule ext)
apply (simp add: prod_2_def)
apply (auto)
apply (simp split: option.splits decision.splits)
done
lemma mt_prod_2[simp]:"\<emptyset> \<Otimes>\<^sub>2 p = \<emptyset>"
apply (rule ext)
apply (simp add: prod_2_def)
done
definition prod_1_id ::"['\<alpha>\<mapsto>'\<beta>, '\<alpha>\<mapsto>'\<gamma>] \<Rightarrow> ('\<alpha> \<mapsto> '\<beta>\<times>'\<gamma>)" (infixr "\<Otimes>\<^sub>1\<^sub>I" 55)
where "p \<Otimes>\<^sub>1\<^sub>I q = (p \<Otimes>\<^sub>1 q) o (\<lambda>x. (x,x))"
lemma prod_1_id_mt[simp]:"p \<Otimes>\<^sub>1\<^sub>I \<emptyset> = \<emptyset>"
apply (rule ext)
apply (simp add: prod_1_id_def)
done
lemma mt_prod_1_id[simp]:"\<emptyset> \<Otimes>\<^sub>1\<^sub>I p = \<emptyset>"
apply (rule ext)
apply (simp add: prod_1_id_def prod_1_def)
done
definition prod_2_id ::"['\<alpha>\<mapsto>'\<beta>, '\<alpha>\<mapsto>'\<gamma>] \<Rightarrow> ('\<alpha> \<mapsto> '\<beta>\<times>'\<gamma>)" (infixr "\<Otimes>\<^sub>2\<^sub>I" 55)
where"p \<Otimes>\<^sub>2\<^sub>I q = (p \<Otimes>\<^sub>2 q) o (\<lambda>x. (x,x))"
lemma prod_2_id_mt[simp]:"p \<Otimes>\<^sub>2\<^sub>I \<emptyset> = \<emptyset>"
apply (rule ext)
apply (simp add: prod_2_id_def)
done
lemma mt_prod_2_id[simp]:"\<emptyset> \<Otimes>\<^sub>2\<^sub>I p = \<emptyset>"
apply (rule ext)
apply (simp add: prod_2_id_def prod_2_def)
done
section{* Combinators for Transition Policies *}
text {*
For constructing transition policies, two additional combinators are required: one combines
state transitions by pairing the states, the other works equivalently on general maps.
*}
definition parallel_map :: "('\<alpha> \<rightharpoonup> '\<beta>) \<Rightarrow> ('\<delta> \<rightharpoonup> '\<gamma>) \<Rightarrow>
('\<alpha> \<times> '\<delta> \<rightharpoonup> '\<beta> \<times> '\<gamma>)" (infixr "\<Otimes>\<^sub>M" 60)
where "p1 \<Otimes>\<^sub>M p2 = (\<lambda> (x,y). case p1 x of \<lfloor>d1\<rfloor> \<Rightarrow>
(case p2 y of \<lfloor>d2\<rfloor> \<Rightarrow> \<lfloor>(d1,d2)\<rfloor>
| \<bottom> \<Rightarrow> \<bottom>)
| \<bottom> \<Rightarrow> \<bottom>)"
definition parallel_st :: "('i \<times> '\<sigma> \<rightharpoonup> '\<sigma>) \<Rightarrow> ('i \<times> '\<sigma>' \<rightharpoonup> '\<sigma>') \<Rightarrow>
('i \<times> '\<sigma> \<times> '\<sigma>' \<rightharpoonup> '\<sigma> \<times> '\<sigma>')" (infixr "\<Otimes>\<^sub>S" 60)
where
"p1 \<Otimes>\<^sub>S p2 = (p1 \<Otimes>\<^sub>M p2) o (\<lambda> (a,b,c). ((a,b),a,c))"
section{* Range Splitting *}
text{*
The following combinator is a special case of both a parallel composition operator and a
range splitting operator. Its primary use case is when combining a policy with state transitions.
*}
definition comp_ran_split :: "[('\<alpha> \<rightharpoonup> '\<gamma>) \<times> ('\<alpha> \<rightharpoonup>'\<gamma>), 'd \<mapsto> '\<beta>] \<Rightarrow> ('d \<times> '\<alpha>) \<mapsto> ('\<beta> \<times> '\<gamma>)"
(infixr "\<Otimes>\<^sub>\<nabla>" 100)
where "P \<Otimes>\<^sub>\<nabla> p \<equiv> \<lambda>x. case p (fst x) of
\<lfloor>allow y\<rfloor> \<Rightarrow> (case ((fst P) (snd x)) of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>z\<rfloor> \<Rightarrow> \<lfloor>allow (y,z)\<rfloor>)
| \<lfloor>deny y\<rfloor> \<Rightarrow> (case ((snd P) (snd x)) of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>z\<rfloor> \<Rightarrow> \<lfloor>deny (y,z)\<rfloor>)
| \<bottom> \<Rightarrow> \<bottom>"
text{* An alternative characterisation of the operator is as follows: *}
lemma comp_ran_split_charn:
"(f, g) \<Otimes>\<^sub>\<nabla> p = (
(((p \<triangleright> Allow)\<Otimes>\<^sub>\<or>\<^sub>A (A\<^sub>p f)) \<Oplus>
((p \<triangleright> Deny) \<Otimes>\<^sub>\<or>\<^sub>A (D\<^sub>p g))))"
apply (rule ext)
apply (simp add: comp_ran_split_def map_add_def o_def ran_restrict_def image_def
Allow_def Deny_def dom_restrict_def prod_orA_def
allow_pfun_def deny_pfun_def
split:option.splits decision.splits)
apply (auto)
done
section {* Distributivity of the parallel combinators *}
lemma distr_or1_a: "(F = F1 \<Oplus> F2) \<Longrightarrow> (((N \<Otimes>\<^sub>1 F) o f) =
(((N \<Otimes>\<^sub>1 F1) o f) \<Oplus> ((N \<Otimes>\<^sub>1 F2) o f))) "
apply (rule ext)
apply (simp add: prod_1_def map_add_def
split: decision.splits option.splits)
apply (case_tac "f x")
apply (simp_all add: prod_1_def map_add_def
split: decision.splits option.splits)
done
lemma distr_or1: "(F = F1 \<Oplus> F2) \<Longrightarrow> ((g o_f ((N \<Otimes>\<^sub>1 F) o f)) =
((g o_f ((N \<Otimes>\<^sub>1 F1) o f)) \<Oplus> (g o_f ((N \<Otimes>\<^sub>1 F2) o f)))) "
apply (rule ext)+
apply (simp add: prod_1_def map_add_def policy_range_comp_def
split: decision.splits option.splits)
apply (case_tac "f x")
apply (simp_all add: prod_1_def map_add_def
split: decision.splits option.splits)
done
lemma distr_or2_a: "(F = F1 \<Oplus> F2) \<Longrightarrow> (((N \<Otimes>\<^sub>2 F) o f) =
(((N \<Otimes>\<^sub>2 F1) o f) \<Oplus> ((N \<Otimes>\<^sub>2 F2) o f))) "
apply (rule ext)
apply (simp add: prod_2_id_def prod_2_def map_add_def
split: decision.splits option.splits)
apply (case_tac "f x")
apply (simp_all add: prod_2_def map_add_def
split: decision.splits option.splits)
done
lemma distr_or2: "(F = F1 \<Oplus> F2) \<Longrightarrow> ((r o_f ((N \<Otimes>\<^sub>2 F) o f)) =
((r o_f ((N \<Otimes>\<^sub>2 F1) o f)) \<Oplus> (r o_f ((N \<Otimes>\<^sub>2 F2) o f)))) "
apply (rule ext)
apply (simp add: prod_2_id_def prod_2_def map_add_def policy_range_comp_def
split: decision.splits option.splits)
apply (case_tac "f x")
apply (simp_all add: prod_2_def map_add_def
split: decision.splits option.splits)
done
lemma distr_orA: "(F = F1 \<Oplus> F2) \<Longrightarrow> ((g o_f ((N \<Otimes>\<^sub>\<or>\<^sub>A F) o f)) =
((g o_f ((N \<Otimes>\<^sub>\<or>\<^sub>A F1) o f)) \<Oplus> (g o_f ((N \<Otimes>\<^sub>\<or>\<^sub>A F2) o f)))) "
apply (rule ext)+
apply (simp add: prod_orA_def map_add_def policy_range_comp_def
split: decision.splits option.splits)
apply (case_tac "f x")
apply (simp_all add: map_add_def
split: decision.splits option.splits)
done
lemma distr_orD: "(F = F1 \<Oplus> F2) \<Longrightarrow> ((g o_f ((N \<Otimes>\<^sub>\<or>\<^sub>D F) o f)) =
((g o_f ((N \<Otimes>\<^sub>\<or>\<^sub>D F1) o f)) \<Oplus> (g o_f ((N \<Otimes>\<^sub>\<or>\<^sub>D F2) o f)))) "
apply (rule ext)+
apply (simp add: prod_orD_def map_add_def policy_range_comp_def
split: decision.splits option.splits)
apply (case_tac "f x")
apply (simp_all add: map_add_def
split: decision.splits option.splits)
done
lemma coerc_assoc: "(r o_f P) o d = r o_f (P o d)"
apply (simp add: policy_range_comp_def)
apply (rule ext)
apply (simp split: option.splits decision.splits)
done
lemmas ParallelDefs = prod_orA_def prod_orD_def prod_1_def prod_2_def parallel_map_def
parallel_st_def comp_ran_split_def
end

15
ROOT Normal file
View File

@ -0,0 +1,15 @@
chapter AFP
session "UPF" (AFP) = HOL +
description {* The Unified Policy Framework (UPF) *}
options [timeout=300]
theories
Monads
UPF
ServiceExample
document_files
"root.tex"
"root.bib"
"introduction.tex"
"conclusion.tex"
"example-intro.tex"

236
SeqComposition.thy Normal file
View File

@ -0,0 +1,236 @@
(*****************************************************************************
* HOL-TestGen --- theorem-prover based test case generation
* http://www.brucker.ch/projects/hol-testgen/
*
* This file is part of HOL-TestGen.
*
* Copyright (c) 2005-2012 ETH Zurich, Switzerland
* 2008-2014 Achim D. Brucker, Germany
* 2009-2014 Université Paris-Sud, France
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* * Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above
* copyright notice, this list of conditions and the following
* disclaimer in the documentation and/or other materials provided
* with the distribution.
*
* * Neither the name of the copyright holders nor the names of its
* contributors may be used to endorse or promote products derived
* from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
******************************************************************************)
(* $Id: SeqComposition.thy 10879 2014-10-26 11:35:31Z brucker $ *)
header{* Sequential Composition *}
theory
SeqComposition
imports
ElementaryPolicies
begin
text{*
Sequential composition is based on the idea that two policies are to be combined by applying
the second policy to the output of the first one. Again, there are four possibilities how the
decisions can be combined. *}
section {* Flattening *}
text{*
A key concept of sequential policy composition is the flattening of nested decisions. There are
four possibilities, and these possibilities will give the various flavours of policy composition.
*}
fun flat_orA :: "('\<alpha> decision) decision \<Rightarrow> ('\<alpha> decision)"
where "flat_orA(allow(allow y)) = allow y"
|"flat_orA(allow(deny y)) = allow y"
|"flat_orA(deny(allow y)) = allow y"
|"flat_orA(deny(deny y)) = deny y"
lemma flat_orA_deny[dest]:"flat_orA x = deny y \<Longrightarrow> x = deny(deny y)"
apply (case_tac "x")
apply (simp_all)
apply (case_tac "\<alpha>")
apply (simp_all)
apply (case_tac "\<alpha>")
apply (simp_all)
done
lemma flat_orA_allow[dest]: "flat_orA x = allow y \<Longrightarrow> x = allow(allow y)
\<or> x = allow(deny y)
\<or> x = deny(allow y)"
apply (case_tac "x")
apply (simp_all)
apply (case_tac "\<alpha>")
apply (simp_all)
apply (case_tac "\<alpha>")
apply (simp_all)
done
fun flat_orD :: "('\<alpha> decision) decision \<Rightarrow> ('\<alpha> decision)"
where "flat_orD(allow(allow y)) = allow y"
|"flat_orD(allow(deny y)) = deny y"
|"flat_orD(deny(allow y)) = deny y"
|"flat_orD(deny(deny y)) = deny y"
lemma flat_orD_allow[dest]: "flat_orD x = allow y \<Longrightarrow> x = allow(allow y)"
apply (case_tac "x")
apply (simp_all)
apply (case_tac "\<alpha>")
apply (simp_all)
apply (case_tac "\<alpha>")
apply (simp_all)
done
lemma flat_orD_deny[dest]: "flat_orD x = deny y \<Longrightarrow> x = deny(deny y)
\<or> x = allow(deny y)
\<or> x = deny(allow y)"
apply (case_tac "x")
apply (simp_all)
apply (case_tac "\<alpha>")
apply (simp_all)
apply (case_tac "\<alpha>")
apply (simp_all)
done
fun flat_1 :: "('\<alpha> decision) decision \<Rightarrow> ('\<alpha> decision)"
where "flat_1(allow(allow y)) = allow y"
|"flat_1(allow(deny y)) = allow y"
|"flat_1(deny(allow y)) = deny y"
|"flat_1(deny(deny y)) = deny y"
lemma flat_1_allow[dest]: "flat_1 x = allow y \<Longrightarrow> x = allow(allow y) \<or> x = allow(deny y)"
apply (case_tac "x")
apply (simp_all)
apply (case_tac "\<alpha>")
apply (simp_all)
apply (case_tac "\<alpha>")
apply (simp_all)
done
lemma flat_1_deny[dest]: "flat_1 x = deny y \<Longrightarrow> x = deny(deny y) \<or> x = deny(allow y)"
apply (case_tac "x")
apply (simp_all)
apply (case_tac "\<alpha>")
apply (simp_all)
apply (case_tac "\<alpha>")
apply (simp_all)
done
fun flat_2 :: "('\<alpha> decision) decision \<Rightarrow> ('\<alpha> decision)"
where "flat_2(allow(allow y)) = allow y"
|"flat_2(allow(deny y)) = deny y"
|"flat_2(deny(allow y)) = allow y"
|"flat_2(deny(deny y)) = deny y"
lemma flat_2_allow[dest]: "flat_2 x = allow y \<Longrightarrow> x = allow(allow y) \<or> x = deny(allow y)"
apply (case_tac "x")
apply (simp_all)
apply (case_tac "\<alpha>")
apply (simp_all)
apply (case_tac "\<alpha>")
apply (simp_all)
done
lemma flat_2_deny[dest]: "flat_2 x = deny y \<Longrightarrow> x = deny(deny y) \<or> x = allow(deny y)"
apply (case_tac "x")
apply (simp_all)
apply (case_tac "\<alpha>")
apply (simp_all)
apply (case_tac "\<alpha>")
apply (simp_all)
done
section{* Policy Composition *}
text{*
The following definition allows to compose two policies. Denies and allows are transferred.
*}
fun lift :: "('\<alpha> \<mapsto> '\<beta>) \<Rightarrow> ('\<alpha> decision \<mapsto>'\<beta> decision)"
where "lift f (deny s) = (case f s of
\<lfloor>y\<rfloor> \<Rightarrow> \<lfloor>deny y\<rfloor>
| \<bottom> \<Rightarrow> \<bottom>)"
| "lift f (allow s) = (case f s of
\<lfloor>y\<rfloor> \<Rightarrow> \<lfloor>allow y\<rfloor>
| \<bottom> \<Rightarrow> \<bottom>)"
lemma lift_mt [simp]: "lift \<emptyset> = \<emptyset>"
apply (rule ext)
apply (case_tac "x")
apply (simp_all)
done
text{*
Since policies are maps, we inherit a composition on them. However, this results in nestings
of decisions---which must be flattened. As we now that there are four different forms of
flattening, we have four different forms of policy composition: *}
definition
comp_orA :: "['\<beta>\<mapsto>'\<gamma>, '\<alpha>\<mapsto>'\<beta>] \<Rightarrow> '\<alpha>\<mapsto>'\<gamma>" (infixl "o'_orA" 55) where
"p2 o_orA p1 \<equiv> (map_option flat_orA) o (lift p2 o_m p1)"
notation (xsymbols)
comp_orA (infixl "\<circ>\<^sub>\<or>\<^sub>A" 55)
lemma comp_orA_mt[simp]:"p \<circ>\<^sub>\<or>\<^sub>A \<emptyset> = \<emptyset>"
by(simp add: comp_orA_def)
lemma mt_comp_orA[simp]:"\<emptyset> \<circ>\<^sub>\<or>\<^sub>A p = \<emptyset>"
by(simp add: comp_orA_def)
definition
comp_orD :: "['\<beta>\<mapsto>'\<gamma>, '\<alpha>\<mapsto>'\<beta>] \<Rightarrow> '\<alpha>\<mapsto>'\<gamma>" (infixl "o'_orD" 55) where
"p2 o_orD p1 \<equiv> (map_option flat_orD) o (lift p2 o_m p1)"
notation (xsymbols)
comp_orD (infixl "\<circ>\<^sub>orD" 55)
lemma comp_orD_mt[simp]:"p o_orD \<emptyset> = \<emptyset>"
by(simp add: comp_orD_def)
lemma mt_comp_orD[simp]:"\<emptyset> o_orD p = \<emptyset>"
by(simp add: comp_orD_def)
definition
comp_1 :: "['\<beta>\<mapsto>'\<gamma>, '\<alpha>\<mapsto>'\<beta>] \<Rightarrow> '\<alpha>\<mapsto>'\<gamma>" (infixl "o'_1" 55) where
"p2 o_1 p1 \<equiv> (map_option flat_1) o (lift p2 o_m p1)"
notation (xsymbols)
comp_1 (infixl "\<circ>\<^sub>1" 55)
lemma comp_1_mt[simp]:"p \<circ>\<^sub>1 \<emptyset> = \<emptyset>"
by(simp add: comp_1_def)
lemma mt_comp_1[simp]:"\<emptyset> \<circ>\<^sub>1 p = \<emptyset>"
by(simp add: comp_1_def)
definition
comp_2 :: "['\<beta>\<mapsto>'\<gamma>, '\<alpha>\<mapsto>'\<beta>] \<Rightarrow> '\<alpha>\<mapsto>'\<gamma>" (infixl "o'_2" 55) where
"p2 o_2 p1 \<equiv> (map_option flat_2) o (lift p2 o_m p1)"
notation (xsymbols)
comp_2 (infixl "\<circ>\<^sub>2" 55)
lemma comp_2_mt[simp]:"p \<circ>\<^sub>2 \<emptyset> = \<emptyset>"
by(simp add: comp_2_def)
lemma mt_comp_2[simp]:"\<emptyset> \<circ>\<^sub>2 p = \<emptyset>"
by(simp add: comp_2_def)
end

478
Service.thy Normal file
View File

@ -0,0 +1,478 @@
(*****************************************************************************
* HOL-TestGen --- theorem-prover based test case generation
* http://www.brucker.ch/projects/hol-testgen/
*
* This file is part of HOL-TestGen.
*
* Copyright (c) 2010-2012 ETH Zurich, Switzerland
* 2010-2014 Achim D. Brucker, Germany
* 2010-2014 Université Paris-Sud, France
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* * Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above
* copyright notice, this list of conditions and the following
* disclaimer in the documentation and/or other materials provided
* with the distribution.
*
* * Neither the name of the copyright holders nor the names of its
* contributors may be used to endorse or promote products derived
* from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
******************************************************************************)
(* $Id: Service.thy 10945 2014-11-21 12:50:43Z wolff $ *)
header {* Secure Service Specification *}
theory
Service
imports
UPF
begin
text {*
In this section, we model a simple Web service and its access control model
that allows the staff in a hospital to access health care records of patients.
*}
section{* Datatypes for Modelling Users and Roles*}
subsection {* Users *}
text{*
First, we introduce a type for users that we use to model that each
staff member has a unique id:
*}
type_synonym user = int (* Each NHS employee has a unique NHS_ID. *)
text {*
Similarly, each patient has a unique id:
*}
type_synonym patient = int (* Each patient gets a unique id *)
subsection {* Roles and Relationships*}
text{* In our example, we assume three different roles for members of the clinical staff: *}
datatype role = ClinicalPractitioner | Nurse | Clerical
text{*
We model treatment relationships (legitimate relationships) between staff and patients
(respectively, their health records. This access control model is inspired by our detailed
NHS model.
*}
type_synonym lr_id = int
type_synonym LR = "lr_id \<rightharpoonup> (user set)"
text{* The security context stores all the existing LRs. *}
type_synonym \<Sigma> = "patient \<rightharpoonup> LR"
text{* The user context stores the roles the users are in. *}
type_synonym \<upsilon> = "user \<rightharpoonup> role"
section {* Modelling Health Records and the Web Service API*}
subsection {* Health Records *}
text {* The content and the status of the entries of a health record *}
datatype data = dummyContent
datatype status = Open | Closed
type_synonym entry_id = int
type_synonym entry = "status \<times> user \<times> data"
type_synonym SCR = "(entry_id \<rightharpoonup> entry)"
type_synonym DB = "patient \<rightharpoonup> SCR"
subsection {* The Web Service API *}
text{* The operations provided by the service: *}
datatype Operation = createSCR user role patient
| appendEntry user role patient entry_id entry
| deleteEntry user role patient entry_id
| readEntry user role patient entry_id
| readSCR user role patient
| addLR user role patient lr_id "(user set)"
| removeLR user role patient lr_id
| changeStatus user role patient entry_id status
| deleteSCR user role patient
| editEntry user role patient entry_id entry
fun is_createSCR where
"is_createSCR (createSCR u r p) = True"
|"is_createSCR x = False"
fun is_appendEntry where
"is_appendEntry (appendEntry u r p e ei) = True"
|"is_appendEntry x = False"
fun is_deleteEntry where
"is_deleteEntry (deleteEntry u r p e_id) = True"
|"is_deleteEntry x = False"
fun is_readEntry where
"is_readEntry (readEntry u r p e) = True"
|"is_readEntry x = False"
fun is_readSCR where
"is_readSCR (readSCR u r p) = True"
|"is_readSCR x = False"
fun is_changeStatus where
"is_changeStatus (changeStatus u r p s ei) = True"
|"is_changeStatus x = False"
fun is_deleteSCR where
"is_deleteSCR (deleteSCR u r p) = True"
|"is_deleteSCR x = False"
fun is_addLR where
"is_addLR (addLR u r lrid lr us) = True"
|"is_addLR x = False"
fun is_removeLR where
"is_removeLR (removeLR u r p lr) = True"
|"is_removeLR x = False"
fun is_editEntry where
"is_editEntry (editEntry u r p e_id s) = True"
|"is_editEntry x = False"
fun SCROp :: "(Operation \<times> DB) \<rightharpoonup> SCR" where
"SCROp ((createSCR u r p), S) = S p"
|"SCROp ((appendEntry u r p ei e), S) = S p"
|"SCROp ((deleteEntry u r p e_id), S) = S p"
|"SCROp ((readEntry u r p e), S) = S p"
|"SCROp ((readSCR u r p), S) = S p"
|"SCROp ((changeStatus u r p s ei),S) = S p"
|"SCROp ((deleteSCR u r p),S) = S p"
|"SCROp ((editEntry u r p e_id s),S) = S p"
|"SCROp x = \<bottom>"
fun patientOfOp :: "Operation \<Rightarrow> patient" where
"patientOfOp (createSCR u r p) = p"
|"patientOfOp (appendEntry u r p e ei) = p"
|"patientOfOp (deleteEntry u r p e_id) = p"
|"patientOfOp (readEntry u r p e) = p"
|"patientOfOp (readSCR u r p) = p"
|"patientOfOp (changeStatus u r p s ei) = p"
|"patientOfOp (deleteSCR u r p) = p"
|"patientOfOp (addLR u r p lr ei) = p"
|"patientOfOp (removeLR u r p lr) = p"
|"patientOfOp (editEntry u r p e_id s) = p"
fun userOfOp :: "Operation \<Rightarrow> user" where
"userOfOp (createSCR u r p) = u"
|"userOfOp (appendEntry u r p e ei) = u"
|"userOfOp (deleteEntry u r p e_id) = u"
|"userOfOp (readEntry u r p e) = u"
|"userOfOp (readSCR u r p) = u"
|"userOfOp (changeStatus u r p s ei) = u"
|"userOfOp (deleteSCR u r p) = u"
|"userOfOp (editEntry u r p e_id s) = u"
|"userOfOp (addLR u r p lr ei) = u"
|"userOfOp (removeLR u r p lr) = u"
fun roleOfOp :: "Operation \<Rightarrow> role" where
"roleOfOp (createSCR u r p) = r"
|"roleOfOp (appendEntry u r p e ei) = r"
|"roleOfOp (deleteEntry u r p e_id) = r"
|"roleOfOp (readEntry u r p e) = r"
|"roleOfOp (readSCR u r p) = r"
|"roleOfOp (changeStatus u r p s ei) = r"
|"roleOfOp (deleteSCR u r p) = r"
|"roleOfOp (editEntry u r p e_id s) = r"
|"roleOfOp (addLR u r p lr ei) = r"
|"roleOfOp (removeLR u r p lr) = r"
fun contentOfOp :: "Operation \<Rightarrow> data" where
"contentOfOp (appendEntry u r p ei e) = (snd (snd e))"
|"contentOfOp (editEntry u r p ei e) = (snd (snd e))"
fun contentStatic :: "Operation \<Rightarrow> bool" where
"contentStatic (appendEntry u r p ei e) = ((snd (snd e)) = dummyContent)"
|"contentStatic (editEntry u r p ei e) = ((snd (snd e)) = dummyContent)"
|"contentStatic x = True"
fun allContentStatic where
"allContentStatic (x#xs) = (contentStatic x \<and> allContentStatic xs)"
|"allContentStatic [] = True"
section{* Modelling Access Control*}
text {*
In the following, we define a rather complex access control model for our
scenario that extends traditional role-based access control
(RBAC)~\cite{sandhu.ea:role-based:1996} with treatment relationships and sealed
envelopes. Sealed envelopes (see~\cite{bruegger:generation:2012} for details)
are a variant of break-the-glass access control (see~\cite{brucker.ea:extending:2009}
for a general motivation and explanation of break-the-glass access control).
*}
subsection {* Sealed Envelopes *}
type_synonym SEPolicy = "(Operation \<times> DB \<mapsto> unit) "
definition get_entry:: "DB \<Rightarrow> patient \<Rightarrow> entry_id \<Rightarrow> entry option" where
"get_entry S p e_id = (case S p of \<bottom> \<Rightarrow> \<bottom>
| \<lfloor>Scr\<rfloor> \<Rightarrow> Scr e_id)"
definition userHasAccess:: "user \<Rightarrow> entry \<Rightarrow> bool" where
"userHasAccess u e = ((fst e) = Open \<or> (fst (snd e) = u))"
definition readEntrySE :: SEPolicy where
"readEntrySE x = (case x of (readEntry u r p e_id,S) \<Rightarrow> (case get_entry S p e_id of
\<bottom> \<Rightarrow> \<bottom>
| \<lfloor>e\<rfloor> \<Rightarrow> (if (userHasAccess u e)
then \<lfloor>allow ()\<rfloor>
else \<lfloor>deny ()\<rfloor> ))
| x \<Rightarrow> \<bottom>)"
definition deleteEntrySE :: SEPolicy where
"deleteEntrySE x = (case x of (deleteEntry u r p e_id,S) \<Rightarrow> (case get_entry S p e_id of
\<bottom> \<Rightarrow> \<bottom>
| \<lfloor>e\<rfloor> \<Rightarrow> (if (userHasAccess u e)
then \<lfloor>allow ()\<rfloor>
else \<lfloor>deny ()\<rfloor>))
| x \<Rightarrow> \<bottom>)"
definition editEntrySE :: SEPolicy where
"editEntrySE x = (case x of (editEntry u r p e_id s,S) \<Rightarrow> (case get_entry S p e_id of
\<bottom> \<Rightarrow> \<bottom>
| \<lfloor>e\<rfloor> \<Rightarrow> (if (userHasAccess u e)
then \<lfloor>allow ()\<rfloor>
else \<lfloor>deny ()\<rfloor>))
| x \<Rightarrow> \<bottom>)"
definition SEPolicy :: SEPolicy where
"SEPolicy = editEntrySE \<Oplus> deleteEntrySE \<Oplus> readEntrySE \<Oplus> A\<^sub>U"
lemmas SEsimps = SEPolicy_def get_entry_def userHasAccess_def
editEntrySE_def deleteEntrySE_def readEntrySE_def
subsection {* Legitimate Relationships *}
type_synonym LRPolicy = "(Operation \<times> \<Sigma>, unit) policy"
fun hasLR:: "user \<Rightarrow> patient \<Rightarrow> \<Sigma> \<Rightarrow> bool" where
"hasLR u p \<Sigma> = (case \<Sigma> p of \<bottom> \<Rightarrow> False
| \<lfloor>lrs\<rfloor> \<Rightarrow> (\<exists>lr. lr\<in>(ran lrs) \<and> u \<in> lr))"
definition LRPolicy :: LRPolicy where
"LRPolicy = (\<lambda>(x,y). (if hasLR (userOfOp x) (patientOfOp x) y
then \<lfloor>allow ()\<rfloor>
else \<lfloor>deny ()\<rfloor>))"
definition createSCRPolicy :: LRPolicy where
"createSCRPolicy x = (if (is_createSCR (fst x))
then \<lfloor>allow ()\<rfloor>
else \<bottom>)"
definition addLRPolicy :: LRPolicy where
"addLRPolicy x = (if (is_addLR (fst x))
then \<lfloor>allow ()\<rfloor>
else \<bottom>)"
definition LR_Policy where "LR_Policy = createSCRPolicy \<Oplus> addLRPolicy \<Oplus> LRPolicy \<Oplus> A\<^sub>U"
lemmas LRsimps = LR_Policy_def createSCRPolicy_def addLRPolicy_def LRPolicy_def
type_synonym FunPolicy = "(Operation \<times> DB \<times> \<Sigma>,unit) policy"
fun createFunPolicy :: FunPolicy where
"createFunPolicy ((createSCR u r p),(D,S)) = (if p \<in> dom D
then \<lfloor>deny ()\<rfloor>
else \<lfloor>allow ()\<rfloor>)"
|"createFunPolicy x = \<bottom>"
fun addLRFunPolicy :: FunPolicy where
"addLRFunPolicy ((addLR u r p l us),(D,S)) = (if l \<in> dom S
then \<lfloor>deny ()\<rfloor>
else \<lfloor>allow ()\<rfloor>)"
|"addLRFunPolicy x = \<bottom>"
fun removeLRFunPolicy :: FunPolicy where
"removeLRFunPolicy ((removeLR u r p l),(D,S)) = (if l \<in> dom S
then \<lfloor>allow ()\<rfloor>
else \<lfloor>deny ()\<rfloor>)"
|"removeLRFunPolicy x = \<bottom>"
fun readSCRFunPolicy :: FunPolicy where
"readSCRFunPolicy ((readSCR u r p),(D,S)) = (if p \<in> dom D
then \<lfloor>allow ()\<rfloor>
else \<lfloor>deny ()\<rfloor>)"
|"readSCRFunPolicy x = \<bottom>"
fun deleteSCRFunPolicy :: FunPolicy where
"deleteSCRFunPolicy ((deleteSCR u r p),(D,S)) = (if p \<in> dom D
then \<lfloor>allow ()\<rfloor>
else \<lfloor>deny ()\<rfloor>)"
|"deleteSCRFunPolicy x = \<bottom>"
fun changeStatusFunPolicy :: FunPolicy where
"changeStatusFunPolicy (changeStatus u r p e s,(d,S)) =
(case d p of \<lfloor>x\<rfloor> \<Rightarrow> (if e \<in> dom x
then \<lfloor>allow ()\<rfloor>
else \<lfloor>deny ()\<rfloor>)
| _ \<Rightarrow> \<lfloor>deny ()\<rfloor>)"
|"changeStatusFunPolicy x = \<bottom>"
fun deleteEntryFunPolicy :: FunPolicy where
"deleteEntryFunPolicy (deleteEntry u r p e,(d,S)) =
(case d p of \<lfloor>x\<rfloor> \<Rightarrow> (if e \<in> dom x
then \<lfloor>allow ()\<rfloor>
else \<lfloor>deny ()\<rfloor>)
| _ \<Rightarrow> \<lfloor>deny ()\<rfloor>)"
|"deleteEntryFunPolicy x = \<bottom>"
fun readEntryFunPolicy :: FunPolicy where
"readEntryFunPolicy (readEntry u r p e,(d,S)) =
(case d p of \<lfloor>x\<rfloor> \<Rightarrow> (if e \<in> dom x
then \<lfloor>allow ()\<rfloor>
else \<lfloor>deny ()\<rfloor>)
| _ \<Rightarrow> \<lfloor>deny ()\<rfloor>)"
|"readEntryFunPolicy x = \<bottom>"
fun appendEntryFunPolicy :: FunPolicy where
"appendEntryFunPolicy (appendEntry u r p e ed,(d,S)) =
(case d p of \<lfloor>x\<rfloor> \<Rightarrow> (if e \<in> dom x
then \<lfloor>deny ()\<rfloor>
else \<lfloor>allow ()\<rfloor>)
| _ \<Rightarrow> \<lfloor>deny ()\<rfloor>)"
|"appendEntryFunPolicy x = \<bottom>"
fun editEntryFunPolicy :: FunPolicy where
"editEntryFunPolicy (editEntry u r p ei e,(d,S)) =
(case d p of \<lfloor>x\<rfloor> \<Rightarrow> (if ei \<in> dom x
then \<lfloor>allow ()\<rfloor>
else \<lfloor>deny ()\<rfloor>)
| _ \<Rightarrow> \<lfloor>deny ()\<rfloor>)"
|"editEntryFunPolicy x = \<bottom>"
definition FunPolicy where
"FunPolicy = editEntryFunPolicy \<Oplus> appendEntryFunPolicy \<Oplus>
readEntryFunPolicy \<Oplus> deleteEntryFunPolicy \<Oplus>
changeStatusFunPolicy \<Oplus> deleteSCRFunPolicy \<Oplus>
removeLRFunPolicy \<Oplus> readSCRFunPolicy \<Oplus>
addLRFunPolicy \<Oplus> createFunPolicy \<Oplus> A\<^sub>U"
subsection{* Modelling Core RBAC *}
type_synonym RBACPolicy = "Operation \<times> \<upsilon> \<mapsto> unit"
definition RBAC :: "(role \<times> Operation) set" where
"RBAC = {(r,f). r = Nurse \<and> is_readEntry f} \<union>
{(r,f). r = Nurse \<and> is_readSCR f} \<union>
{(r,f). r = ClinicalPractitioner \<and> is_appendEntry f} \<union>
{(r,f). r = ClinicalPractitioner \<and> is_deleteEntry f} \<union>
{(r,f). r = ClinicalPractitioner \<and> is_readEntry f} \<union>
{(r,f). r = ClinicalPractitioner \<and> is_readSCR f} \<union>
{(r,f). r = ClinicalPractitioner \<and> is_changeStatus f} \<union>
{(r,f). r = ClinicalPractitioner \<and> is_editEntry f} \<union>
{(r,f). r = Clerical \<and> is_createSCR f} \<union>
{(r,f). r = Clerical \<and> is_deleteSCR f} \<union>
{(r,f). r = Clerical \<and> is_addLR f} \<union>
{(r,f). r = Clerical \<and> is_removeLR f}"
definition RBACPolicy :: RBACPolicy where
"RBACPolicy = (\<lambda> (f,uc).
if ((roleOfOp f,f) \<in> RBAC \<and> \<lfloor>roleOfOp f\<rfloor> = uc (userOfOp f))
then \<lfloor>allow ()\<rfloor>
else \<lfloor>deny ()\<rfloor>)"
section {* The State Transitions and Output Function*}
subsection{* State Transition *}
fun OpSuccessDB :: "(Operation \<times> DB) \<rightharpoonup> DB" where
"OpSuccessDB (createSCR u r p,S) = (case S p of \<bottom> \<Rightarrow> \<lfloor>S(p\<mapsto>\<emptyset>)\<rfloor>
| \<lfloor>x\<rfloor> \<Rightarrow> \<lfloor>S\<rfloor>)"
|"OpSuccessDB ((appendEntry u r p ei e),S) =
(case S p of \<bottom> \<Rightarrow> \<lfloor>S\<rfloor>
| \<lfloor>x\<rfloor> \<Rightarrow> ((if ei \<in> (dom x)
then \<lfloor>S\<rfloor>
else \<lfloor>S(p \<mapsto> x(ei\<mapsto>e))\<rfloor>)))"
|"OpSuccessDB ((deleteSCR u r p),S) = (Some (S(p:=\<bottom>)))"
|"OpSuccessDB ((deleteEntry u r p ei),S) =
(case S p of \<bottom> \<Rightarrow> \<lfloor>S\<rfloor>
| \<lfloor>x\<rfloor> \<Rightarrow> Some (S(p\<mapsto>(x(ei:=\<bottom>)))))"
|"OpSuccessDB ((changeStatus u r p ei s),S) =
(case S p of \<bottom> \<Rightarrow> \<lfloor>S\<rfloor>
| \<lfloor>x\<rfloor> \<Rightarrow> (case x ei of
\<lfloor>e\<rfloor> \<Rightarrow> \<lfloor>S(p \<mapsto> x(ei\<mapsto>(s,snd e)))\<rfloor>
| \<bottom> \<Rightarrow> \<lfloor>S\<rfloor>))"
|"OpSuccessDB ((editEntry u r p ei e),S) =
(case S p of \<bottom> \<Rightarrow>\<lfloor>S\<rfloor>
| \<lfloor>x\<rfloor> \<Rightarrow> (case x ei of
\<lfloor>e\<rfloor> \<Rightarrow> \<lfloor>S(p\<mapsto>(x(ei\<mapsto>(e))))\<rfloor>
| \<bottom> \<Rightarrow> \<lfloor>S\<rfloor>))"
|"OpSuccessDB (x,S) = \<lfloor>S\<rfloor>"
fun OpSuccessSigma :: "(Operation \<times> \<Sigma>) \<rightharpoonup> \<Sigma>" where
"OpSuccessSigma (addLR u r p lr_id us,S) =
(case S p of \<lfloor>lrs\<rfloor> \<Rightarrow> (case (lrs lr_id) of
\<bottom> \<Rightarrow> \<lfloor>S(p\<mapsto>(lrs(lr_id\<mapsto>us)))\<rfloor>
| \<lfloor>x\<rfloor> \<Rightarrow> \<lfloor>S\<rfloor>)
| \<bottom> \<Rightarrow> \<lfloor>S(p\<mapsto>(empty(lr_id\<mapsto>us)))\<rfloor>)"
|"OpSuccessSigma (removeLR u r p lr_id,S) =
(case S p of Some lrs \<Rightarrow> \<lfloor>S(p\<mapsto>(lrs(lr_id:=\<bottom>)))\<rfloor>
| \<bottom> \<Rightarrow> \<lfloor>S\<rfloor>)"
|"OpSuccessSigma (x,S) = \<lfloor>S\<rfloor>"
fun OpSuccessUC :: "(Operation \<times> \<upsilon>) \<rightharpoonup> \<upsilon>" where
"OpSuccessUC (f,u) = \<lfloor>u\<rfloor>"
subsection {* Output *}
type_synonym Output = unit
fun OpSuccessOutput :: "(Operation) \<rightharpoonup> Output" where
"OpSuccessOutput x = \<lfloor>()\<rfloor>"
fun OpFailOutput :: "Operation \<rightharpoonup> Output" where
"OpFailOutput x = \<lfloor>()\<rfloor>"
section {* Combine All Parts *}
definition SE_LR_Policy :: "(Operation \<times> DB \<times> \<Sigma>, unit) policy" where
"SE_LR_Policy = (\<lambda>(x,x). x) o\<^sub>f (SEPolicy \<Otimes>\<^sub>\<or>\<^sub>D LR_Policy) o (\<lambda>(a,b,c). ((a,b),a,c))"
definition SE_LR_FUN_Policy :: "(Operation \<times> DB \<times> \<Sigma>, unit) policy" where
"SE_LR_FUN_Policy = ((\<lambda>(x,x). x) o\<^sub>f (FunPolicy \<Otimes>\<^sub>\<or>\<^sub>D SE_LR_Policy) o (\<lambda>a. (a,a)))"
definition SE_LR_RBAC_Policy :: "(Operation \<times> DB \<times> \<Sigma> \<times> \<upsilon>, unit) policy" where
"SE_LR_RBAC_Policy = (\<lambda>(x,x). x)
o\<^sub>f (RBACPolicy \<Otimes>\<^sub>\<or>\<^sub>D SE_LR_FUN_Policy)
o (\<lambda>(a,b,c,d). ((a,d),(a,b,c)))"
definition ST_Allow :: "Operation \<times> DB \<times> \<Sigma> \<times> \<upsilon> \<rightharpoonup> Output \<times> DB \<times> \<Sigma> \<times> \<upsilon>"
where "ST_Allow = ((OpSuccessOutput \<Otimes>\<^sub>M (OpSuccessDB \<Otimes>\<^sub>S OpSuccessSigma \<Otimes>\<^sub>S OpSuccessUC))
o ( (\<lambda>(a,b,c). ((a),(a,b,c)))))"
definition ST_Deny :: "Operation \<times> DB \<times> \<Sigma> \<times> \<upsilon> \<rightharpoonup> Output \<times> DB \<times> \<Sigma> \<times> \<upsilon>"
where "ST_Deny = (\<lambda> (ope,sp,si,uc). Some ((), sp,si,uc))"
definition SE_LR_RBAC_ST_Policy :: "Operation \<times> DB \<times> \<Sigma> \<times> \<upsilon> \<mapsto> Output \<times> DB \<times> \<Sigma> \<times> \<upsilon>"
where "SE_LR_RBAC_ST_Policy = ((\<lambda> (x,y).y)
o\<^sub>f ((ST_Allow,ST_Deny) \<Otimes>\<^sub>\<nabla> SE_LR_RBAC_Policy)
o (\<lambda>x.(x,x)))"
definition PolMon :: "Operation \<Rightarrow> (Output decision,DB \<times> \<Sigma> \<times> \<upsilon>) MON\<^sub>S\<^sub>E"
where "PolMon = (policy2MON SE_LR_RBAC_ST_Policy)"
end

135
ServiceExample.thy Normal file
View File

@ -0,0 +1,135 @@
(*****************************************************************************
* HOL-TestGen --- theorem-prover based test case generation
* http://www.brucker.ch/projects/hol-testgen/
*
* This file is part of HOL-TestGen.
*
* Copyright (c) 2010-2012 ETH Zurich, Switzerland
* 2010-2014 Achim D. Brucker, Germany
* 2010-2014 Université Paris-Sud, France
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* * Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above
* copyright notice, this list of conditions and the following
* disclaimer in the documentation and/or other materials provided
* with the distribution.
*
* * Neither the name of the copyright holders nor the names of its
* contributors may be used to endorse or promote products derived
* from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
******************************************************************************)
(* $Id: ServiceExample.thy 10954 2014-11-24 12:43:29Z wolff $ *)
header {* Instantiating Our Secure Service Example *}
theory
ServiceExample
imports
Service
begin
text {*
In the following, we briefly present an instantiations of our secure service example
from the last section. We assume three different members of the health care staff and
two patients:
*}
section {* Access Control Configuration *}
definition alice :: user where "alice = 1"
definition bob :: user where "bob = 2"
definition charlie :: user where "charlie = 3"
definition patient1 :: patient where "patient1 = 5"
definition patient2 :: patient where "patient2 = 6"
definition UC0 :: \<upsilon> where
"UC0 = empty(alice\<mapsto>Nurse)(bob\<mapsto>ClinicalPractitioner)(charlie\<mapsto>Clerical)"
definition entry1 :: entry where
"entry1 = (Open,alice, dummyContent)"
definition entry2 :: entry where
"entry2 = (Closed,bob, dummyContent)"
definition entry3 :: entry where
"entry3 = (Closed,alice, dummyContent)"
definition SCR1 :: SCR where
"SCR1 = (Map.empty(1\<mapsto>entry1))"
definition SCR2 :: SCR where
"SCR2 = (Map.empty)"
definition Spine0 :: DB where
"Spine0 = empty(patient1\<mapsto>SCR1)(patient2\<mapsto>SCR2)"
definition LR1 :: LR where
"LR1 =(empty(1\<mapsto>{alice}))"
definition \<Sigma>0 :: \<Sigma> where
"\<Sigma>0 = (empty(patient1\<mapsto>LR1))"
section {* The Initial System State *}
definition \<sigma>0 :: "DB \<times> \<Sigma>\<times>\<upsilon>" where
"\<sigma>0 = (Spine0,\<Sigma>0,UC0)"
section{* Basic Properties *}
lemma [simp]: "(case a of allow d \<Rightarrow> \<lfloor>X\<rfloor> | deny d2 \<Rightarrow> \<lfloor>Y\<rfloor>) = \<bottom> \<Longrightarrow> False"
by (case_tac a,simp_all)
lemma [cong,simp]:
"((if hasLR urp1_alice 1 \<Sigma>0 then \<lfloor>allow ()\<rfloor> else \<lfloor>deny ()\<rfloor>) = \<bottom>) = False"
by (simp)
lemmas MonSimps = valid_SE_def unit_SE_def bind_SE_def
lemmas Psplits = option.splits unit.splits prod.splits decision.splits
lemmas PolSimps = valid_SE_def unit_SE_def bind_SE_def if_splits policy2MON_def
SE_LR_RBAC_ST_Policy_def map_add_def id_def LRsimps prod_2_def RBACPolicy_def
SE_LR_Policy_def SEPolicy_def RBAC_def deleteEntrySE_def editEntrySE_def
readEntrySE_def \<sigma>0_def \<Sigma>0_def UC0_def patient1_def patient2_def LR1_def
alice_def bob_def charlie_def get_entry_def SE_LR_RBAC_Policy_def Allow_def
Deny_def dom_restrict_def policy_range_comp_def prod_orA_def prod_orD_def
ST_Allow_def ST_Deny_def Spine0_def SCR1_def SCR2_def entry1_def entry2_def
entry3_def FunPolicy_def SE_LR_FUN_Policy_def o_def image_def UPFDefs
lemma "SE_LR_RBAC_Policy ((createSCR alice Clerical patient1),\<sigma>0)= Some (deny ())"
by (simp add: PolSimps)
lemma exBool[simp]: "\<exists>a\<Colon>bool. a" by auto
lemma deny_allow[simp]: " \<lfloor>deny ()\<rfloor> \<notin> Some ` range allow" by auto
lemma allow_deny[simp]: " \<lfloor>allow ()\<rfloor> \<notin> Some ` range deny" by auto
text{* Policy as monad. Alice using her first urp can read the SCR of patient1. *}
lemma
"(\<sigma>0 \<Turnstile> (os \<leftarrow> mbind [(createSCR alice Clerical patient1)] (PolMon);
(return (os = [(deny (Out) )]))))"
by (simp add: PolMon_def MonSimps PolSimps)
text{* Presenting her other urp, she is not allowed to read it. *}
lemma "SE_LR_RBAC_Policy ((appendEntry alice Clerical patient1 ei d),\<sigma>0)= \<lfloor>deny ()\<rfloor>"
by (simp add: PolSimps)
end

59
UPF.thy Normal file
View File

@ -0,0 +1,59 @@
(*****************************************************************************
* HOL-TestGen --- theorem-prover based test case generation
* http://www.brucker.ch/projects/hol-testgen/
*
* UPF
* This file is part of HOL-TestGen.
*
* Copyright (c) 2005-2012 ETH Zurich, Switzerland
* 2008-2014 Achim D. Brucker, Germany
* 2009-2014 Université Paris-Sud, France
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* * Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above
* copyright notice, this list of conditions and the following
* disclaimer in the documentation and/or other materials provided
* with the distribution.
*
* * Neither the name of the copyright holders nor the names of its
* contributors may be used to endorse or promote products derived
* from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
******************************************************************************)
(* $Id: UPF.thy 10879 2014-10-26 11:35:31Z brucker $ *)
header {* Putting Everything Together: UPF *}
theory
UPF
imports
Normalisation
NormalisationTestSpecification
Analysis
begin
text{*
This is the top-level theory for the Unified Policy Framework (UPF) and, thus,
builds the base theory for using UPF. For the moment, we only define a set of
lemmas for all core UPF definitions that is useful for using UPF:
*}
lemmas UPFDefs = UPFCoreDefs ParallelDefs ElementaryPoliciesDefs
end

400
UPFCore.thy Normal file
View File

@ -0,0 +1,400 @@
(*****************************************************************************
* HOL-TestGen --- theorem-prover based test case generation
* http://www.brucker.ch/projects/hol-testgen/
*
* UPF
* This file is part of HOL-TestGen.
*
* Copyright (c) 2005-2012 ETH Zurich, Switzerland
* 2008-2014 Achim D. Brucker, Germany
* 2009-2014 Université Paris-Sud, France
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* * Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above
* copyright notice, this list of conditions and the following
* disclaimer in the documentation and/or other materials provided
* with the distribution.
*
* * Neither the name of the copyright holders nor the names of its
* contributors may be used to endorse or promote products derived
* from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
******************************************************************************)
(* $Id: UPFCore.thy 10951 2014-11-21 21:54:46Z wolff $ *)
header{* The Core of the Unified Policy Framework (UPF) *}
theory
UPFCore
imports
Monads
begin
section{* Foundation *}
text{*
The purpose of this theory is to formalize a somewhat non-standard view
on the fundamental concept of a security policy which is worth outlining.
This view has arisen from prior experience in the modelling of network
(firewall) policies. Instead of regarding policies as relations on resources,
sets of permissions, etc., we emphasise the view that a policy is a policy
decision function that grants or denies access to resources, permissions, etc.
In other words, we model the concrete function that implements the policy
decision point in a system, and which represents a "wrapper" around the
business logic. An advantage of this view is that it is compatible
with many different policy models, enabling a uniform modelling framework to be
defined. Furthermore, this function is typically a large cascade of nested
conditionals, using conditions referring to an internal state and security
contexts of the system or a user. This cascade of conditionals can easily be
decomposed into a set of test cases similar to transformations used for binary
decision diagrams (BDD), and motivate equivalence class testing for unit test and
sequence test scenarios. From the modelling perspective, using \HOL as
its input language, we will consequently use the expressive power of its
underlying functional programming language, including the possibility to
define higher-order combinators.
In more detail, we model policies as partial functions based on input
data $\alpha$ (arguments, system state, security context, ...) to output
data $\beta$:
*}
datatype '\<alpha> decision = allow '\<alpha> | deny '\<alpha>
type_synonym ('\<alpha>,'\<beta>) policy = "'\<alpha> \<rightharpoonup> '\<beta> decision" (infixr "|->" 0)
text{*In the following, we introduce a number of shortcuts and alternative notations.
The type of policies is represented as: *}
translations (type) "'\<alpha> |-> '\<beta>" <= (type) "'\<alpha> \<rightharpoonup> '\<beta> decision"
type_notation (xsymbols) "policy" (infixr "\<mapsto>" 0)
text{* ... allowing the notation @{typ "'\<alpha> \<mapsto> '\<beta>"} for the policy type and the
alternative notations for @{term None} and @{term Some} of the \HOL library
@{typ "'\<alpha> option"} type:*}
notation "None" ("\<bottom>")
notation "Some" ("\<lfloor>_\<rfloor>" 80)
text{* Thus, the range of a policy may consist of @{term "\<lfloor>accept x\<rfloor>"} data,
of @{term "\<lfloor>deny x\<rfloor>"} data, as well as @{term "\<bottom>"} modeling the undefinedness
of a policy, i.e. a policy is considered as a partial function. Partial
functions are used since we describe elementary policies by partial system
behaviour, which are glued together by operators such as function override and
functional composition.
*}
text{* We define the two fundamental sets, the allow-set $Allow$ and the
deny-set $Deny$ (written $A$ and $D$ set for short), to characterize these
two main sets of the range of a policy.
*}
definition Allow :: "('\<alpha> decision) set"
where "Allow = range allow"
definition Deny :: "('\<alpha> decision) set"
where "Deny = range deny"
section{* Policy Constructors *}
text{*
Most elementary policy constructors are based on the
update operation @{thm [source] "Fun.fun_upd_def"} @{thm Fun.fun_upd_def}
and the maplet-notation @{term "a(x \<mapsto> y)"} used for @{term "a(x:=\<lfloor>y\<rfloor>)"}.
Furthermore, we add notation adopted to our problem domain: *}
nonterminal policylets and policylet
syntax
"_policylet1" :: "['a, 'a] => policylet" ("_ /+=/ _")
"_policylet2" :: "['a, 'a] => policylet" ("_ /-=/ _")
"" :: "policylet => policylets" ("_")
"_Maplets" :: "[policylet, policylets] => policylets" ("_,/ _")
"_Maplets" :: "[policylet, policylets] => policylets" ("_,/ _")
"_MapUpd" :: "['a |-> 'b, policylets] => 'a |-> 'b" ("_/'(_')" [900,0]900)
syntax (xsymbols)
"_policylet1" :: "['a, 'a] => policylet" ("_ /\<mapsto>\<^sub>+/ _")
"_policylet2" :: "['a, 'a] => policylet" ("_ /\<mapsto>\<^sub>-/ _")
"_emptypolicy" :: "'a |-> 'b" ("\<emptyset>")
translations
"_MapUpd m (_Maplets xy ms)" \<rightleftharpoons> "_MapUpd (_MapUpd m xy) ms"
"_MapUpd m (_policylet1 x y)" \<rightleftharpoons> "m(x := CONST Some (CONST allow y))"
"_MapUpd m (_policylet2 x y)" \<rightleftharpoons> "m(x := CONST Some (CONST deny y))"
"\<emptyset>" \<rightleftharpoons> "CONST empty"
text{* Here are some lemmas essentially showing syntactic equivalences: *}
lemma test: "empty(x+=a, y-= b) = \<emptyset>(x \<mapsto>\<^sub>+ a, y \<mapsto>\<^sub>- b)" by simp
lemma test2: "p(x\<mapsto>\<^sub>+a,x\<mapsto>\<^sub>-b) = p(x\<mapsto>\<^sub>-b)" by simp
text{*
We inherit a fairly rich theory on policy updates from Map here. Some examples are:
*}
lemma pol_upd_triv1: "t k = \<lfloor>allow x\<rfloor> \<Longrightarrow> t(k\<mapsto>\<^sub>+x) = t"
by (rule ext) simp
lemma pol_upd_triv2: "t k = \<lfloor>deny x\<rfloor> \<Longrightarrow> t(k\<mapsto>\<^sub>-x) = t"
by (rule ext) simp
lemma pol_upd_allow_nonempty: "t(k\<mapsto>\<^sub>+x) \<noteq> \<emptyset>"
by simp
lemma pol_upd_deny_nonempty: "t(k\<mapsto>\<^sub>-x) \<noteq> \<emptyset>"
by simp
lemma pol_upd_eqD1 : "m(a\<mapsto>\<^sub>+x) = n(a\<mapsto>\<^sub>+y) \<Longrightarrow> x = y"
by(auto dest: map_upd_eqD1)
lemma pol_upd_eqD2 : "m(a\<mapsto>\<^sub>-x) = n(a\<mapsto>\<^sub>-y) \<Longrightarrow> x = y"
by(auto dest: map_upd_eqD1)
lemma pol_upd_neq1 [simp]: "m(a\<mapsto>\<^sub>+x) \<noteq> n(a\<mapsto>\<^sub>-y)"
by(auto dest: map_upd_eqD1)
section{* Override Operators *}
text{*
Key operators for constructing policies are the override operators. There are four different
versions of them, with one of them being the override operator from the Map theory. As it is
common to compose policy rules in a ``left-to-right-first-fit''-manner, that one is taken as
default, defined by a syntax translation from the provided override operator from the Map
theory (which does it in reverse order).
*}
syntax
"_policyoverride" :: "['a \<mapsto> 'b, 'a \<mapsto> 'b] \<Rightarrow> 'a \<mapsto> 'b" (infixl "(+p/)" 100)
syntax (xsymbols)
"_policyoverride" :: "['a \<mapsto> 'b, 'a \<mapsto> 'b] \<Rightarrow> 'a \<mapsto> 'b" (infixl "\<Oplus>" 100)
translations
"p \<Oplus> q" \<rightleftharpoons> "q ++ p"
text{*
Some elementary facts inherited from Map are:
*}
lemma override_empty: "p \<Oplus> \<emptyset> = p"
by simp
lemma empty_override: "\<emptyset> \<Oplus> p = p"
by simp
lemma override_assoc: "p1 \<Oplus> (p2 \<Oplus> p3) = (p1 \<Oplus> p2) \<Oplus> p3"
by simp
text{*
The following two operators are variants of the standard override. For override\_A,
an allow of wins over a deny. For override\_D, the situation is dual.
*}
definition override_A :: "['\<alpha>\<mapsto>'\<beta>, '\<alpha>\<mapsto>'\<beta>] \<Rightarrow> '\<alpha>\<mapsto>'\<beta>" (infixl "++'_A" 100)
where "m2 ++_A m1 =
(\<lambda>x. (case m1 x of
\<lfloor>allow a\<rfloor> \<Rightarrow> \<lfloor>allow a\<rfloor>
| \<lfloor>deny a\<rfloor> \<Rightarrow> (case m2 x of \<lfloor>allow b\<rfloor> \<Rightarrow> \<lfloor>allow b\<rfloor>
| _ \<Rightarrow> \<lfloor>deny a\<rfloor>)
| \<bottom> \<Rightarrow> m2 x)
)"
syntax (xsymbols)
"_policyoverride_A" :: "['a \<mapsto> 'b, 'a \<mapsto> 'b] \<Rightarrow> 'a \<mapsto> 'b" (infixl "\<Oplus>\<^sub>A" 100)
translations
"p \<Oplus>\<^sub>A q" \<rightleftharpoons> "p ++_A q"
lemma override_A_empty[simp]: "p \<Oplus>\<^sub>A \<emptyset> = p"
by(simp add:override_A_def)
lemma empty_override_A[simp]: "\<emptyset> \<Oplus>\<^sub>A p = p"
apply (rule ext)
apply (simp add:override_A_def)
apply (case_tac "p x")
apply (simp_all)
apply (case_tac a)
apply (simp_all)
done
lemma override_A_assoc: "p1 \<Oplus>\<^sub>A (p2 \<Oplus>\<^sub>A p3) = (p1 \<Oplus>\<^sub>A p2) \<Oplus>\<^sub>A p3"
by (rule ext, simp add: override_A_def split: decision.splits option.splits)
definition override_D :: "['\<alpha>\<mapsto>'\<beta>, '\<alpha>\<mapsto>'\<beta>] \<Rightarrow> '\<alpha>\<mapsto>'\<beta>" (infixl "++'_D" 100)
where "m1 ++_D m2 =
(\<lambda>x. case m2 x of
\<lfloor>deny a\<rfloor> \<Rightarrow> \<lfloor>deny a\<rfloor>
| \<lfloor>allow a\<rfloor> \<Rightarrow> (case m1 x of \<lfloor>deny b\<rfloor> \<Rightarrow> \<lfloor>deny b\<rfloor>
| _ \<Rightarrow> \<lfloor>allow a\<rfloor>)
| \<bottom> \<Rightarrow> m1 x
)"
syntax (xsymbols)
"_policyoverride_D" :: "['a \<mapsto> 'b, 'a \<mapsto> 'b] \<Rightarrow> 'a \<mapsto> 'b" (infixl "\<Oplus>\<^sub>D" 100)
translations
"p \<Oplus>\<^sub>D q" \<rightleftharpoons> "p ++_D q"
lemma override_D_empty[simp]: "p \<Oplus>\<^sub>D \<emptyset> = p"
by(simp add:override_D_def)
lemma empty_override_D[simp]: "\<emptyset> \<Oplus>\<^sub>D p = p"
apply (rule ext)
apply (simp add:override_D_def)
apply (case_tac "p x", simp_all)
apply (case_tac a, simp_all)
done
lemma override_D_assoc: "p1 \<Oplus>\<^sub>D (p2 \<Oplus>\<^sub>D p3) = (p1 \<Oplus>\<^sub>D p2) \<Oplus>\<^sub>D p3"
apply (rule ext)
apply (simp add: override_D_def split: decision.splits option.splits)
done
section{* Coercion Operators *}
text{*
Often, especially when combining policies of different type, it is necessary to
adapt the input or output domain of a policy to a more refined context.
*}
text{*
An analogous for the range of a policy is defined as follows:
*}
definition policy_range_comp :: "['\<beta>\<Rightarrow>'\<gamma>, '\<alpha>\<mapsto>'\<beta>] \<Rightarrow> '\<alpha> \<mapsto>'\<gamma>" (infixl "o'_f" 55)
where
"f o_f p = (\<lambda>x. case p x of
\<lfloor>allow y\<rfloor> \<Rightarrow> \<lfloor>allow (f y)\<rfloor>
| \<lfloor>deny y\<rfloor> \<Rightarrow> \<lfloor>deny (f y)\<rfloor>
| \<bottom> \<Rightarrow> \<bottom>)"
syntax (xsymbols)
"_policy_range_comp" :: "['\<beta>\<Rightarrow>'\<gamma>, '\<alpha>\<mapsto>'\<beta>] \<Rightarrow> '\<alpha> \<mapsto>'\<gamma>" (infixl "o\<^sub>f" 55)
translations
"p o\<^sub>f q" \<rightleftharpoons> "p o_f q"
lemma policy_range_comp_strict : "f o\<^sub>f \<emptyset> = \<emptyset>"
apply (rule ext)
apply (simp add: policy_range_comp_def)
done
text{*
A generalized version is, where separate coercion functions are applied to the result
depending on the decision of the policy is as follows:
*}
definition range_split :: "[('\<beta>\<Rightarrow>'\<gamma>)\<times>('\<beta>\<Rightarrow>'\<gamma>),'\<alpha> \<mapsto> '\<beta>] \<Rightarrow> '\<alpha> \<mapsto> '\<gamma>"
(infixr "\<nabla>" 100)
where "(P) \<nabla> p = (\<lambda>x. case p x of
\<lfloor>allow y\<rfloor> \<Rightarrow> \<lfloor>allow ((fst P) y)\<rfloor>
| \<lfloor>deny y\<rfloor> \<Rightarrow> \<lfloor>deny ((snd P) y)\<rfloor>
| \<bottom> \<Rightarrow> \<bottom>)"
lemma range_split_strict[simp]: "P \<nabla> \<emptyset> = \<emptyset>"
apply (rule ext)
apply (simp add: range_split_def)
done
lemma range_split_charn:
"(f,g) \<nabla> p = (\<lambda>x. case p x of
\<lfloor>allow x\<rfloor> \<Rightarrow> \<lfloor>allow (f x)\<rfloor>
| \<lfloor>deny x\<rfloor> \<Rightarrow> \<lfloor>deny (g x)\<rfloor>
| \<bottom> \<Rightarrow> \<bottom>)"
apply (simp add: range_split_def)
apply (rule ext)
apply (case_tac "p x")
apply (simp_all)
apply (case_tac "a")
apply (simp_all)
done
text{*
The connection between these two becomes apparent if considering the following lemma:
*}
lemma range_split_vs_range_compose: "(f,f) \<nabla> p = f o\<^sub>f p"
by(simp add: range_split_charn policy_range_comp_def)
lemma range_split_id [simp]: "(id,id) \<nabla> p = p"
apply (rule ext)
apply (simp add: range_split_charn id_def)
apply (case_tac "p x")
apply (simp_all)
apply (case_tac "a")
apply (simp_all)
done
lemma range_split_bi_compose [simp]: "(f1,f2) \<nabla> (g1,g2) \<nabla> p = (f1 o g1,f2 o g2) \<nabla> p"
apply (rule ext)
apply (simp add: range_split_charn comp_def)
apply (case_tac "p x")
apply (simp_all)
apply (case_tac "a")
apply (simp_all)
done
text{*
The next three operators are rather exotic and in most cases not used.
*}
text {*
The following is a variant of range\_split, where the change in the decision depends
on the input instead of the output.
*}
definition dom_split2a :: "[('\<alpha> \<rightharpoonup> '\<gamma>) \<times> ('\<alpha> \<rightharpoonup>'\<gamma>),'\<alpha> \<mapsto> '\<beta>] \<Rightarrow> '\<alpha> \<mapsto> '\<gamma>" (infixr "\<Delta>a" 100)
where "P \<Delta>a p = (\<lambda>x. case p x of
\<lfloor>allow y\<rfloor> \<Rightarrow> \<lfloor>allow (the ((fst P) x))\<rfloor>
| \<lfloor>deny y\<rfloor> \<Rightarrow> \<lfloor>deny (the ((snd P) x))\<rfloor>
| \<bottom> \<Rightarrow> \<bottom>)"
definition dom_split2 :: "[('\<alpha> \<Rightarrow> '\<gamma>) \<times> ('\<alpha> \<Rightarrow>'\<gamma>),'\<alpha> \<mapsto> '\<beta>] \<Rightarrow> '\<alpha> \<mapsto> '\<gamma>" (infixr "\<Delta>" 100)
where "P \<Delta> p = (\<lambda>x. case p x of
\<lfloor>allow y\<rfloor> \<Rightarrow> \<lfloor>allow ((fst P) x)\<rfloor>
| \<lfloor>deny y\<rfloor> \<Rightarrow> \<lfloor>deny ((snd P) x)\<rfloor>
| \<bottom> \<Rightarrow> \<bottom>)"
definition range_split2 :: "[('\<alpha> \<Rightarrow> '\<gamma>) \<times> ('\<alpha> \<Rightarrow>'\<gamma>),'\<alpha> \<mapsto> '\<beta>] \<Rightarrow> '\<alpha> \<mapsto> ('\<beta> \<times>'\<gamma>)" (infixr "\<nabla>2" 100)
where "P \<nabla>2 p = (\<lambda>x. case p x of
\<lfloor>allow y\<rfloor> \<Rightarrow> \<lfloor>allow (y,(fst P) x)\<rfloor>
| \<lfloor>deny y\<rfloor> \<Rightarrow> \<lfloor>deny (y,(snd P) x)\<rfloor>
| \<bottom> \<Rightarrow> \<bottom>)"
text{*
The following operator is used for transition policies only: a transition policy is transformed
into a state-exception monad. Such a monad can for example be used for test case generation using
HOL-Testgen~\cite{brucker.ea:theorem-prover:2012}.
*}
definition policy2MON :: "('\<iota>\<times>'\<sigma> \<mapsto> 'o\<times>'\<sigma>) \<Rightarrow> ('\<iota> \<Rightarrow>('o decision,'\<sigma>) MON\<^sub>S\<^sub>E)"
where "policy2MON p = (\<lambda> \<iota> \<sigma>. case p (\<iota>,\<sigma>) of
\<lfloor>(allow (outs,\<sigma>'))\<rfloor> \<Rightarrow> \<lfloor>(allow outs, \<sigma>')\<rfloor>
| \<lfloor>(deny (outs,\<sigma>'))\<rfloor> \<Rightarrow> \<lfloor>(deny outs, \<sigma>')\<rfloor>
| \<bottom> \<Rightarrow> \<bottom>)"
lemmas UPFCoreDefs = Allow_def Deny_def override_A_def override_D_def policy_range_comp_def
range_split_def dom_split2_def map_add_def restrict_map_def
end

9
config Normal file
View File

@ -0,0 +1,9 @@
# -*- shell-script -*-
# Get email when automated build fails. May be empty.
# values: "email1 email2 .. emailn"
NOTIFY="adbrucker@0x5f.org wolff@lri.fr lukas.a.bruegger@gmail.com"
# Participate in frequent (nightly) build (only for small submissions)
# values: "yes" "no"
FREQUENT="no"

25
document/auto/root.el Normal file
View File

@ -0,0 +1,25 @@
(TeX-add-style-hook "root"
(lambda ()
(LaTeX-add-bibitems
"brucker.ea:formal-fw-testing:2014"
"brucker.ea:hol-testgen-fw:2013"
"brucker.ea:model-based:2011"
"brucker.ea:theorem-prover:2012"
"bruegger:generation:2012"
"barker:next:2009"
"sandhu.ea:role-based:1996"
"wainer.ea:dw-rbac:2007"
"sandhu.ea:nist:2000"
"samuel.ea:context-aware:2008"
"bertino.ea:trbac:2001"
"moyer.ea:generalized:2001"
"bell.ea:secure:1996"
"bell:looking:2005"
"oasis:xacml:2005"
"ferreira.ea:how:2009"
"ansi:rbac:2004"
"li.ea:critique:2007"
"ardagna.ea:access:2010"
"sandhu.ea:arbac97:1999"
"becker:information:2007")))

40
document/conclusion.tex Normal file
View File

@ -0,0 +1,40 @@
\chapter{Conclusion and Related Work}
\section{Related Work}
With \citet{barker:next:2009}, our UPF shares the observation
that a broad range of access control models can be reduced to a
surprisingly small number of primitives together with a set of
combinators or relations to build more complex policies. We also share
the vision that the semantics of access control models should be
formally defined. In contrast to \cite{barker:next:2009}, UPF
uses higher-order constructs and, more importantly, is geared towards
machine support for (formally) transforming policies and supporting
model-based test case generation approaches.
\section{Conclusion Future Work}
We have presented a uniform framework for modelling security
policies. This might be regarded as merely an interesting academic
exercise in the art of abstraction, especially given the fact that
underlying core concepts are logically equivalent, but presented
remarkably different from---apparently simple---security textbook
formalisations. However, we have successfully used the framework to
model fully the large and complex information governance policy of a
national health-care record system as described in the official
documents~\cite{brucker.ea:model-based:2011} as well as network
policies~\cite{brucker.ea:formal-fw-testing:2014}. Thus, we have shown
the framework being able to accommodate relatively conventional
RBAC~\cite{sandhu.ea:role-based:1996} mechanisms alongside less common
ones such as Legitimate Relationships. These security concepts are
modelled separately and combined into one global access control
mechanism. Moreover, we have shown the practical relevance of our
model by using it in our test generation system
\testgen~\cite{brucker.ea:theorem-prover:2012}, translating informal
security requirements into formal test specifications to be processed
to test sequences for a distributed system consisting of applications
accessing a central record storage system.
Besides applying our framework to other access control models, we plan
to develop specific test case generation algorithms. Such
domain-specific algorithms allow, by exploiting knowledge about the
structure of access control models, respectively the UPF, for a
deeper exploration of the test space. Finally, this results in an
improved test coverage.

10
document/example-intro.tex Normal file
View File

@ -0,0 +1,10 @@
In this chapter, we present a small example application of UPF for
modeling access control for a Web service that might be used in a
hospital. This scenario is motivated by our formalization of the NHS
system~\cite{bruegger:generation:2012,brucker.ea:model-based:2011}.
UPF was also successfully used for modeling network security policies
such as the ones enforced by
firewalls~\cite{bruegger:generation:2012,brucker.ea:formal-fw-testing:2014}. These
models were also used for generating test cases using
HOL-TestGen~\cite{brucker.ea:theorem-prover:2012}.

55
document/introduction.tex Normal file
View File

@ -0,0 +1,55 @@
\chapter{Introduction}
Access control, \ie, restricting the access to information or
resources, is an important pillar of today's information security
portfolio. Thus the large number of access control models
(\eg,~\cite{moyer.ea:generalized:2001,sandhu.ea:arbac97:1999,
sandhu.ea:nist:2000,ansi:rbac:2004,bell:looking:2005,bell.ea:secure:1996,oasis:xacml:2005,li.ea:critique:2007})
and variants thereof
(\eg,~\cite{ferreira.ea:how:2009,wainer.ea:dw-rbac:2007,ardagna.ea:access:2010,samuel.ea:context-aware:2008,bertino.ea:trbac:2001,ardagna.ea:access:2010,becker:information:2007})
is not surprising. On the one hand, this variety of specialized access
control models allows concise representation of access control
policies. On the other hand, the lack of a common foundations makes it
difficult to compare and analyze different access control models
formally.
We present formalization of the Unified Policy Framework
(UPF)~\cite{bruegger:generation:2012} that provides a formal semantics
for the core concepts of access control policiesb. It can serve as a
meta-model for a large set of well-known access control
policies and moreover, serve as a framework for analysis and test
generation tools addressing common ground in policy models.
Thus, UPF for comparing different access control models,
including a formal correctness proof of a specific embedding, for
example, implementing a role-based access control policy in terms of a
discretionary access enforcement architecture. Moreover, defining
well-known access control models by instantiating a unified policy
framework allows to re-use tools, such as test-case generators, that
are already provided for the unified policy framework. As the
instantiation of a unified policy framework may also define a
domain-specific (\ie, access control model specific) set of policy
combinators (syntax), such an approach still provides the usual
notations and thus a concise representation of access control
policies.
UPF was already successful used as a basis for large scale access
control policies in the health care
domain~\cite{brucker.ea:model-based:2011} as well as in the domain of
firewall and router
policies~\cite{brucker.ea:formal-fw-testing:2014}. In both domains,
the formal policy specifications served as basis for the generation,
using {HOL-TestGen}~\cite{brucker.ea:theorem-prover:2012}, of test
cases that can be used for validating the compliance of an
implementation to the formal model. UPF is based on the following four
principles:
\begin{enumerate}
\item policies are represented as \emph{functions} (rather than relations),
\item policy combination avoids conflicts by construction,
\item the decision type is three-valued (allow, deny, undefined),
\item the output type does not only contain the decision but also a
`slot' for arbitrary result data.
\end{enumerate}
UPF is related to the state-exception monad modeling failing computations;
in some cases our UPF model makes explicit use of this connection, although it
is not central. The used theory for state-exception monads can be found in the
appendix.

701
document/root.bib Normal file
View File

@ -0,0 +1,701 @@
@PREAMBLE{ {\providecommand{\ac}[1]{\textsc{#1}} }
# {\providecommand{\acs}[1]{\textsc{#1}} }
# {\providecommand{\acf}[1]{\textsc{#1}} }
# {\providecommand{\TAP}{T\kern-.1em\lower-.5ex\hbox{A}\kern-.1em P} }
# {\providecommand{\leanTAP}{\mbox{\sf lean\it\TAP}} }
# {\providecommand{\holz}{\textsc{hol-z}} }
# {\providecommand{\holocl}{\textsc{hol-ocl}} }
# {\providecommand{\isbn}{\textsc{isbn}} }
# {\providecommand{\Cpp}{C++} }
# {\providecommand{\Specsharp}{Spec\#} }
# {\providecommand{\doi}[1]{\href{http://dx.doi.org/#1}{doi:
{\urlstyle{rm}\nolinkurl{#1}}}}} }
@STRING{conf-sacmat="ACM symposium on access control models and technologies
(SACMAT)" }
@STRING{j-computer="Computer" }
@STRING{j-fac = "Formal Aspects of Computing (FAC)" }
@STRING{j-stvr = "Software Testing, Verification \& Reliability (STVR)" }
@STRING{j-tissec= "ACM Transactions on Information and System Security" }
@STRING{proc = "Proceedings of the " }
@STRING{pub-acm = {ACM Press} }
@STRING{pub-acm:adr={New York, NY USA} }
@STRING{pub-elsevier={Elsevier Science Publishers} }
@STRING{pub-ieee= {IEEE Computer Society} }
@STRING{pub-ieee:adr={Los Alamitos, CA, USA} }
@STRING{pub-springer={Springer-Verlag} }
@STRING{pub-wiley={John Wiley \& Sons} }
@STRING{s-lncs = "Lecture Notes in Computer Science" }
@Article{ brucker.ea:formal-fw-testing:2014,
abstract = {Firewalls are an important means to secure critical ICT
infrastructures. As configurable off-the-shelf prod\-ucts,
the effectiveness of a firewall crucially depends on both
the correctness of the implementation itself as well as the
correct configuration. While testing the implementation can
be done once by the manufacturer, the configuration needs
to be tested for each application individually. This is
particularly challenging as the configuration, implementing
a firewall policy, is inherently complex, hard to
understand, administrated by different stakeholders and
thus difficult to validate. This paper presents a formal
model of both stateless and stateful firewalls (packet
filters), including NAT, to which a specification-based
conformance test case gen\-eration approach is applied.
Furthermore, a verified optimisation technique for this
approach is presented: starting from a formal model for
stateless firewalls, a collection of semantics-preserving
policy transformation rules and an algorithm that optimizes
the specification with respect of the number of test cases
required for path coverage of the model are derived. We
extend an existing approach that integrates verification
and testing, that is, tests and proofs to support
conformance testing of network policies. The presented
approach is supported by a test framework that allows to
test actual firewalls using the test cases generated on the
basis of the formal model. Finally, a report on several
larger case studies is presented.},
address = {pub-wiley:adr},
author = {Achim D. Brucker and Lukas Br{\"u}gger and Burkhart Wolff},
doi = {10.1002/stvr.1544},
journal = {Software Testing, Verification \& Reliability (STVR)},
keywords = {model-based testing; conformance testing; security
testing; firewall; specification-based testing; testing
cloud infrastructure, transformation for testability;
HOL-TestGen; test and proof; security configuration
testing},
language = {USenglish},
pdf = {http://www.brucker.ch/bibliography/download/2014/brucker.ea-formal-fw-testing-2014.pdf}
,
publisher = {pub-wiley},
title = {Formal Firewall Conformance Testing: An Application of
Test and Proof Techniques},
url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-formal-fw-testing-2014}
,
year = {2014}
}
@InCollection{ brucker.ea:hol-testgen-fw:2013,
abstract = {The HOL-TestGen environment is conceived as a system for
modeling and semi-automated test generation with an
emphasis on expressive power and generality. However, its
underlying technical framework Isabelle/HOL supports the
customization as well as the development of highly
automated add-ons working in specific application
domains.\\\\In this paper, we present HOL-TestGen/fw, an
add-on for the test framework HOL-TestGen, that allows for
testing the conformance of firewall implementations to
high-level security policies. Based on generic theories
specifying a security-policy language, we developed
specific theories for network data and firewall policies.
On top of these firewall specific theories, we provide
mechanisms for policy transformations based on derived
rules and adapted code-generators producing test drivers.
Our empirical evaluations shows that HOL-TestGen/fw is a
competitive environment for testing firewalls or high-level
policies of local networks.},
address = {Heidelberg},
author = {Achim D. Brucker and Lukas Br{\"u}gger and Burkhart Wolff},
booktitle = {International Colloquium on Theoretical Aspects of
Computing (ICTAC)},
doi = {10.1007/978-3-642-39718-9_7},
editor = {Zhiming Liu and Jim Woodcock and Huibiao Zhu},
isbn = {978-3-642-39717-2},
keywords = {symbolic test case generations, black box testing, theorem
proving, network security, firewall testing, conformance
testing},
language = {USenglish},
location = {Shanghai},
number = {8049},
pages = {112--121},
pdf = {http://www.brucker.ch/bibliography/download/2013/brucker.ea-hol-testgen-fw-2013.pdf}
,
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
title = {{HOL-TestGen/FW:} An Environment for Specification-based
Firewall Conformance Testing},
url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-testgen-fw-2013}
,
year = {2013}
}
@InProceedings{ brucker.ea:model-based:2011,
abstract = {We present a generic modular policy modelling framework
and instantiate it with a substantial case study for
model-based testing of some key security mechanisms of
applications and services of the NPfIT. NPfIT, the National
Programme for IT, is a very large-scale development project
aiming to modernise the IT infrastructure of the NHS in
England. Consisting of heterogeneous and distributed
applications, it is an ideal target for model-based testing
techniques of a large system exhibiting critical security
features.\\\\We model the four information governance
principles, comprising a role-based access control model,
as well as policy rules governing the concepts of patient
consent, sealed envelopes and legitimate relationship. The
model is given in HOL and processed together with suitable
test specifications in the HOL-TestGen system, that
generates test sequences according to them. Particular
emphasis is put on the modular description of security
policies and their generic combination and its consequences
for model-based testing.},
address = {New York, NY, USA},
author = {Achim D. Brucker and Lukas Br{\"u}gger and Paul Kearney
and Burkhart Wolff},
booktitle = {ACM symposium on access control models and technologies
(SACMAT)},
copyright = {ACM},
copyrighturl = {http://dl.acm.org/authorize?431936},
doi = {10.1145/1998441.1998461},
isbn = {978-1-4503-0688-1},
language = {USenglish},
location = {Innsbruck, Austria},
pages = {133--142},
pdf = {http://www.brucker.ch/bibliography/download/2011/brucker.ea-model-based-2011.pdf}
,
publisher = {ACM Press},
title = {An Approach to Modular and Testable Security Models of
Real-world Health-care Applications},
url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-model-based-2011}
,
year = {2011}
}
@Article{ brucker.ea:theorem-prover:2012,
abstract = {HOL-TestGen is a specification and test case generation
environment extending the interactive theorem prover
Isabelle/HOL. As such, HOL-TestGen allows for an integrated
workflow supporting interactive theorem proving, test case
generation, and test data generation.\\\\The HOL-TestGen
method is two-staged: first, the original formula is
partitioned into test cases by transformation into a normal
form called test theorem. Second, the test cases are
analyzed for ground instances (the test data) satisfying
the constraints of the test cases. Particular emphasis is
put on the control of explicit test-hypotheses which can be
proven over concrete programs.\\\\Due to the generality of
the underlying framework, our system can be used for
black-box unit, sequence, reactive sequence and white-box
test scenarios. Although based on particularly clean
theoretical foundations, the system can be applied for
substantial case-studies.},
address = {Heidelberg},
author = {Achim D. Brucker and Burkhart Wolff},
doi = {10.1007/s00165-012-0222-y},
issn = {0934-5043},
journal = {Formal Aspects of Computing},
keywords = {test case generation, domain partitioning, test sequence,
theorem proving, HOL-TestGen},
language = {USenglish},
number = {5},
pages = {683--721},
pdf = {http://www.brucker.ch/bibliography/download/2012/brucker.ea-theorem-prover-2012.pdf}
,
publisher = {Springer-Verlag},
title = {On Theorem Prover-based Testing},
url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-theorem-prover-2012}
,
volume = {25},
year = {2013}
}
@PhDThesis{ bruegger:generation:2012,
author = {Lukas Br{\"u}gger},
title = {A Framework for Modelling and Testing of Security
Policies},
school = {ETH Zurich},
year = {2012},
categories = {holtestgen},
note = {ETH Dissertation No. 20513.},
public = yes,
pdf = {http://www.brucker.ch/bibliography/download/bruegger-generation-2012.pdf}
,
url = {http://www.brucker.ch/bibliography/abstract/bruegger-generation-2012}
}
@InProceedings{ barker:next:2009,
author = {Steve Barker},
title = {The next 700 access control models or a unifying
meta-model?},
booktitle = {Proceedings of the 14th ACM symposium on Access control
models and technologies},
series = {SACMAT '09},
year = 2009,
isbn = {978-1-60558-537-6},
location = {Stresa, Italy},
pages = {187--196},
numpages = 10,
doi = {10.1145/1542207.1542238},
acmid = 1542238,
publisher = pub-acm,
address = pub-acm:adr,
keywords = {access control models, access control policies},
abstract = {We address some fundamental questions, which were raised
by Atluri and Ferraiolo at SACMAT'08, on the prospects for
and benefits of a meta-model of access control. We
demonstrate that a meta-model for access control can be
defined and that multiple access control models can be
derived as special cases. An anticipated consequence of the
contribution that we describe is to encourage researchers
to adopt a meta-model view of access control rather than
them developing the next 700 particular instances of access
control models.}
}
@Article{ sandhu.ea:role-based:1996,
author = {Ravi S. Sandhu and Edward J. Coyne and Hal L. Feinstein
and Charles E. Youman},
title = {Role-Based Access Control Models},
journal = j-computer,
year = 1996,
volume = 29,
number = 2,
address = pub-ieee:adr,
publisher = pub-ieee,
pages = {38--47},
url = {http://ite.gmu.edu/list/journals/computer/pdf_ver/i94rbac(org).pdf}
,
abstract = {Abstract This article introduces a family of reference
models for rolebased acce ss control (RBAC) in which
permissions are associated with roles, and users are made
members of appropriate roles. This greatly simplifies
management of permiss ions. Roles are closely related to
the concept of user groups in access control. However, a
role brings together a set of users on one side and a set
of permiss ions on the other, whereas user groups are
typically defined as a set of users o nly.
The basic concepts of RBAC originated with early multi-user
computer systems. Th e resurgence of interest in RBAC has
been driven by the need for general-purpose customizable
facilities for RBAC and the need to manage the
administration of R BAC itself. As a consequence RBAC
facilities range from simple to complex. This article
describes a novel framework of reference models to
systematically addres s the diverse components of RBAC, and
their interactions.},
issn = {0018-9162},
keywords = {Computational linguistics; Computer control systems;
Computer simulation; Computer software; Data abstraction;
Database systems; Discretionary access control; Encoding
(symbols); Integration; Mandator access control; Role based
access control; Semantics; Software encoding; User
interfaces},
acknowledgement={none},
bibkey = {sandhu.ea:role-based:1996}
}
@Article{ wainer.ea:dw-rbac:2007,
author = {Jacques Wainer and Akhil Kumar and Paulo Barthelmess},
title = {DW-RBAC: A formal security model of delegation and
revocation in workflow systems},
journal = {Inf. Syst.},
year = 2007,
volume = 32,
number = 3,
pages = {365--384},
abstract = {One reason workflow systems have been criticized as being
inflexible is that they lack support for delegation. This
paper shows how delegation can be introduced in a workflow
system by extending the role-based access control (RBAC)
model. The current RBAC model is a security mechanism to
implement access control in organizations by allowing users
to be assigned to roles and privileges to be associated
with the roles. Thus, users can perform tasks based on the
privileges possessed by their own role or roles they
inherit by virtue of their organizational position.
However, there is no easy way to handle delegations within
this model. This paper tries to treat the issues
surrounding delegation in workflow systems in a
comprehensive way. We show how delegations can be
incorporated into the RBAC model in a simple and
straightforward manner. The new extended model is called
RBAC with delegation in a workflow context (DW-RBAC). It
allows for delegations to be specified from a user to
another user, and later revoked when the delegation is no
longer required. The implications of such specifications
and their subsequent revocations are examined. Several
formal definitions for assertion, acceptance, execution and
revocation are provided, and proofs are given for the
important properties of our delegation framework.},
issn = {0306-4379},
doi = {http://dx.doi.org/10.1016/j.is.2005.11.008},
publisher = pub-elsevier,
address = {Oxford, UK, UK},
tags = {ReadingList, SoKNOS},
clearance = {unclassified},
timestap = {2008-05-26}
}
@InProceedings{ sandhu.ea:nist:2000,
author = {Ravi S. Sandhu and David F. Ferraiolo and D. Richard
Kuhn},
title = {The NIST model for role-based access control: towards a
unified standard},
booktitle = {ACM Workshop on Role-Based Access Control},
year = 2000,
pages = {47--63},
doi = {10.1145/344287.344301},
tags = {ReadingList, AccessControl},
clearance = {unclassified},
timestap = {2008-05-26}
}
@Article{ samuel.ea:context-aware:2008,
author = {Samuel, A. and Ghafoor, A. and Bertino, E.},
title = {Context-Aware Adaptation of Access-Control Policies},
journal = {Internet Computing, IEEE},
year = 2008,
volume = 12,
number = 1,
pages = {51--54},
abstract = {Today, public-service delivery mechanisms such as
hospitals, police, and fire departments rely on digital
generation, storage, and analysis of vital information. To
protect critical digital resources, these organizations
employ access-control mechanisms, which define rules under
which authorized users can access the resources they need
to perform organizational tasks. Natural or man-made
disasters pose a unique challenge, whereby previously
defined constraints can potentially debilitate an
organization's ability to act. Here, the authors propose
employing contextual parameters - specifically, activity
context in the form of emergency warnings - to adapt
access-control policies according to a priori
configuration.},
keywords = {authorisation, disasters, organisational
aspectsaccess-control policy, context-aware adaptation,
digital resource protection, natural disaster,
organizational task, public-service delivery mechanism},
doi = {10.1109/MIC.2008.6},
issn = {1089-7801},
tags = {ReadingList, AccessControl, SoKNOS},
clearance = {unclassified},
timestap = {2008-05-26}
}
@Article{ bertino.ea:trbac:2001,
author = {Elisa Bertino and Piero Andrea Bonatti and Elena Ferrari},
title = {TRBAC: A temporal role-based access control model},
journal = {ACM Trans. Inf. Syst. Secur.},
volume = 4,
number = 3,
year = 2001,
issn = {1094-9224},
pages = {191--233},
doi = {10.1145/501978.501979},
publisher = pub-acm,
address = pub-acm:adr,
tags = {noTAG},
clearance = {unclassified},
timestap = {2008-05-29}
}
@Article{ moyer.ea:generalized:2001,
title = {Generalized role-based access control},
author = {Moyer, M.J. and Abamad, M.},
journal = {Distributed Computing Systems, 2001. 21st International
Conference on.},
year = 2001,
month = {Apr},
pages = {391--398},
keywords = {authorisation, distributed processing, transaction
processingGRBAC, JPEG, RBAC, access control, access control
decisions, access control models, environment roles,
environmental information, expressive power, generalized
role based access control, object roles, object type, rich
access control policies, security policy, security-relevant
characteristics, sensitivity level, subject roles},
doi = {10.1109/ICDSC.2001.918969},
abstract = {Generalized Role-Based Access Control (GRBAC) is a new
paradigm for creating and maintaining rich access control
policies. GRBAC leverages and extends the power of
traditional role based access control (RBAC) by
incorporating subject roles, object roles and environment
roles into access control decisions. Subject roles are like
traditional RBAC roles: they abstract the security-relevant
characteristics of subjects into categories that can be
used in defining a security policy. Similarly, object roles
abstract the various properties of objects, such as object
type (e.g., text, JPEG, executable) or sensitivity level
(e.g., classified, top secret) into categories. Environment
roles capture environmental information, such as time of
day or system load so it can be used to mediate access
control. Together, these three types of roles offer
flexibility and expressive power, as well as a degree of
usability not found in current access control models},
tags = {noTAG},
clearance = {unclassified},
timestap = {2008-05-29}
}
@InProceedings{ bell.ea:secure:1996,
author = {D. Elliott Bell and Leonard J. LaPadula},
title = {Secure Computer Systems: A Mathematical Model, Volume
{II}},
booktitle = {Journal of Computer Security 4},
year = 1996,
pages = {229--263},
note = {An electronic reconstruction of \emph{Secure Computer
Systems: Mathematical Foundations}, 1973}
}
@InProceedings{ bell:looking:2005,
title = {Looking Back at the Bell-La Padula Model},
author = {D. Elliott Bell},
journal = proc
# { the 21st Annual Computer Security Applications
Conference},
year = 2005,
isbn = {1063-9527},
doi = {10.1109/CSAC.2005.37},
publisher = {pub-ieee},
address = pub-ieee:adr,
pages = {337--351}
}
@Booklet{ oasis:xacml:2005,
title = {{eXtensible Access Control Markup Language (XACML)},
Version 2.0},
year = 2005,
url = {http://docs.oasis-open.org/xacml/2.0/XACML-2.0-OS-NORMATIVE.zip}
,
bibkey = {oasis:xacml:2005},
publisher = {OASIS},
key = {OASIS},
language = {USenglish},
public = {yes}
}
@InProceedings{ ferreira.ea:how:2009,
author = {Ana Ferreira and David Chadwick and Pedro Farinha and
Gansen Zhao and Rui Chilro and Ricardo Cruz-Correia and
Luis Antunes},
title = {How to securely break into RBAC: the BTG-RBAC model},
booktitle = {Annual Computer Security Applications Conference (ACSAC)},
year = 2009,
abstract = {Access control models describe frameworks that dictate how
subjects (e.g. users) access resources. In the Role-Based
Access Control (RBAC) model access to resources is based on
the role the user holds within the organization. Although
flexible and easier to manage within large-scale
authorization frameworks, RBAC is usually a static model
where access control decisions have only two output
options: Grant or Deny. Break The Glass (BTG) policies can
be provided in order to break or override the access
controls within an access control policy but in a
controlled and justifiable manner. The main objective of
this paper is to integrate BTG within the NIST/ANSI RBAC
model in a transparent and secure way so that it can be
adopted generically in any domain where unanticipated or
emergency situations may occur. The new proposed model,
called BTG-RBAC, provides a third decision option BTG. This
allows break the glass policies to be implemented in any
application without any major changes to either the
application or the RBAC authorization infrastructure, apart
from the decision engine. Finally, in order to validate the
model, we discuss how the BTG-RBAC model is being
introduced within a Portuguese healthcare institution where
the legislation requires that genetic information must be
accessed by a restricted group of healthcare professionals.
These professionals, advised by the ethical committee, have
required and asked for the implementation of the BTG
concept in order to comply with the said legislation.}
}
@Manual{ ansi:rbac:2004,
bibkey = {ansi:rbac:1998},
abstract = {This standard describes RBAC features that have achieved
acceptance in the commercial marketplace. It includes a
reference model and functional specifications for the RBAC
features defined in the reference model. It is intended for
(1) software engineers and product development managers who
design products incorporating access control features; and
(2) managers and procurement officials who seek to acquire
computer security products with features that provide
access control capabilities in accordance with commonly
known and understood terminology and functional
specifications.},
note = {ANSI INCITS 359-2004},
title = {American National Standard for Information Technology --
Role Based Access Control},
organization = {ANSI},
year = 2004,
month = feb,
publisher = {The American National Standards Institute},
address = {New York}
}
@Article{ li.ea:critique:2007,
author = {Ninghui Li and JiWon Byun and Elisa Bertino},
journal = {Security Privacy, IEEE},
title = {A Critique of the ANSI Standard on Role-Based Access
Control},
year = 2007,
month = {nov.-dec. },
volume = 5,
number = 6,
pages = {41--49},
abstract = {In 2004, the American National Standards Institute
approved the Role-Based Access Control standard to fulfill
"a need among government and industry purchasers of
information technology products for a consistent and
uniform definition of role based access control (RBAC)
features". Such uniform definitions give IT product vendors
and customers a common and unambiguous terminology for RBAC
features, which can lead to wider adoption of RBAC and
increased productivity. However, the current ANSI RBAC
Standard has several limitations, design flaws, and
technical errors that, it unaddressed, could lead to
confusions among IT product vendors and customers and to
RBAC implementations with different semantics, thus
defeating the standard's purpose.},
keywords = {ANSI standard;IT product vendors;role-based access
control;DP industry;authorisation;standards;},
doi = {10.1109/MSP.2007.158},
issn = {1540-7993}
}
@Article{ ardagna.ea:access:2010,
title = {Access control for smarter healthcare using policy
spaces},
journal = {Computers \& Security},
year = 2010,
issn = {0167-4048},
doi = {10.1016/j.cose.2010.07.001},
author = {Claudio A. Ardagna and Sabrina De Capitani di Vimercati
and Sara Foresti and Tyrone W. Grandison and Sushil Jajodia
and Pierangela Samarati},
keywords = {Access control, Break the glass, Policy spaces,
Exceptions, Healthcare systems},
abstract = {A fundamental requirement for the healthcare industry is
that the delivery of care comes first and nothing should
interfere with it. As a consequence, the access control
mechanisms used in healthcare to regulate and restrict the
disclosure of data are often bypassed in case of
emergencies. This phenomenon, called "break the glass", is
a common pattern in healthcare organizations and, though
quite useful and mandatory in emergency situations, from a
security perspective, it represents a serious system
weakness. Malicious users, in fact, can abuse the system by
exploiting the break the glass principle to gain
unauthorized privileges and accesses. In this paper, we
propose an access control solution aimed at better
regulating break the glass exceptions that occur in
healthcare systems. Our solution is based on the definition
of different policy spaces, a language, and a composition
algebra to regulate access to patient data and to balance
the rigorous nature of traditional access control systems
with the "delivery of care comes first" principle.}
}
@Article{ sandhu.ea:arbac97:1999,
author = {Ravi Sandhu and Venkata Bhamidipati and Qamar Munawer},
title = {The ARBAC97 model for role-based administration of roles},
journal = j-tissec,
volume = 2,
number = 1,
year = 1999,
issn = {1094-9224},
pages = {105--135},
doi = {10.1145/300830.300839},
address = pub-acm:adr,
publisher = pub-acm,
abstract = { In role-based access control (RBAC), permissions are
associated with roles' and users are made members of roles,
thereby acquiring the roles; permissions. RBAC's motivation
is to simplify administration of authorizations. An
appealing possibility is to use RBAC itself to manage RBAC,
to further provide administrative convenience and
scalability, especially in decentralizing administrative
authority, responsibility, and chores. This paper describes
the motivation, intuition, and formal definition of a new
role-based model for RBAC administration. This model is
called ARBAC97 (administrative RBAC '97) and has three
components: URA97 (user-role assignment '97), RPA97
(permission-role assignment '97), and RRA97 (role-role
assignment '97) dealing with different aspects of RBAC
administration. URA97, PRA97, and an outline of RRA97 were
defined in 1997, hence the designation given to the entire
model. RRA97 was completed in 1998. ARBAC97 is described
completely in this paper for the first time. We also
discusses possible extensions of ARBAC97. }
}
@Article{ becker:information:2007,
title = {Information governance in NHS's NPfIT: A case for policy
specification},
journal = {International Journal of Medical Informatics},
volume = 76,
number = {5-6},
pages = {432--437},
year = 2007,
mynote = {"Virtual Biomedical Universities and E-Learning" and
"Secure eHealth: Managing Risk to Patient Data" -
E-Learning and Secure eHealth Double S.I.},
issn = {1386-5056},
doi = {10.1016/j.ijmedinf.2006.09.008},
author = {Moritz Y. Becker},
keywords = {Access control},
abstract = {Purpose The National Health Service's (NHS's) National
Programme for Information Technology (NPfIT) in the UK with
its proposed nation-wide online health record service poses
serious technical challenges, especially with regard to
access control and patient confidentiality. The complexity
of the confidentiality requirements and their constantly
evolving nature (due to changes in law, guidelines and
ethical consensus) make traditional technologies such as
role-based access control (RBAC) unsuitable. Furthermore, a
more formal approach is also needed for debating about and
communicating on information governance, as
natural-language descriptions of security policies are
inherently ambiguous and incomplete. Our main goal is to
convince the reader of the strong benefits of employing
formal policy specification in nation-wide electronic
health record (EHR) projects.Approach Many difficulties
could be alleviated by specifying the requirements in a
formal authorisation policy language such as Cassandra. The
language is unambiguous, declarative and
machine-enforceable, and is based on distributed
constrained Datalog. Cassandra is interpreted within a
distributed Trust Management environment, where digital
credentials are used for establishing mutual trust between
strangers.Results To demonstrate how policy specification
can be applied to NPfIT, we translate a fragment of
natural-language NHS specification into formal Cassandra
rules. In particular, we present policy rules pertaining to
the management of Clinician Sealed Envelopes, the mechanism
by which clinical patient data can be concealed in the
nation-wide EHR service. Our case study exposes ambiguities
and incompletenesses in the informal NHS
documents.Conclusions We strongly recommend the use of
trust management and policy specification technology for
the implementation of nation-wide EHR infrastructures.
Formal policies can be used for automatically enforcing
confidentiality requirements, but also for specification
and communication purposes. Formalising the requirements
also reveals ambiguities and missing details in the
currently used informal specification documents.},
publisher = pub-elsevier
}
@InCollection{ brucker.ea:extending:2009,
abstract = {Access control models are usually static, i.e., permissions are granted based on a policy that only changes seldom. Especially for scenarios in health care and disaster management, a more flexible support of access control, i.e., the underlying policy, is needed.\\\\Break-glass is one approach for such a flexible support of policies which helps to prevent system stagnation that could harm lives or otherwise result in losses. Today, break-glass techniques are usually added on top of standard access control solutions in an ad-hoc manner and, therefore, lack an integration into the underlying access control paradigm and the systems' access control enforcement architecture.\\\\We present an approach for integrating, in a fine-grained manner, break-glass strategies into standard access control models and their accompanying enforcement architecture. This integration provides means for specifying break-glass policies precisely and supporting model-driven development techniques based on such policies.},
address = {New York, NY, USA},
author = {Achim D. Brucker and Helmut Petritsch},
booktitle = {ACM symposium on access control models and technologies (SACMAT)},
copyright = {ACM},
copyrighturl = {http://dl.acm.org/authorize?175073},
doi = {10.1145/1542207.1542239},
editor = {Barbara Carminati and James Joshi},
isbn = {978-1-60558-537-6},
keywords = {disaster management, access-control, break-glass, model-driven security},
location = {Stresa, Italy},
pages = {197--206},
pdf = {http://www.brucker.ch/bibliography/download/2009/brucker.ea-extending-2009.pdf},
publisher = {ACM Press},
talk = {talk:brucker.ea:extending:2009},
title = {Extending Access Control Models with Break-glass},
url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-extending-2009},
year = {2009},
}

154
document/root.tex Normal file
View File

@ -0,0 +1,154 @@
\documentclass[11pt,DIV10,a4paper,twoside=semi,openright,titlepage]{scrreprt}
\usepackage{fixltx2e}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Overrides the (rightfully issued) warning by Koma Script that \rm
%%% etc. should not be used (they are deprecated since more than a
%%% decade)
\DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
\DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
\DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
\DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
\DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{isabelle,isabellesym}
\usepackage{stmaryrd}
\usepackage{paralist}
\usepackage{xspace}
\newcommand{\testgen}{HOL-TestGen\xspace}
\newcommand{\testgenFW}{HOL-TestGen/FW\xspace}
\usepackage[numbers, sort&compress, sectionbib]{natbib}
\usepackage{graphicx}
\usepackage{color}
\sloppy
\usepackage{amssymb}
\newcommand{\isasymmodels}{\isamath{\models}}
\newcommand{\HOL}{HOL}
\newcommand{\ie}{i.\,e.}
\newcommand{\eg}{e.\,g.}
\usepackage{pdfsetup}
\urlstyle{rm}
\isabellestyle{it}
\renewcommand{\isamarkupheader}[1]{\section{#1}}
\renewcommand{\isamarkupsection}[1]{\subsection{#1}}
\renewcommand{\isamarkupsubsection}[1]{\subsubsection{#1}}
\renewcommand{\isamarkupsubsubsection}[1]{\paragraph{#1}}
\renewcommand{\isamarkupsect}[1]{\subsection{#1}}
\renewcommand{\isamarkupsubsect}[1]{\susubsection{#1}}
\renewcommand{\isamarkupsubsubsect}[1]{\paragraph{#1}}
\renewcommand{\isastyle}{\isastyleminor}
\pagestyle{empty}
\begin{document}
\renewcommand{\subsubsectionautorefname}{Section}
\renewcommand{\subsectionautorefname}{Section}
\renewcommand{\sectionautorefname}{Section}
\renewcommand{\chapterautorefname}{Chapter}
\newcommand{\subtableautorefname}{\tableautorefname}
\newcommand{\subfigureautorefname}{\figureautorefname}
\title{The Unified Policy Framework\\
(UPF)}
\author{Achim D. Brucker\footnotemark[1] \quad
Lukas Br\"ugger\footnotemark[2] \quad
Burkhart Wolff\footnotemark[3]\\[1.5em]
\normalsize
\normalsize\footnotemark[1]~SAP SE, Vincenz-Priessnitz-Str. 1, 76131 Karlsruhe,
Germany \texorpdfstring{\\}{}
\normalsize\href{mailto:"Achim D. Brucker"
<achim.brucker@sap.com>}{achim.brucker@sap.com}\\[1em]
%
\normalsize\footnotemark[2]Information Security, ETH Zurich, 8092 Zurich, Switzerland
\texorpdfstring{\\}{}
\normalsize\href{mailto:"Lukas Bruegger"
<lukas.a.bruegger@gmail.com>}{Lukas.A.Bruegger@gmail.com}\\[1em]
%
\normalsize\footnotemark[3]~Univ. Paris-Sud, Laboratoire LRI,
UMR8623, 91405 Orsay, France
France\texorpdfstring{\\}{}
\normalsize\href{mailto:"Burkhart Wolff" <burkhart.wolff@lri.fr>}{burkhart.wolff@lri.fr}
}
\pagestyle{empty}
\publishers{%
\normalfont\normalsize%
\centerline{\textsf{\textbf{\large Abstract}}}
\vspace{1ex}%
\parbox{0.8\linewidth}{%
We present the \emph{Unified Policy Framework}
(UPF), a generic framework for modelling security
(access-control) policies; in Isabelle/\HOL.
%\cite{}.
UPF emphasizes the view that a policy is a policy decision
function that grants or denies access to resources, permissions,
etc. In other words, instead of modelling the
relations of permitted or prohibited requests directly, we model
the concrete function that implements the policy decision point
in a system, seen as an ``aspect'' of ``wrapper'' around the
business logic % Fachlogik
of a system.
In more detail, UPF is based on the following four principles:
\begin{inparaenum}
\item Functional representation of policies,
\item No conflicts are possible,
\item Three-valued decision type (allow, deny, undefined),
\item Output type not containing the decision only.
\end{inparaenum}
}
}
\maketitle
\cleardoublepage
\pagestyle{plain}
\tableofcontents
\cleardoublepage
\input{introduction}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% <session>
% \input{session}
\chapter{The Unified Policy Framework (UPF)}
\input{UPFCore}
\input{ElementaryPolicies}
\input{SeqComposition}
\input{ParallelComposition}
\input{Analysis}
\input{Normalisation}
\input{NormalisationTestSpecification}
\input{UPF}
\chapter{Example}
\input{example-intro}
\input{Service}
\input{ServiceExample}
% </session>
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\input{conclusion}
\chapter{Appendix}
\input{Monads}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End:
\nocite{brucker.ea:formal-fw-testing:2014,brucker.ea:hol-testgen-fw:2013,brucker.ea:theorem-prover:2012,brucker.ea:model-based:2011}
\nocite{bruegger:generation:2012}
\bibliographystyle{abbrvnat}
\bibliography{root}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: