A Modal Logic for Role-Based Access Control - Computer Network Security - page 181

The rest of this paper is organized as follows. Section 2 provides a brief
RBAC tutorial. Section 3 describes the syntax and and semantics of our logic,
which builds on the work of Abadi and colleagues [11,1]. Section 4 explains how
RBAC relations are described in our extended logic. Section 5 presents the HOL
definitions of static and dynamic separation of duty constraints. Finally, our
conclusions are in Section 6.

2 Role-Based Access Control (RBAC)

Role-Based Access Control (RBAC) [5,4,6] replaces direct user-permission as-
sociations in traditional access control through a combination of user-role and
role-permission associations. Rather than assigning individuals specific permis-
sions that may change as their duties and status change, an RBAC policy assigns
users to roles and grants permissions to roles. In RBAC, an access request q made
by a user U will be granted if and only if U is authorized to act in a role R that
has been granted the permission q .
RBAC policies involve three essential entities: a set of users, a set of roles,
and a set of permissions. RBAC also defines a set UA of user assignments and a
set PA of permission assignments: ( U, R )

∈ UA means that user U has the right

to act in role R ,and( p, R ) ∈ PA means that permission p is assigned to role R .

2.1 Role Inheritance

RBAC also includes a partial order over roles called role inheritance .When
role R 1 inherits role R 2 , denoted R 1 R 2 ,everyuser U explicitly assigned

to role R 1 is also implicitly assigned to role R 2 ; likewise, every permission p
explicitly associated with role R 2 is implicitly associated with role R 1 .Thesets
authorized users ( R )and authorized permissions ( R ) define the authorized users
and authorized permissions of a role R are given respectively:

authorized users ( R )=
{ R ∈ ROLES. ( R (( U, R ) U ∈ USERS |∃ R ) ∧ ∈ UA ) }

authorized permissions ( R )=
{ R ∈ R ) (( p, R ) p ∈ PRMS |∃ ROLES. ( R ∧ ∈ PA ) } .

From these definitions, it is straightforward to verify the following two properties:

1. If R 1 R 2 ,then authorized users ( R 1 ) ⊆ authorized users ( R 2 ).

2. If R 1 R 2 ,then authorized permissions ( R 2 ) ⊆ authorized permissions ( R 1 ).

2.2 Separation of Duty

RBAC also supports constraints such as separation of duty. Static separation of
duty provides a way to specify mutually exclusive roles (i.e., roles that should
never have authorized users in common). In RBAC, static separation of duty is