Specification and Analysis of Dynamic Authorisation Policies
Specification and Analysis of Dynamic Authorisation Policies
复制标题
动态授权策略规范与分析
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Moritz Y. Becker
中科院分区：
文献类型：
--
作者：
Moritz Y. Becker
本文提出了一种基于事务逻辑的动态授权策略语言，管理可能取决于和更新授权状态的操作的规则。该语言比以前的动态授权语言更具表现力，具有条件批量插入和撤回授权事实，非单调否定和嵌套动作定义与事务执行语义。还提出了两种互补的政策分析方法，一种是基于人工智能规划，用于验证有限域中的可达性属性，第二种是基于自动定理证明，用于检查适用于所有动作序列和任意（包括无限）域的政策不变量。这两种方法的结合可以分析广泛的安全属性，包括安全性，可用性和包容性。
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.