Formal specification for role based access control user/role and role/role relationship management

Abstract

Role Based Access Control (RBAC), an access control mechanism, reduces the cost of administering access con trol policies as well as making the process less error-prone. The Admin Tool developed for the NIST RBAC Model manages user/role and role/role relationships stored in the RBA C Database. This paper presents a formal specification of the RBAC Database and Admin Tool operations. Consistency requirements for the RBAC Database are defined as a set of properties. Alternative properties, substantially simpler to verify in an implementation, are shown to be equivalen t. In addition, the paper defines the semantics of Admin Tool operations, and shows that, given a consistent RBAC Database and an operation which meets specified conditions, the RBAC Database remains consistent after the operation is performed. This paper describes the Admin Tool developed for the NIST RBAC Model. It presents a formal specification of the initial set of consistency properties for the RBAC Da tabase consistency and the simplified set. These two sets of consistency properties are shown to be equivalent. In addition, the paper presents a formal specification of RBAC Database operations. It is shown that, given a consistent RBAC Database, database operations which meet given conditions maintain database consistency. The Admin Tool described in this paper is part of three implementations of the NIST RBAC Model: one for the World Wide Web (RBAC/Web) (2), one for use in relational database environments, where the RBAC Database is implemented by tables in a commercial DBMS, and one for Windows NT.1 The Windows NT implementation does not support Dynamic Separation of Duties.