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

355 lines
13 KiB
Plaintext
Raw Permalink Blame History

(*****************************************************************************
* 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-2015 Achim D. Brucker, Germany
* 2009-2017 Université Paris-Sud, France
* 2015-2017 The University of Sheffield, UK
*
* 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.
******************************************************************************)
section\<open>Elementary Policies\<close>
theory
ElementaryPolicies
imports
UPFCore
begin
text\<open>
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.
\<close>
subsection\<open>The Core Policy Combinators: Allow and Deny Everything\<close>
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
"_allow_pfun" :: "('\<alpha> \<rightharpoonup>'\<beta>) \<Rightarrow> ('\<alpha> \<mapsto> '\<beta>)" ("A\<^sub>p")
translations
"A\<^sub>p f" \<rightleftharpoons> "AllA f"
syntax
"_deny_pfun" :: "('\<alpha> \<rightharpoonup>'\<beta>) \<Rightarrow> ('\<alpha> \<mapsto> '\<beta>)" ("D\<^sub>p")
translations
"D\<^sub>p f" \<rightleftharpoons> "AllD f"
notation
"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)
subgoal for x
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
done
subsection\<open>Common Instances\<close>
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\<open>... and resulting properties:\<close>
lemma "A\<^sub>I \<Oplus> Map.empty = A\<^sub>I"
by simp
lemma "A\<^sub>f f \<Oplus> Map.empty = A\<^sub>f f"
by simp
lemma "allow_pfun Map.empty = Map.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)+
by (auto simp: deny_pfun_def option.splits)
subsection\<open>Domain, Range, and Restrictions\<close>
text\<open>
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}
\<close>
text\<open>
However, some properties are specific to policy concepts:
\<close>
lemma sub_ran : "ran p \<subseteq> Allow \<union> Deny"
apply (auto simp: Allow_def Deny_def ran_def full_SetCompr_eq[symmetric])[1]
subgoal for x a
apply (case_tac "x")
apply (simp_all)
done
done
lemma dom_allow_pfun [simp]:"dom(allow_pfun f) = dom f"
apply (auto simp: allow_pfun_def)
subgoal for x y
apply (case_tac "f x", simp_all)
done
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)[1]
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)[1]
subgoal for x a
apply (case_tac "f a")
apply (auto simp: image_def)[1]
apply (auto simp: image_def)[1]
done
subgoal for xa a
apply (rule_tac x=a in exI)
apply (simp)
done
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)[1]
subgoal for x a
apply (case_tac "f a")
apply (auto simp: image_def)[1]
apply (auto simp: image_def)[1]
done
subgoal for xa a
apply (rule_tac x=a in exI)
apply (simp)
done
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\<open>
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.
\<close>
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)
subgoal for x y
apply (case_tac "x \<in> S")
apply (simp_all)
done
subgoal for x y
apply (case_tac "x \<in> S")
apply (simp_all)
done
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)
subgoal for x xa xb
apply (case_tac "x xb")
apply simp_all
apply (metis inj_Some inj_image_mem_iff)
done
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
Reference in New Issue View Git Blame Copy Permalink