Formal Z Specifications of Several Flat Role-Based Access Control Models

Role-based access control (RBAC) is a high level authorization mechanism in which access decisions are based on the roles that users hold within an organization. Because RBAC offers scalability, consistency and ease of maintenance, it is very useful, particularly for large organizations. RBAC has been used to describe authorization in a wide variety of applications ranging from operating systems and databases to complex information systems. Despite its widespread adoption, however, there doesn´t seem to be a common agreement on the semantics of even key RBAC concepts. For examples, the definitions of fundamental terms such as subject, principal, role, task, and permission have been open to many different and sometimes inconsistent interpretations. This paper attempts to clarify and define essential RBAC concepts. Based on these definitions, a variety of state-based flat role based access control models are developed. These models have increasing degrees of complexity and are formulated in the specification notation Z. The starting point is a core RBAC model which, in turn, is successively refined into a series of flat RBAC models with increasing levels of details. The semantics of each model is captured by giving a precise formulation of its corresponding reference monitor which makes access control decisions