Role-based authorization constraints specification.
Constraints are an important aspect of role-based access control (RBAC) and are often regarded as one of the principal motivations behind RBAC. Although the importance of contraints in RBAC has been recogni zed for a long time, they have not recieved much attention. In this article, we introduce an intuitive formal language for specifying role-based authorization constraints named RCL 2000 including its basic elements, syntax, and semantics. We give soundness and completeness proofs for RCL 2000 relative to a restricted form of first-order predicate logic. Also, we show how previously identified role-based authorization constraints such as separtation of duty (SOD) can be expressed in our language. Moreover, we show there are other significant SOD properties that have not been previously identified in the literature. Our work shows that there are many alternate formulations of even the simplest SOD properties, with varying degree of flexibility and assurance. Our language provides us a rigorous foundation for systematic study of role-based authorization constraints.
INTRODUCTION
Role-based access control (RBAC) has emerged as a widely accepted alternative to
classical discretionary and mandatory access controls [Sandhu et al. 1996]. Several
models of RBAC have been published and several commercial implementations are
available. RBAC regulates the access of users to information and system resources
Authors' address: Gail-Joon Ahn, College of InformationTechnology, University of North Carolina
at Charlotte, 9201 University City Blvd., Charlotte, NC 28223-0001; email: gahn@uncc.edu; url:
Information and Software Engineering Department, Mail Stop
4A4, George Mason University, Fairfax, VA 22030; email: sandhu@gmu.edu; url: www.list.gmu.edu
Permission to make digital or hard copies of part or all of this work for personal or classroom use is
granted without fee provided that copies are not made or distributed for profit or direct commercial
advantage and that copies show this notice on the first page or initial screen of a display along
with the full citation. Copyrights for components of this work owned by others than ACM must
be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on
servers, to redistribute to lists, or to use any component of this work in other works, requires prior
specific permission and/or a fee. Permissions may be requested from Publications Dept, ACM
Inc., 1515 Broadway, New York, NY 10036 USA, fax +1 (212) 869-0481, or permissions@acm.org.
on the basis of activities that users need to execute in the system. It requires
the identification of roles in the system. A role can be defined as a set of actions
and responsibilities associated with a particular working activity. Then, instead
of specifying all the accesses each individual user is allowed, access authorizations
on objects are specified for roles. Since roles in an organization are relatively
persistent with respect to user turnover and task re-assignment, RBAC provides
a powerful mechanism for reducing the complexity, cost, and potential for error
in assigning permissions to users within the organization. Because roles within an
organization typically have overlapping permissions RBAC models include features
to establish role hierarchies, where a given role can include all of the permissions
of another role. Another fundamental aspect of RBAC is authorization constraints
(also simply called constraints). Although the importance of constraints in RBAC
has been recognized for a long time, they have not received much attention in
the research literature, while role hierarchies have been practiced and discussed at
considerable length.
In this paper our focus is on constraint specifications, i.e, on how constraints can
be expressed. Constraints can be expressed in natural languages, such as English,
or in more formal languages. Natural language specification has the advantage of
ease of comprehension by human beings, but may be prone to ambiguities. Natural
language specifications do not lend themselves to the analysis of properties of the
set of constraints. For example, one may want to check if there are conflicting
constraints in the set of access constraints for an organization. We opted for a formal
language approach to specify constraints. The advantages of a formal approach
include a formal way of reasoning about constraints, a framework for identifying new
types of constraints, a classification scheme for types of constraints (e.g., prohibition
constraints and obligation constraints), and a basis for supporting optimization and
specification techniques on sets of constraints.
To specify these constraints we introduce the specification language RCL 2000
(for Role-based Constraints Language 2000, pronounced R ' ickle 2000) which is the
specification language for role-based authorization constraints. In this paper we describe
its basic elements, syntax, and the formal foundation of RCL 2000 including
rigorous soundness and completeness proofs. RCL 2000 is a substantial generalization
of RSL99 [Ahn and Sandhu 1999] which is the earlier version of RCL 2000. It
obligation constraints in addition to the usual separation of duty and
prohibition constraints. 1
Who would be the user of RCL 2000? The first reaction might be to say the
security officer or the security administrator. However, we feel there is room for a
security policy designer distinct from security administrator. The policy designer
has to understand organizational objectives and articulate major policy decisions
1 A common example of prohibition constraints is separation of duty. We can consider the following
statement as an example of this type of constraints: if a user is assigned to purchasing manager,
he cannot be assigned to accounts payable manager and vice versa. This statement requires that
the same individual cannot be assigned to both roles which are declared mutually exclusive. We
identify another class of constraints called obligation constraints. In [Sandhu 1996], there is a
constraint which requires that certain roles should be simultaneously active in the same session.
There is another constraints which requires a user to have certain combinations of roles in user-role
assignment. We classify such constraints as obligation constraints.
Role-based Authorization Constraints Specification \Delta 3
to support these objectives. The security officer or security administrator is more
concerned with day to day operations. Policy in the large is specified by the security
policy designer and the actions of the security administrator should be subject to
this policy. Thus policy in the large might stipulate what is the meaning of conflicting
roles and what roles are in conflict. For example, the meaning of conflicting
roles for a given organization might be that no users other than senior executives
can belong to two conflicting roles. For another organization the meaning might
be that no one, however senior, may belong to two conflicting roles. In another
context we may want both these interpretations to coexist. So we have a notion
of weak conflict (former case) and strong conflict (latter case), applied to different
roles sets. RCL 2000 is also useful for security researchers to think and reason
about role-based authorization constraints.
The rest of this paper is organized as follows. In section 2 we describes the formal
language RCL 2000 including basic elements and syntax. In section 3 we describe
its formal semantics including soundness and completeness proofs. Section 4 shows
the expressive power of RCL 2000. Section 5 concludes this paper.
2. ROLE-BASED CONSTRAINTS LANGUAGE (RCL 2000)
RCL 2000 is defined in context of RBAC96 which is a well-known family of models
for RBAC [Sandhu et al. 1996]. This model has become a widely-cited authoritative
reference and is the basis of a standard currently under development by the National
Institute of Standards and Technology [Sandhu et al. 2000]. Here we use a slightly
augmented form of RBAC96 illustrated in figure 1. We decompose permissions into
operations and objects to enable formulation of certain forms of constraints. Also
in figure 1 we drop the administrative roles of RBAC96 since they are not germane
to RCL 2000.
Intuitively, a user is a human being or an autonomous agent, a role is a job function
or job title within an organization with some associated semantics regarding
the authority and responsibility conferred on a member of the role, and a permission
is an approval of a particular mode of access (operation) to one or more objects in
the system. Roles are organized in a partial order or hierarchy, so that a senior role
inherits permissions from junior roles, but not vice versa. A user can be a member
of many roles and a role can have many users. Similarly, a role can have many
permissions and the same permission can be assigned to many roles. Each session
relates one user to possibly many roles. Intuitively, a user establishes a session (e.g.,
by signing on to the system) during which the user activates some subset of roles
that he or she is a member of. The permissions available to the users are the union
of permissions from all roles activated in that session. Each session is associated
with a single user. This association remains constant for the life of a session. A
user may have multiple sessions open at the same time, each in a different window
on the workstation screen, for instance. Each session may have a different combination
of active roles. The concept of a session equates to the traditional notion of
a subject in access control. A subject is a unit of access control, and a user may
have multiple subjects (or sessions) with different permissions (or roles) active at
the same time. RBAC96 does not define constraints formally.
Constraints are an important aspect of role-based access control and are a powerful
mechanism for laying out higher level organizational policy. The construc-
U
USERS
USER
ASSIGNMENT
UA
ROLES
R
user roles
PERMISSION
ASSIGNMENT
PA
IONS
OPERA-
TIONS
OP OBJ
HIERARCHY
ROLE RH
Fig. 1. Basic Elements and System Functions : from RBAC96 Model
tions of [Sandhu 1996; Sandhu and Munawer 1998] clearly demonstrate the strong
connection between constraints and policy in RBAC systems. The importance of
flexible constraints to support emerging applications has been recently discussed
by Jaeger [Jaeger 1999]. Consequently, the specification of constraints needs to be
considered. To date, this topic has not received much formal attention in context of
role-based access control. A notable exception is the work of Giuri and Iglio [Giuri
and Iglio 1996] who defined a formal model for constraints on role-activation. RCL
2000 considers all aspects of role-based constraints, not just those applying to role
activation. Another notable exception is the work of Gligor et al [Gligor et al.
1998] who formalize separation of duty constraints enumerated informally by Simon
and Zurko [Simon and Zurko 1997]. RCL 2000 goes beyond separation of
duty to include obligation constraints [Ahn 2000] such as used in the constructions
of [Sandhu 1996; Osborn et al. 2000] for simulating mandatory and discretionary
access controls in RBAC. 2
One of our central claims is that it is futile to try to enumerate all interesting
and practically useful constraints because there are too many possibilities and vari-
ations. Instead, we should pursue an intuitively simple yet rigorous language for
specifying constraints such as RCL 2000. The expressive power of RCL 2000 is
demonstrated in section 4, where it shown that many constraints previously identified
in the RBAC literature and many new ones can be conveniently formulated
in RCL 2000.
2.1 Basic Components
The basic elements and system functions on which RCL 2000 is based are defined
in figure 2. Figure 1 shows the RBAC96 model which is the context for these defi-
nitions. RCL 2000 has six entity sets called users (U), roles (R), objects (OBJ), oper-
Intuitively, Prohibition Constraints are constrains that forbid the RBAC component from doing
(or being) something which is not allowed to do (or be). Most of SOD constraints are included
in this class of constraints. And Obligation Constraints are constraints that force the RBAC
component to do (or be) something.
Role-based Authorization Constraints Specification \Delta 5
set of users, fu1 ; :::; un g.
-R= a set of roles, fr1 ; :::; rmg.
set of operations, fop1 ; :::; opog.
set of objects, fobj1 ; :::; obj r g.
OBJ, a set of permissions, fp1 ; :::; pqg.
set of sessions, fs1 ; :::; s r g.
-RH ' R \Theta R is a partial order on R called the role hierarchy or role dominance relation,
written as -.
-UA ' U \Theta R, a many-to-many user-to-role assignment relation.
\Theta R, a many-to-many permission-to-role assignment relation.
mapping each session s i to the single user.
user mapping each role r i to a set of users.
-roles mapping the set U, P, and S to a set of roles R.
roles extends roles in presence of role hierarchy.
roles
roles   (p i
roles
-sessions mapping each user u i to a set of sessions.
-permissions mapping each role r i to a set of permissions.
permissions extends permissions in presence of role hierarchy.
permissions   (r i
-operations mapping each role r i and object obj i to a set
of operations.
mapping each permission p i to a set of objects.
Fig. 2. Basic Elements and System Functions : from the RBAC96 Model
6 \Delta G.-J. Ahn and R. Sandhu
Quality
Engineer 2
Engineer 1
Production Quality
Engineer 1
Engineering Department (ED)
Employee (E)
Director (DIR)
Project lead 1 (PL1)
Project lead 2 (PL2)
Engineer 2 (E2)
Project 1 Project 2
Production
Engineer 2
Fig. 3. Example of role hierarchies
ations (OP), permissions (P), and sessions (S). These are interpreted as in RBAC96
as discussed above. OBJ and OP are not in RBAC96. OBJ is the passive entities that
contain or receive information. OP is an executable image of a program, which upon
execution causes information flow between objects. P is an approval of a particular
mode of operation to one or more objects in the system.
The function user gives us the user associated with a session and roles gives
us the roles activated in a session. Both functions do not change during the life of
a session. This is a slight simplification from RBAC96 which does allow roles in a
session to change. RCL 2000 thus builds in the constraint that roles in a session
cannot change.
Hierarchies are a natural means for structuring roles to reflect an organization's
lines of authority and responsibility (see Figure 3). By convention, senior roles
are shown toward the top of this diagram and junior roles toward the bottom.
Mathematically, these hierarchies are partial orders. A partial order is a reflexive,
transitive, and antisymmetric relation, so that if x - y then role x inherits the
permissions of role y , but not vice versa. In figure 3, the junior-most role is that
of Employee. The Engineering Department role is senior to Employee and thereby
inherits all permissions from Employee. The Engineering Department role can
have permissions besides those it inherited. Permission inheritance is transitive,
for example, the Engineer1 role inherits permissions from both the Engineering
Department and Employee roles. Engineer1 and Engineer2 both inherit permissions
from the Engineering Department role, but each will have different permissions
directly assigned to it.
The user assignment relation UA is a many-to-many relation between users and
roles. Similarly the permission-assignment relation PA is a many-to-many relation
Role-based Authorization Constraints Specification \Delta 7
a collection of conflicting role sets, fcr 1 ; :::; cr s g, where cr
a collection of conflicting permission sets, fcp
a collection of conflicting user sets,
Fig. 4. Basic Elements and Non-deterministic Functions: beyond RBAC96 Model
between permissions and roles. Users are authorized to use the permissions of roles
to which they are assigned. This is the essence of RBAC.
The remaining functions defined in figure 2 are built from the sets, relations and
functions discussed above. In particular, note that the roles and user functions
can have different types of arguments so we are overloading these symbols. Also
the definition of roles   is carefully formulated to reflect the role inheritance with
respect to users and sessions going downward and with respect to permissions going
upward. In other words a permission in a junior role is available to senior roles,
and activation of a senior role makes available permissions of junior roles. This is a
well-accepted concept in the RBAC literature and is a feature of RBAC96. Using
a single symbol roles   simplifies our notation so long as we keep this duality of
inheritance in mind.
Additional elements and system functions used in RCL 2000 are defined in figure
4. The precise meaning of conflicting roles, permissions and users will be specified
as per organizational policy in RCL 2000. For mutually disjoint organizational
roles such as those of purchasing manager and accounts payable manager, the same
individual is generally not permitted to belong to both roles. We defined these
mutually disjoint roles as conflicting roles. We assume that there is a collection CR
of sets of roles which have been defined to conflict.
The concept of conflicting permissions defines conflict in terms of permissions
rather than roles. Thus the permission to issue purchase orders and the permission
to issue payments are conflicting, irrespective of the roles to which they are assigned.
We denote sets of conflicting permissions as CP. As we will see defining conflict
in terms of permissions offers greater assurance than defining it in terms of roles.
Conflict defined in terms of roles allows conflicting permissions to be assigned to the
same role by error (or malice). Conflict defined in terms of permissions eliminates
this possibility. In the real world, conflicting users should be also considered. For
example, for the process of preparing and approving purchase orders, it might be
company policy that members of the same family should not prepare the purchase
order, and also be a user who approves that order.
RCL 2000 has two non-deterministic functions, oneelement and allother. The
function allows us to get one element x i from set X. We usually write
oneelement as OE. Multiple occurrences of OE(X) in a single RCL 2000 statement
all select the same element x i from X. With allother(X) we can get a set by taking
out one element. We usually write allother as AO. These two non-deterministic
functions are related by context, because for any set S , fOE(S )g [ AO(S
at the same time, neither is a deterministic function.
In order to illustrate how to use these two functions to specify role-based con-
straints, we take the requirement of static separation of duty (SOD) property which
is the simplest variation of SOD. For simplicity assume there is no role hierarchy
(otherwise replace roles by roles   ).
Requirement: No user can be assigned to two conflicting roles. In other
words, conflicting roles cannot have common users. We can express this
requirement as below.
OE(CR) means a conflicting role set and the function roles(OE(U)) returns all roles
which are assigned to a single user OE(U). Therefore this statement ensures that
a single user cannot have more than one conflicting role from the specific role
set OE(CR). We can interpret the above expression as saying that if a user has
been assigned to one conflicting role, that user cannot be assigned to any other
conflicting role. We can also specify this property in many different ways using
RCL 2000, such as
or user(OE(OE(CR))) "
The expression specifies dynamic separation
of duties applied to active roles in a single session as opposed to static
separation applied to user-role assignment. Dynamic separation applied to all sessions
of a user is expressed by j
A permission-centric formulation of separation of duty is specified as roles(OE(OE(CP)))"
OE. The expression roles(OE(OE(CP))) means all roles which
have a conflicting permission from say cp stands for all
roles which have other conflicting permissions from the same conflicting permission
set cp i . This formulation leaves open the particular roles to which conflicting permissions
are assigned but requires that they be distinct. This is just a sampling of
the expressive power of RCL 2000 to be discussed in section 4.
RCL 2000 system functions do not include a time or state variable in their struc-
ture. So we assume that each function considers the current time or state. For
example, the sessions function maps a user u i to a set of current sessions which
are established by user u i . Elimination of time or state from the language simplifies
its formal semantics. RCL 2000 thereby cannot express history or time-based con-
straints. It will need to be extended to incorporate time or state for this purpose.
As a general notational device we have the following convention.
-For any set valued function f defined on set X,
We understand g.
For example, suppose we want to get all users who are assigned to a set of roles
Engineer2g. We can express this using the function user(R)
as equivalent to user(Employee) [ user(Engineer1) [ user(Engineer2).
2.2 Syntax of RCL 2000
The syntax of RCL 2000 is defined by the syntax diagram and grammar given in
figure 5. The rules take the form of flow diagrams. The possible paths represent
the possible sequence of symbols. Starting at the beginning of a diagram, a path
is followed either by transferring to another diagram if a rectangle is reached or by
reading a basic symbol contained in a circle. Backus Normal Form (BNF) is also
Role-based Authorization Constraints Specification \Delta 9
token
expression
statement
token
token
size
set
|
expression
statement
expression
| set
function ( set
op
|
AO
|
size ::= OE
set ::= U
function ::= user j roles j roles   j sessions j permissions j permissions   j
operations
Fig. 5. Syntax of Language
used to describe the grammar of RCL 2000 as shown in the bottom of figure 5.
The symbols of this form are: ::= meaning "is defined as" and j meaning "or."

Figure

5 shows that RCL 2000 statements consist of an expression possibly followed
by implication (=)) and another expression. Also RCL 2000 statements can be
recursively combined with logical AND operator (-). Each expression consists of a
token followed by a comparison operator and token, size, set, or set with cardinality.
Also token itself can be an expression. Each token can be just a term or a term
with cardinality. Each term consists of functions and sets including set operators.
The sets and system functions described earlier in section 2.1 are allowed in this
syntax. Also, we denote oneelement and allother as OE and AO respectively.
3. FORMAL SEMANTICS OF RCL 2000
In this section we discuss the formal semantics for RCL 2000. We do so by identifying
a restricted form of first order predicate logic called RFOPL which is exactly
equivalent to RCL 2000. Any property written in RCL 2000, called a RCL 2000
expression, can be translated to an equivalent expression in RFOPL and vice versa.
The syntax of RFOPL is described later in this section. The translation algorithm,
namely Reduction, converts a RCL 2000 expression to an equivalent RFOPL ex-
pression. This algorithm is outlined in figure 6. Reduction algorithm eliminates AO
from RCL 2000 expression in the first step. Then we translate OE terms
iteratively introducing universal quantifiers from left to right. If we have nested
OE functions in the RCL 2000 expression, translation will start from innermost OE
terms. This algorithm translates RCL 2000 expression to RFOPL expression in
time O(n), supposing that the number of OE term is n.
For example, the following expression can be converted to RFOPL expression
according to the sequences below.
Example 1
Example 2
The resulting RFOPL expression will have the following general structure.
(1) The RFOPL expression has a (possibly empty) sequence of universal quantifiers
as a left prefix, and these are the only quantifiers it can have. We call this
sequence the quantifier part.
Role-based Authorization Constraints Specification \Delta 11
Reduction Algorithm
Input: RCL 2000 expression ; Output: RFOPL expression
Let Simple-OE term be either OE(set), or OE(function(element)), where
set is an element of fU, R, OP, OBJ, P, S, CR, CU, CP, cr, cu, cpg and
function is an element of fuser, roles, roles   , sessions, permissions, permissions   ,
operations, objectg
1. AO elimination
replace all occurrences of AO(expr) with (expr - fOE(expr)g);
2. OE elimination
While There exists Simple-OE term in RCL 2000 expression
choose Simple-OE term;
call reduction procedure;
End
Procedure reduction
case (i) Simple-OE term is OE(set)
create new variable x
put 8x 2 set to right of existing quantifier(s);
replace all occurrences of OE(set) by x ;
case (ii) Simple-OE term is OE(function(element))
create new variable x
put 8x 2 function(element) to right of existing quantifier(s);
replace all occurrences of OE(function(element)) by x ;
End
Fig. 6. Reduction
Construction Algorithm
Input: RFOPL expression ; Output: RCL 2000 expression
1. Construction RCL 2000 expression from RFOPL expression
While There exists a quantifier in RFOPL expression
choose the rightmost quantifier 8 x 2 X;
pick values x and X from the chosen quantifier;
replace all occurrences of x by OE(X);
End
2. Replacement of AO
if there is (expr - fOE(expr)g) in RFOPL expression
replace it with AO(expr);
Fig. 7. Construction
op
function element
set element
element
Fig. 8. Syntax of restricted FOPL expression
(2) The quantifier part will be followed by a predicate separated by a colon (:), i.e.,
universal quantifier part : predicate
(3) The predicate has no free variables or constant symbols. All variables are
declared in the quantifier part, e.g., 8 r 2 R, 8 u
(4) The order of quantifiers is determined by the sequence of OE elimination. In
some cases this order is important so as to reflect the nesting of OE terms in the
RCL 2000 expression. For example, in 8 cr 2 CR, 8 r 2 cr ,8 u
the set cr , which is used in the second quantifier, must be declared in a previous
quantifier as an element, such as cr in the first quantifier.
most of rules in the syntax of RCL 2000 except term syntax
in figure 5. Figure 8 shows the syntax which predicate should follow to express
term.
Because the reduction algorithm has non-deterministic choice for reduction of OE
term, we may have several RFOPL expressions that are translated from a RCL 2000
expression. As we will see in lemma 4 these expressions are logically equivalent, so
it does not matter semantically which one is obtained.
Next, we discuss the algorithm Construction that constructs a RCL 2000 expression
from an RFOPL expression. The algorithm is described in figure 7. This
algorithm repeatedly chooses the rightmost quantifier in RFOPL expression and
constructs the corresponding OE term by eliminating the variable of that quantifier.
After all quantifiers are eliminated the algorithm constructs AO terms according to
the formal definition of AO function. The running time of the algorithm obviously
depends on the number of quantifiers in RFOPL expression.
For example, the following RFOPL expression can be converted to RCL 2000
expression according to the sequence described below.
RFOPL expression:
RCL 2000 expression :
Role-based Authorization Constraints Specification \Delta 13
Unlike the reduction algorithm we can observe the following lemma, where C(expr)
denotes the RCL 2000 expression constructed by Construction algorithm.
Lemma 1. C(fi) always gives us the same RCL 2000 expression ff.
Proof: Construction algorithm always choose the rightmost quantifiers to construct
RCL 2000 expression from RFOPL expression. This procedure is deterministic.
Therefore, given RFOPL expression fi, we will always get the same RCL 2000
We introduced two algorithms, namely Reduction and Construction, that can
reduce and construct RCL 2000 expression. Next we show the soundness and
completeness of this relationship between RCL 2000 and RFOPL expressions.
3.1 Soundness Theorem
Let us define the expressions generated during reduction and construction as intermediate
expression collectively called IE. These expressions have mixed form of
RCL 2000 and RFOPL expressions, that is, they contain quantifiers as well as OE
terms. Note that RCL 2000 and RFOPL expressions are also intermediate expressions

In order to show the soundness of RCL 2000, we introduce the following lemma.
Lemma 2. If the intermediate expression fl is derived from RCL 2000 expression
ff by reduction algorithm in k iterations then construction algorithm applied to fl
will terminate in exactly k iterations.
Proof: It is obvious that fl has k quantifiers because the reduction algorithm
generates exactly one quantifier for each iteration. Now the construction algorithm
eliminates exactly one quantifier per iteration, and will therefore terminate in k
iterations. 2
This leads to the following theorem, where R(expr) denotes the RFOPL expression
translated by Reduction algorithm. We define all occurrences of same OE term
in an intermediate expression as a distinct OE term.
Theorem 1. Given RCL 2000 expression ff, ff can be translated into RFOPL
expression fi. Also ff can be reconstructed from fi. That is,
Proof: Let us define C n as n iterations of reduction algorithm, and R n as n
iterations of reduction algorithm. We will prove the stronger result that C n (R n (ff))
by induction on the number of iterations in reduction R (or, C under the result
of lemma 2).
Basis: If the number of iterations n is 0, the theorem follows trivially.
Inductive Hypothesis: We assume that if n=k , this theorem is true.
Inductive Step: Consider the intermediate expression fl translated by reduction
algorithm in k iterations. Let flbe the intermediate expression translated by
reduction algorithm in the k th iteration. fl differs from flin having an additional
rightmost quantifier and one less distinct OE term. Applying the construction algorithm
to fl, eliminates this rightmost quantifier and brings back the same OE term in
all its occurrences. Thus the construction algorithm applied to fl gives us fl. From
this intermediate expression fl, we can construct ff due to the inductive hypothesis.
This completes the inductive proof. 2
14 \Delta G.-J. Ahn and R. Sandhu
3.2 Completeness Theorem
In order to show the completeness of RCL 2000 relative to RFOPL, we introduce
the following lemma analogous to lemma 2.
Lemma 3. If the intermediate expression fl is derived from RFOPL expression
fi by construction algorithm in k iterations then reduction algorithm applied to fl
will terminate in exactly k iterations.
Proof: It is obvious that fl has k distinct OE terms because the construction algorithm
generates exactly one distinct OE term for each iteration. Now the reduction
algorithm eliminates exactly one distinct OE term per iteration, and will therefore
terminate in k iterations. 2
Next we prove our earlier claim that even though the reduction algorithm is
non-deterministic, all RFOPL expressions translated from the same RCL 2000 expression
will be logically equivalent. More precisely we prove the following result.
Lemma 4. Let ff be an intermediate expression. If R(ff) gives us fi 1 and fi 2 , fi 1
Proof: The proof is by induction on the number n of OE terms in ff.
Basis: If n is 0 the lemma follows trivially.
Inductive Hypothesis: We assume that if n=k , this lemma is true.
Inductive Step: Let By definition R reduces a simple OE term. Clearly
the choice of variable symbol used for this term is not significant. The choice of
term does not matter so long as it is a simple term. Thus all choices for reducing
a simple OE term are equivalent. The Lemma follows by induction hypothesis. 2
The final step to our desired completeness result is obtained below.
Lemma 5. There exists an execution of R such that
Proof: We prove the stronger result that there is an execution of R such that
by induction on the number of iterations in construction C (or, R
under the result of lemma 3).
Basis: If the number of iterations n is 0, the theorem follows trivially.
Inductive Hypothesis: We assume that if n=k , this theorem is true.
Inductive Step: Consider the intermediate expression fl constructed by construction
algorithm in k iterations. Let flbe intermediate expression after the k th
iteration. fl differs from flin having one less quantifier and one more distinct
OE term. Applying one iteration of the reduction algorithm to fl, we can choose
to eliminate this particular OE term and introduce the same variable in the new
rightmost quantifier. This gives us fl 0
. By inductive hypothesis from
there is an
execution of R k that will give us fi. 2
Putting these facts together, we obtain the theorem which shows the completeness
of RCL 2000, relative to RFOPL.
Theorem 2. Given RFOPL expression fi, fi can be translated into RCL 2000
expression ff. Also any firetranslated from ff is logically equivalent to fi. That is,
states that C(fi) gives us a unique result. Let us call it ff. Lemma 5
states there is an execution of R that will go back exactly to fi from ff. Lemma 4
Role-based Authorization Constraints Specification \Delta 15
states that all executions of R for ff will give an equivalent RFOPL expression.
The theorem follows. 2
In this section we have given a formal semantics for RCL 2000 and have demonstrated
its soundness and completeness. Any property written in RCL 2000 could
be translated to an expression which is written in a restricted form of first order
predicate logic, which we call RFOPL. During the analysis of this translation, we
proved two theorems which support the soundness and completeness of the specification
language RCL 2000 and RFOPL respectively.
4. EXPRESSIVE POWER OF RCL 2000
In this section we demonstrate the expressive power of RCL 2000 by showing how
it can be used to express a variety of separation of duty (SOD) properties. In [Ahn
2000] it is further shown how the construction of [Sandhu 1996] and [Osborn et al.
2000] to respectively simulate mandatory and discretionary access controls in RBAC
can be expressed in RCL 2000. As a security principle, SOD is a fundamental
technique for prevention of fraud and errors, known and practiced long before the
existence of computers. It is used to formulate multi-user control policies, requiring
that two or more different users be responsible for the completion of a transaction
or set of related transactions. The purpose of this principle is to minimize fraud by
spreading the responsibility and authority for an action or task over multiple users,
thereby raising the risk involved in committing a fraudulent act by requiring the
involvement of more than one individual. A frequently used example is the process
of preparing and approving purchase orders. If a single individual prepares and
approves purchase orders, it is easy and tempting to prepare and approve a false
order and pocket the money. If different users must prepare and approve orders,
then committing fraud requires a conspiracy of at least two, which significantly
raises the risk of disclosure and capture.
Although separation of duty is easy to motivate and understand intuitively, so far
there is no formal basis for expressing this principle in computer security systems.
Several definitions of SOD have been given in the literature. For the purpose of
this paper we use the following definition.
Separation of duty reduces the possibility for fraud or significant errors
(which can cause damage to an organization) by partitioning of tasks
and associated privileges so cooperation of multiple users is required to
complete sensitive tasks.
We have the following definition for interpreting SOD in role-based environments.
Role-Based separation of duty ensures SOD requirements in role-based
systems by controlling membership in, activation of, and use of
roles as well as permission assignment.
There are several papers in the literature over the past decade which deal with
separation of duty. During this period various forms of SOD have been identified.
Attempts have been made to systematically categorize these definitions. Notably,
Simon and Zurko [Simon and Zurko 1997] provide an informal characterization,
and Gligor et al. [Gligor et al. 1998] provide a formalism of this characterization.
However, this work has significant limitations. It omits important forms of SOD
Properties Expressions
1. SSOD-CR j roles
2. SSOD-CP j permissions(roles
3. Variation of 2 (2) - j permissions
4. Variation of 1 (1) - j permissions
5. SSOD-CU (1) -
6. Yet another variation (4) - (5)

Table

1. Static Separation of Duty
including session-based dynamic SOD needed for simulating lattice-based access
control and Chinese Walls in RBAC [Sandhu 1993; Sandhu 1996]. It also does not
deal with SOD in the presence of role hierarchies. Moreover, as will see, there are
additional SOD properties that have not been identified in the previous literature.
Here, we take a different approach to understand SOD. Rather than simply enumerating
different kinds of SOD we show how RCL 2000 can be used to specify the
various separation of duty properties.
4.1 Static SOD
Static SOD (SSOD) is the simplest variation of SOD. In table 1 we show our
expression of several forms of SSOD. These include new forms of SSOD which have
not previously been identified in the literature. This demonstrates how RCL 2000
helps us in understanding SOD and discovering new basic forms of it.
Property 1 is the most straightforward property. The SSOD requirement is that
no user should be assigned to two roles which are conflicting each other. In other
words, it means that conflicting roles cannot have common users. RCL 2000 can
clearly express this property. This property is the classic formulation of SSOD
which is identified by several papers including [Gligor et al. 1998; Kuhn 1997;
Sandhu et al. 1996]. It is a role-centric property.
Property 2 follows the same intuition as property 1, but is permission-centric.
that a user can have at most one conflicting permission acquired
through roles assigned to the user. Property 2 is a stronger formulation than property
which prevents mistakes in role-permission assignment. This kind of property
has not been previously mentioned in the literature. RCL 2000 helps us discover
such omissions in previous work. In retrospect property 2 is an "obvious property"
but there is no mention of this property in over a decade of SOD literature. Even
though property 2 allows more flexibility in role-permission assignment since the
conflicting roles are not predefined, it can also generate roles which cannot be used
at all. For example, two conflicting permissions can be assigned to a role. Property
simply requires that no user can be assigned to such a role or any role senior to
it, which makes that role quite useless. Thus property 2 prevents certain kinds of
mistakes in role-permissions but tolerates others.
Property 3 eliminates the possibility of useless roles with an extra condition,
jpermissions   (OE(R))"OE(CP) j - 1. This condition ensures that each role can have
at most one conflicting permission without consideration of user-role assignment.
With this new condition, we can extend property 1 in presence of conflicting
Role-based Authorization Constraints Specification \Delta 17
permissions as property 4. In property 4 we have another additional condition that
conflicting permissions can only be assigned to conflicting roles. In other words,
non-conflicting roles cannot have conflicting permissions. The net effect is that a
user can have at most one conflicting permission via roles assigned to the user.
Property 4 can be viewed as a reformulation of property 3 in a role-centric man-
ner. Property 3 does not stipulate a concept of conflicting roles. However, we
can interpret conflicting roles to be those that happen to have conflicting permissions
assigned to them. Thus for every cp i we can define cr
OEg. With this interpretation, properties 3 and 4 are essentially
identical. The viewpoint of property 3 is that conflicting permissions get
assigned to distinct roles which thereby become conflicting, and therefore cannot
assigned to the same user. Which roles are deemed conflicting is not determined a
priori but is a side-effect of permission-role assignment. The viewpoint of property
4 is that conflicting roles are designated in advance and conflicting permissions must
be restricted to conflicting roles. These properties have different consequences on
how roles get designed and managed but essentially achieve the same objective with
respect to separation of conflicting permissions. Both properties achieve this goal
with much higher assurance than property 1. Property 2 achieves this goal with
similar high assurance but allows for the possibility of useless roles. Thus, even in
the simple situation of static SOD, we have a number of alternative formulations
offering different degrees of assurance and flexibility.
Property 5 is a very different property and is also new to the literature. With a
notion of conflicting users, we identify new forms of SSOD. Property 5 says that two
conflicting users cannot be assigned to roles in the same conflicting role set. This
property is useful because it is much easier to commit fraud if two conflicting users
can have different conflicting roles in the same conflicting role set. This property
prevents this kind of situation in role-based systems. A collection of conflicting
users is less trustworthy than a collection of non-conflicting users, and therefore
should not be mixed up in the same conflicting role set. This property has not
been previously identified in the literature.
We also identify a composite property which includes conflicting users, roles and
permissions. Property 6 combines property 4 and 5 so that conflicting users cannot
have conflicting roles from the same conflict set while assuring that conflicting roles
have at most one conflicting permission from each conflicting permission sets. This
property supports SSOD in user-role and role-permission assignment with respect
to conflicting users, roles, and permissions.
4.2 Dynamic SOD
In RBAC systems, a dynamic SOD (DSOD) property with respect to the roles activated
by the users requires that no user can activate two conflicting roles. In other
words, conflicting roles may have common users but users can not simultaneously
activate roles which are conflicting each other. From this requirement we can express
user-based Dynamic SOD as property 1. We can also identify a Session-based
Dynamic SOD property which can apply to the single session as property 2. We can
also consider these properties with conflicting users such as property 1-1 and 2-1.
Additional analysis of dynamic SOD properties based on conflicting permissions
can also be pursued as was done for static SOD.
Properties Expressions
1. User-based DSOD j roles
1-1. User-based DSOD with CU j roles
2. Session-based DSOD j roles
2-1. Session-based DSOD with CU j roles

Table

2. Dynamic Separation of Duty
5. CONCLUSION
In this paper we have described the specification language RCL 2000. This language
is built on RBAC96 components and has two non-deterministic functions
OE and AO. We have given a formal syntax and semantics for RCL 2000 and have
demonstrated its soundness and completeness. Any property written in RCL 2000
could be translated to an expression which is written in a restricted form of first
order predicate logic, which we call RFOPL. During the analysis of this transla-
tion, we proved two theorems which support the soundness and completeness of the
specification language RCL 2000 and RFOPL respectively.
RCL 2000 provides us a foundation for studying role-based authorization con-
straints. It is more natural and intuitive than RFOPL. The OE and AO operators
were intuitively motivated by Chen and Sandhu [Chen and Sandhu 1995] and formalized
in RCL 2000. They provide a viable alternative to reasoning in terms of
long strings of universal quantifiers. Also the same RCL 2000 expression has multiple
but equivalent RFOPL formulations indicating that there is a unifying concept
in RCL 2000.
There is room for much additional work with RCL 2000 and similar specification
languages. The language can be extended by introducing time and state. Analysis
of RCL 2000 specifications and their composition can be studied. The efficient
enforcement of these constraints can also be investigated. A user-friendly front-end
to the language can be developed so that it can be realistically used by security
policy designers.

Acknowledgement

This work is partially supported by the National Science Foundation and the National
Agency.



--R

The RCL
The RSL99 language for role-based separation of duty constraints
Constraints for role based access control.
A formal model for role-based access control with constraints


On the increasing importance of constraints.
Mutual exclusion of roles as a means of implementing separation of duty in role-based access control systems
Configuring role-based access control to enforce mandatory and discretionary access control policies

The nist model for role-based access control: Towards a unified standard
How to do discretionary access control using roles.
Role hierarchies and constraints for lattice-based access controls


Separation of duty in role-based environments
--TR
Role-Based Access Control Models
Mutual exclusion of roles as a means of implementing separation of duty in role-based access control systems
Constraints for role-based access control
How to do discretionary access control using roles
On the increasing importance of constraints
The <italic>RSL99</italic> language for role-based separation of duty constraints
The NIST model for role-based access control
Configuring role-based access control to enforce mandatory and discretionary access control policies
Lattice-Based Access Control Models
Role Hierarchies and Constraints for Lattice-Based Access Controls
A Formal Model for Role-Based Access Control with Constraints
Separation of Duty in Role-based Environments
The rcl 2000 language for specifying role-based authorization constraints

--CTR
David F. Ferraiolo , Ravi Sandhu , Serban Gavrila , D. Richard Kuhn , Ramaswamy Chandramouli, Proposed NIST standard for role-based access control, ACM Transactions on Information and System Security (TISSEC), v.4 n.3, p.224-274, August 2001
Trent Jeager, Managing access control complexity using metrices, Proceedings of the sixth ACM symposium on Access control models and technologies, p.131-139, May 2001, Chantilly, Virginia, United States
Ninghui Li , Mahesh V. Tripunitara, Security analysis in role-based access control, ACM Transactions on Information and System Security (TISSEC), v.9 n.4, p.391-420, November 2006
Ninghui Li , Mahesh V. Tripunitara , Qihua Wang, Resiliency policies in access control, Proceedings of the 13th ACM conference on Computer and communications security, October 30-November 03, 2006, Alexandria, Virginia, USA
Timothy Fraser , David Ferraiolo , Mikel L. Matthews , Casey Schaufler , Stephen Smalley , Robert Watson, Panel: which access control technique will provide the greatest overall benefit, Proceedings of the sixth ACM symposium on Access control models and technologies, p.141-149, May 2001, Chantilly, Virginia, United States
Jason Crampton , George Loizou, Authorisation and antichains, ACM SIGOPS Operating Systems Review, v.35 n.3, p.6-15, July 1 2001
Chiara Braghin , Daniele Gorla , Vladimiro Sassone, Role-based access control for a distributed calculus, Journal of Computer Security, v.14 n.2, p.113-155, January 2006
Jason Crampton , George Loizou, Administrative scope: A foundation for role-based administrative models, ACM Transactions on Information and System Security (TISSEC), v.6 n.2, p.201-231, May
James B. D. Joshi , Elisa Bertino , Arif Ghafoor, An Analysis of Expressiveness and Design Issues for the Generalized Temporal Role-Based Access Control Model, IEEE Transactions on Dependable and Secure Computing, v.2 n.2, p.157-175, April 2005
Ninghui Li , Ziad Bizri , Mahesh V. Tripunitara, On mutually-exclusive roles and separation of duty, Proceedings of the 11th ACM conference on Computer and communications security, October 25-29, 2004, Washington DC, USA
Shih-Chien Chou , Wei-Chuan Hsu , Wei-Kuang Lo, DPE/PAC: decentralized process engine with product access control, Journal of Systems and Software, v.76 n.3, p.207-219, June 2005
Dongwan Shin , Gail-Joon Ahn , Sangrae Cho , Seunghun Jin, On modeling system-centric information for role engineering, Proceedings of the eighth ACM symposium on Access control models and technologies, June 02-03, 2003, Como, Italy
Tolone , Gail-Joon Ahn , Tanusree Pai , Seng-Phil Hong, Access control in collaborative systems, ACM Computing Surveys (CSUR), v.37 n.1, p.29-41, March 2005
Jean Bacon , Ken Moody , Walt Yao, A model of OASIS role-based access control and its support for active security, ACM Transactions on Information and System Security (TISSEC), v.5 n.4, p.492-540, November 2002
James B. D. Joshi , Elisa Bertino , Usman Latif , Arif Ghafoor, A Generalized Temporal Role-Based Access Control Model, IEEE Transactions on Knowledge and Data Engineering, v.17 n.1, p.4-23, January 2005
Steve Barker , Peter J. Stuckey, Flexible access control policy specification with constraint logic programming, ACM Transactions on Information and System Security (TISSEC), v.6 n.4, p.501-546, November
Ninghui Li , Mahesh V. Tripunitara, Security analysis in role-based access control, Proceedings of the ninth ACM symposium on Access control models and technologies, June 02-04, 2004, Yorktown Heights, New York, USA
M. Koch , L. V. Mancini , F. Parisi-Presicce, Administrative scope in the graph-based framework, Proceedings of the ninth ACM symposium on Access control models and technologies, June 02-04, 2004, Yorktown Heights, New York, USA
Steve Neely , Helen Lowe , David Eyers , Jean Bacon , Julian Newman , Xiaofeng Gong, An architecture for supporting vicarious learning in a distributed environment, Proceedings of the 2004 ACM symposium on Applied computing, March 14-17, 2004, Nicosia, Cyprus
Trent Jaeger , Reiner Sailer , Xiaolan Zhang, Resolving constraint conflicts, Proceedings of the ninth ACM symposium on Access control models and technologies, June 02-04, 2004, Yorktown Heights, New York, USA
Dongwan Shin , Gail-Joon Ahn , Sangrae Cho , Seunghun Jin, A role administration system in role-based authorization infrastructures: design and implementation, Proceedings of the ACM symposium on Applied computing, March 09-12, 2003, Melbourne, Florida
Trent Jaeger , Xiaolan Zhang , Fidel Cacheda, Policy management using access control spaces, ACM Transactions on Information and System Security (TISSEC), v.6 n.3, p.327-364, August
Sushil Jajodia , Duminda Wijesekera, Recent advances in access control models, Proceedings of the fifteenth annual working conference on Database and application security, p.3-15, July 15-18, 2001, Niagara, Ontario, Canada
David F. Ferraiolo, An argument for the role-based access control model, Proceedings of the sixth ACM symposium on Access control models and technologies, p.142-143, May 2001, Chantilly, Virginia, United States
Duminda Wijesekera , Sushil Jajodia, Policy algebras for access control the predicate case, Proceedings of the 9th ACM conference on Computer and communications security, November 18-22, 2002, Washington, DC, USA
Joon S. Park , Ravi Sandhu , Gail-Joon Ahn, Role-based access control on the web, ACM Transactions on Information and System Security (TISSEC), v.4 n.1, p.37-71, Feb. 2001
Trent Jaeger , Antony Edwards , Xiaolan Zhang, Managing access control policies using access control spaces, Proceedings of the seventh ACM symposium on Access control models and technologies, June 03-04, 2002, Monterey, California, USA
James B. D. Joshi , Basit Shafiq , Arif Ghafoor , Elisa Bertino, Dependencies and separation of duty constraints in GTRBAC, Proceedings of the eighth ACM symposium on Access control models and technologies, June 02-03, 2003, Como, Italy
Ninghui Li , Mahesh V. Tripunitara , Ziad Bizri, On mutually exclusive roles and separation-of-duty, ACM Transactions on Information and System Security (TISSEC), v.10 n.2, p.5-es, May 2007
Mark Strembeck , Gustaf Neumann, An integrated approach to engineer and enforce context constraints in RBAC environments, ACM Transactions on Information and System Security (TISSEC), v.7 n.3, p.392-427, August 2004
Shariq Rizvi , Alberto Mendelzon , S. Sudarshan , Prasan Roy, Extending query rewriting techniques for fine-grained access control, Proceedings of the 2004 ACM SIGMOD international conference on Management of data, June 13-18, 2004, Paris, France
Ninghui Li , Qihua Wang, Beyond separation of duty: an algebra for specifying high-level security policies, Proceedings of the 13th ACM conference on Computer and communications security, October 30-November 03, 2006, Alexandria, Virginia, USA
Jason Crampton, Specifying and enforcing constraints in role-based access control, Proceedings of the eighth ACM symposium on Access control models and technologies, June 02-03, 2003, Como, Italy
Gail-Joon Ahn , Badrinath Mohan , Seng-Phil Hong, Towards secure information sharing using role-based delegation, Journal of Network and Computer Applications, v.30 n.1, p.42-59, January 2007
Hong Chen , Ninghui Li, Constraint generation for separation of duty, Proceedings of the eleventh ACM symposium on Access control models and technologies, June 07-09, 2006, Lake Tahoe, California, USA
Rakesh Bobba , Serban Gavrila , Virgil Gligor , Himanshu Khurana , Radostina Koleva, Administering access control in dynamic coalitions, Proceedings of the 19th conference on Large Installation System Administration Conference, p.23-23, December 04-09, 2005, San Diego, CA
David Basin , Jrgen Doser , Torsten Lodderstedt, Model driven security: From UML models to access control infrastructures, ACM Transactions on Software Engineering and Methodology (TOSEM), v.15 n.1, p.39-91, January 2006
Shih-Chien Chou, Embedding role-based access control model in object-oriented systems to protect privacy, Journal of Systems and Software, v.71 n.1-2, p.143-161, April 2004
Gustaf Neumann , Mark Strembeck, An approach to engineer and enforce context constraints in an RBAC environment, Proceedings of the eighth ACM symposium on Access control models and technologies, June 02-03, 2003, Como, Italy
Trent Jaeger , Jonathon E. Tidswell, Practical safety in flexible access control models, ACM Transactions on Information and System Security (TISSEC), v.4 n.2, p.158-190, May 2001
David F. Ferraiolo , R. Chandramouli , Gail-Joon Ahn , Serban I. Gavrila, The role control center: features and case studies, Proceedings of the eighth ACM symposium on Access control models and technologies, June 02-03, 2003, Como, Italy
Longhua Zhang , Gail-Joon Ahn , Bei-Tseng Chu, A rule-based framework for role-based delegation and revocation, ACM Transactions on Information and System Security (TISSEC), v.6 n.3, p.404-441, August
Ravi Sandhu , Kumar Ranganathan , Xinwen Zhang, Secure information sharing enabled by Trusted Computing and PEI models, Proceedings of the 2006 ACM Symposium on Information, computer and communications security, March 21-24, 2006, Taipei, Taiwan
Gustaf Neumann , Mark Strembeck, Design and implementation of a flexible RBAC-service in an object-oriented scripting language, Proceedings of the 8th ACM conference on Computer and Communications Security, November 05-08, 2001, Philadelphia, PA, USA
Tanvir Ahmed , Anand R. Tripathi, Specification and verification of security requirements in a programming model for decentralized CSCW systems, ACM Transactions on Information and System Security (TISSEC), v.10 n.2, p.7-es, May 2007
Merwyn Taylor, Hierarchical data security in a query-by-example interface for a shared database, Journal of Biomedical Informatics, v.35 n.3, p.171-177, June 2002
Gail-Joon Ahn , Hongxin Hu, Towards realizing a formal RBAC model in real systems, Proceedings of the 12th ACM symposium on Access control models and technologies, June 20-22, 2007, Sophia Antipolis, France
Elisa Bertino , Ravi Sandhu, Database Security-Concepts, Approaches, and Challenges, IEEE Transactions on Dependable and Secure Computing, v.2 n.1, p.2-19, January 2005
Andreas Schaad , Volkmar Lotz , Karsten Sohr, A model-checking approach to analysing organisational controls in a loan origination process, Proceedings of the eleventh ACM symposium on Access control models and technologies, June 07-09, 2006, Lake Tahoe, California, USA
JuHum Kwon , Chang-Joo Moon, Visual modeling and formal specification of constraints of RBAC using semantic web technology, Knowledge-Based Systems, v.20 n.4, p.350-356, May, 2007
Khaled Alghathbar, Validating the enforcement of access control policies and separation of duty principle in requirement engineering, Information and Software Technology, v.49 n.2, p.142-157, February, 2007
authorization constraints;constraints specification;access control models;role-based access control