关键词: 基于属性的访问控制, 模型检测, 覆盖性验证, 完整性验证

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