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

voting member. These constraints can be represented by the following static
separation-of-duty relation:

SSD = { ( { Ten, UnTen } , 2) , ( { P&T VM, Chair } , 2) } .

Because the roles Chair and P&T VM both inherit the Ten role, these two
constraints also prevent untenured faculty from being department chair and
from being voting members of the P&T committee.
The department's bylaws also require the P&T Committee to contain a fixed
number of representatives from each of the CS and CE programs. Thus, for
the purposes of P&T deliberations, no faculty member can simultaneously rep-
resent both the CS and CE programs, although she may be associated with
both programs. This constraint can be represented by the following dynamic
separation-of-duty relation:

DSD = { ( { CS Fac, CE Fac, P&T VM } , 3) } .

Thus, no one may simultaneously act as CS faculty, CE faculty, and a P&T
voting member, although they may authorized for all three roles and may act in
any two of those roles simultaneously.
We have not explicitly given the user-role and permission-role assignments.
However, suppose that the permission read student grade reports is associated
with the faculty role Fac (i.e., ( read student grade reports, Fac ) ∈ PA ), and that

Alice is explicitly assigned to the role Chair (i.e., ( Alice, Chair ) UA ). First of

all, note that the SSD relation prohibits any user from being authorized for both
the Ten and UnTen roles. Thus, the role hierarchy prevents Alice from being
assigned to the UnTen role, as her assignment to Chair also implicitly authorizes
her for the Ten role. Second, the role-inheritance relation also authorizes Alice
to act in the role Fac ( Alice

∈

authorized users ( Fac )), and hence she is entitled
to adopt either the Fac or Chair roles to read student grade reports .
Having described the key concepts of RBAC, we now introduce a modal logic
for access control in which RBAC relationships can be described.

∈

3 A Logic for Reasoning About Access Control

The access-control logic of Abadi and colleagues [11,1] incorporates a calculus of
principals into a standard multi-agent modal logic. The result is a set of logical
rules for manipulating formulas that provides a tool for reasoning about access
control, delegation, and trust.
Principals are entities (e.g., people, machines, encryption keys, and processes)
that make statements. Principals can be either a simple name (e.g., “ Alice ”) or
compound principals (e.g., “ Alice and Carol ”). Statements are the things that
principals say, such as “read file foo ”or“ Alice can read file foo .”
In this section, we extend the Abadi logic with a few constructs that will
allow us to reason about requests in the context of RBAC.