Model Checking Agent Knowledge in Dynamic Access Control Policies
Model Checking Agent Knowledge in Dynamic Access Control Policies
复制标题
动态访问控制策略中的模型检查代理知识
DOI：
10.1007/978-3-642-36742-7_31
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
M. Ryan
中科院分区：
文献类型：
--
作者：
M. Koleini;Eike Ritter;M. Ryan
在本文中，我们开发了一种基于解释系统的建模技术，以验证访问控制策略的时间认知属性。这种方法使我们能够检测信息流的动态策略中的漏洞，通过验证阅读和推理系统信息所获得的代理的知识。为了克服实际的限制状态爆炸模型检查的时间认知属性，我们引入了一种新的抽象和细化技术的时间认知安全属性在ACTLK（ACTL知识模态K）和一类有趣的属性，不属于这一类。
In this paper, we develop a modeling technique based on interpreted systems in order to verify temporal-epistemic properties over access control policies. This approach enables us to detect information flow vulnerabilities in dynamic policies by verifying the knowledge of the agents gained by both reading and reasoning about system information. To overcome the practical limitations of state explosion in model-checking temporal-epistemic properties, we introduce a novel abstraction and refinement technique for temporal-epistemic safety properties in ACTLK (ACTL with knowledge modality K) and a class of interesting properties that does fall in this category.
DOI：
10.1145/1558109.1558144
发表时间：
2009-05
期刊：
--
影响因子：
--
作者：
F. Russo
通讯作者：
F. Russo