Information Technology Reference
In-Depth Information
A Modal Logic for Role-Based Access Control
Thumrongsak Kosiyatrakul, Susan Older, and Shiu-Kai Chin
EECS Department, Syracuse University, Syracuse, New York 13244, USA
skchin@syr.edu
Abstract.
Making correct access-control decisions is central to security,
which in turn requires accounting correctly for the identity, credentials,
roles, authority, and privileges of users and their agents. In networked
systems, these decisions are made more complex because of delegation
and differing access-control policies. Methods for reasoning rigorously
about access control and computer-assisted reasoning tools for verifica-
tion are effective for providing assurances of security. In this paper we
extend the access-control logic of [11,1] to also support reasoning about
role-based access control (RBAC), which is a popular technique for reduc-
ing the complexity of assigning privileges to users. The result is an access-
control logic which is simple enough for design and verification engineers
to use to assure the correctness of systems with access-control require-
ments but yet powerful enough to reason about delegations, credentials,
and trusted authorities. We explain how to describe RBAC components
such as user assignments, permission assignments, role inheritance, role
activations, and users' requests. The logic and its extensions are proved
to be sound and implemented in the HOL (Higher Order Logic version
4) theorem prover. We also provide formal support for RBAC's static
separation of duty and dynamic separation of duty constraints in the
HOL theorem prover. As a result, HOL can be used to verify properties
of RBAC access-control policies, credentials, authority, and delegations.
1
Introduction
The ubiquitous use of inter-networked computers makes controlled access to
information and services simultaneously essential and complex. Access is ulti-
mately granted based on establishing a relationship between a principal and her
privileges with respect to a particular object. In networked systems, requests
and authority may be delegated. This complicates the task of establishing the
identity and authority of principals behind access requests.
One interesting specialty logic for reasoning about access-control policies and
decisions is the access-control logic of Abadi and colleagues [11,1]. This modal
logic brings clarity and consistency to reasoning about access requests because it
provides a formal model of principals, statements, credentials, authority, trust,
Partially supported by the CASE Center at Syracuse University, a New York State
Center for Advanced Technology supported by the New York State Oce of Science
Technology and Academic Research.
