Dynamic Access Control Policies - Specification and Verification
Date
2012Abstract
Security requirements deal with the protection of assets against unauthorized access (disclosure
or modification) and their availability to authorized users. Temporal constraints of history-based
access control policies are difficult to express naturally in traditional policy languages. We propose
a compositional formal framework for the specification and verification of temporal access control
policies for security critical systems in which history-based policies and other temporal constraints
can be expressed. In particular, our framework allows for the specification of policies that can change
dynamically in response to time or events enabling dynamic reconfiguration of the access control
mechanisms. The framework utilizes a single well-defined formalism, interval temporal logic, for
defining the semantics of these policies and to reason about them.We illustrate our approach with a
detailed case study of an electronic paper submission system showing the compositional verification
of their safety, liveness and information flow properties.
Description
Citation : Janicke, H. et al. (2012) Dynamic Access Control Policies - Specification and Verification. The Computer Journal, 56 (4), pp. 440-463
Research Group : Software Technology Research Laboratory (STRL)
Research Institute : Cyber Technology Institute (CTI)
Peer Reviewed : Yes