Specification and Analysis of Dynamic Authorisation Policies
- Mo Becker
22nd IEEE Computer Security Foundations Symposium (CSF) |
Published by IEEE
This paper presents a language, based on transaction logic, for specifying dynamic authorisation policies, i.e., rules governing actions that may depend on and update the authorisation state. The language is more expressive than previous dynamic authorisation languages, featuring conditional bulk insertions and retractions of authorisation facts, non-monotonic negation, and nested action definitions with transactional execution semantics. Two complementary policy analysis methods are also presented, one based on AI planning for verifying reachability properties in finite domains, and the second based on automated theorem proving, for checking policy invariants that hold for all sequences of actions and in arbitrary, including infinite, domains. The combination of both methods can analyse a wide range of security properties, including safety, availability and containment.
© 2008 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.http://www.ieee.org/