Today more and more security-relevant data is stored on computer systems; security-critical business processes are mapped to their digital counterparts. This situation applies to various domains such as health care industry, digital government, and financial service institutes requiring that different security requirements must be fulfilled. Authorization constraints can help the policy architect design and express higher-level organizational rules. Although the importance of authorization constraints has been addressed in the literature, there does not exist a systematic way to verify and validate authorization constraints. In this paper, we specify both non-temporal 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 USE system, a validation to...