UPF/Service.thy

479 lines
23 KiB
Plaintext
Raw Permalink Normal View History

(*****************************************************************************
* 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