Timed constraint programming: A declarative approach to usage control

Abstract

This paper focuses on policy languages for (role-based) access control [14, 32], especially in their modern incarnations in the form of trust-management systems [9] and usage control [30, 31]. Any (declarative) approach to access control and trust management has to address the following issues: Explicit denial, inheritance, and overriding, and History-sensitive access control 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. Copyright 2005 ACM.