A Light-Weight Formal Approach for Modeling, Verifying and Integrating Role-Based Access Control Requirements

As the complexity of access control requirements is increasing to protect valuable organizational data the value of correct specification and integration of access rights into the system specification has also increased. Role-based access control (RBAC) facilitates specification of access control requirements in a flexible manner. However, various available models do not always support effective integration of the requirements into rest of the system specification. Furthermore, automated verification of RBAC model poses the challenge of state-explosion. In this paper we propose a lightweight formal method for model-checking of RBAC specification. We use BT-RBAC model to specify access control requirements. The model is based on a graphical notation with formal semantics and supports a requirements translation process, strong traceability of requirements, and uses a single notation to support effective integration of the model. The automated translation into SAL specification input language is used to formally verify the correctness of the model.