Automated Verification Of Role-Based Access Control Policies Constraints Using Prover9
This work addresses the need for reliable constraint verification in RBAC systems, which is crucial for security in organizations managing sensitive records, but it is incremental as it applies existing theorem-proving tools to a known bottleneck.
The paper tackles the problem of verifying constraints in role-based access control (RBAC) policies, which is time-consuming and error-prone, by proposing a first-order logic theory for specification and using the Prover9 theorem prover for automated verification, resulting in an automated approach that reduces manual effort.
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.