Abstract: This paper presents a rule set model which is used in access control systems and the corresponding model checking algorithm for loopholes which are brought by the rules in access control system. A method which search system states is used to determine if the goals can be achieved under the conditions that some permissions are given by rights. Corresponding strategies are output when the goals are achieved. Experimental results show that the algorithm is efficient in moderate systems.

Key words: access control system, model checking, transition

摘要： 针对访问控制系统规则存在漏洞问题，提出一个建立在系统读写规则集基础之上的访问控制系统规则集模型及相应的模型检测算法，通过对系统状态的遍历，判断目标在权限提供某些许可的情况下是否可完成，并在目标可完成的情况下输出相应的策略。实验结果证明，在中等规模的系统中该算法有效。

关键词: 访问控制系统, 模型检测, 变迁

CLC Number: 

• TP302