Analyzing and managing role-based access control policies

Today, more and more sensitive data is stored on computer systems; security-critical business processes are mapped to their digital counterparts. This situation applies to institutes that have different security requirements, such as the healthcare industry, digital government, and financial service institutes. Authorization constraints help the policy architect design and express higher level organizational rules. Although the Importance of authorization constraints has been addressed in the literature, a systematic way to verify and validate authorization constraints does not exist. In this paper, we specify both nontemporal and history-based authorization constraints in the Object Constraint Language (OCL) and first-order linear temporal logic (LTL). Based upon these specifications, we attempt to formally verify role-based access control policies with the help of a theorem prover and to validate policies with the UML-based Specification Environment (USE) system, a validation tool for OCL constraints. We also describe an authorization engine, which supports the enforcement of authorization constraints.