355 lines
13 KiB
Plaintext
355 lines
13 KiB
Plaintext
(*****************************************************************************
|
|
* 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
|