Security Analysis of Administrative Role-Based Access Control Policies with Contextual Information

In many ubiquitous systems, Role-based Access Control (RBAC) is often used to restrict system access to authorized users. Spatial-Temporal Role-Based Access Control (STRBAC) is an extension of RBAC with contextual information (such as time and space) and has been adopted in real world applications. In a large organization, the RBAC policy may be complex and managed by multiple collaborative administrators to satisfy the evolving needs of the organization. Collaborative administrative actions may interact in unintended ways with each other's that may result in undesired effects to the security requirement of the organization. Analysis of these RBAC security concerns have been studied, especially with the Administrative Role-Based Access Control (ARBAC97). However, the analysis of its extension with contextual information, e.g., STRBAC, has not been considered in the literature. In this paper, we introduce a security analysis technique for the safety of Administrative STRBAC (ASTRBAC) Policies. We leverage First-Order Logic and Symbolic Model Checking (SMT) by translating ASTRBAC policy to decidable reachability problems. An extensive experimental evaluation confirms the correctness of our proposed solution, which supports finite ASTRBAC policies analysis without prior knowledge about the number of users.