To appear in PPDP 2005.
This paper focuses on policy languages for (role-based) access control, especially in their modern incarnations in the form of trust-management systems and usage control. Any (declarative) approach to access control and trust management has to address the following issues:
Our main contribution is a policy algebra, in the timed concurrent constraint programming paradigm, that uses a form of default constraint programming to address the first issue, and reactive computing to address the second issue.
The policy algebra is declarative --- programs can be viewed as imposing temporal constraints on the evolution of the system --- and supports equational reasoning. The validity of equations is established by coinductive proofs based on an operational semantics.
The design of the policy algebra supports reasoning about policies by a systematic combination of constraint reasoning and model checking techniques based on linear time temporal-logic. Our framework permits us to perform security analysis with dynamic state-dependent restrictions.