Automated Verification Of Role-Based Access Control Policies Constraints Using Prover9

TL;DR

This paper introduces an automated method for verifying role-based access control policies and constraints using first-order logic and the Prover9 theorem prover, enhancing accuracy and efficiency in security policy validation.

Contribution

It develops a formal logical framework for specifying RBAC policies and constraints and demonstrates their verification using Prover9, addressing the complexity of manual validation.

Findings

Formal specification of RBAC constraints in first-order logic

Implementation of automated verification with Prover9

Improved accuracy and efficiency in policy validation

Abstract

Access control policies are used to restrict access to sensitive records for authorized users only. One approach for specifying policies is using role based access control (RBAC) where authorization is given to roles instead of users. Users are assigned to roles such that each user can access all the records that are allowed to his/her role. RBAC has a great interest because of its flexibility. One issue in RBAC is dealing with constraints. Usually, policies should satisfy pre-defined constraints as for example separation of duty (SOD) which states that users are not allowed to play two conflicting roles. Verifying the satisfiability of constraints based on policies is time consuming and may lead to errors. Therefore, an automated verification is essential. In this paper, we propose a theory for specifying policies and constraints in first order logic. Furthermore, we present a comprehensive list of constraints. We identity constraints based on the relation between users and roles, between roles and permission on records, between users and permission on records, and between users, roles, and permission on records. Then, we use a general purpose theorem prover tool called Prover9 for proving the satisfaction of constraints.