Specifying and enforcing constraints in dynamic access control policies

Constraints in access control models are used to organize access privileges in order to avoid fraudulent situations. Ensuring that the constraints are satisfied during the evolution of the system is an important issue. Thus, there is a need to have a formal reasoning language in order to express the constraints policy and to prove that the constraints are always satisfied. In this work, we propose a formal language based on the deontic logic of actions and situation calculus. The proposed language is easy to use to specify various constraints mentioned in the literature. In addition, we formally specify the condition to prove that the system specification is secure with respect to the access control requirements.