计算机工程与应用2016，Vol.52Issue(18)：98-103,132,7.DOI:10.3778/j.issn.1002-8331.1410-0296
基于属性的访问控制策略的正确性验证
Verification of correctness of attribute based access control
摘要
Abstract
The attribute-based access control has bean used more and more widely, because it controls users and process to access system resources more accurate. However, it is necessary to ensure the correctness of policy, which can prevent illegal access to system resources. So an effective method must be developed to verify policies. In this paper, a method based on model checking is put forward, which can be used to check the coverage and completeness of rules. The main idea is to regard rule set and its variation as models, and then describe the properties with modal logic formulas. It uses model checking algorithm to check the logic formulas on models, which can help discover the fault of the model and deletion of rules. At the same time it analyzes the completeness of properties. Finally, it will call model checking algorithm again to verify fixed properties on fixed models. The case study shows that the coverage checking can find wrong rules effectively and the completeness checking can identify the integrity of rules. Since methods are based on model checking, they have some advantages of model checking such as automation, easy operation, reliable result et al.关键词
基于属性的访问控制/模型检测/覆盖性验证/完整性验证Key words
attribute based access control/model checking/coverage verification/completeness verification分类
信息技术与安全科学引用本文复制引用
吕江华,刘志锋,徐亚涛,周从华..基于属性的访问控制策略的正确性验证[J].计算机工程与应用,2016,52(18):98-103,132,7.基金项目
国家自然科学基金（No.61300228）。 （）
