| 具有冲突约束的RBAC模型的形式化规范与证明 |
| |
| 引用本文： | 袁春阳,贺也平,何建波,周洲仪.具有冲突约束的RBAC模型的形式化规范与证明[J].计算机研究与发展,2006,43(Z2). |
| |
| 作者姓名： | 袁春阳 贺也平 何建波 周洲仪 |
| |
| 基金项目： | 国家重点基础研究发展计划(973计划);国家高技术研究发展计划(863计划);国家自然科学基金 |
| |
| 摘 要： | 在实际应用"基于角色的访问控制"(RBAC)模型时,经常遇到由于责任分离等策略而引起的冲突问题,如权限间的互斥等.访问控制操作应满足某些约束条件,以避免冲突的存在.但这些冲突关系相当复杂,如何检测出冲突问题是模型安全实施的重要保证.借助Z语言,提出了基于状态的RBAC形式化模型,对状态转换函数进行了形式化规范,描述了操作的具体内容和应满足的冲突约束条件.根据安全不变量给出了安全性定理,分别进行数学的和形式化的证明.最后,通过实例分析,说明在实际系统中,如何形式化规约和验证RBAC系统并检测出冲突问题,从而为今后使用RBAC模型开发具有高安全保证的系统提供了一种形式化规范和证明方法.
|
| 关 键 词： | 基于角色的访问控制 形式化规范和证明 责任分离 冲突约束 Z语言 |
Formal Specification and Proof of the RBAC Model with Constraints of Conflicts |
| |
| Yuan Chunyang,He Yeping,He Jianbo,Zhou Zhouyi.Formal Specification and Proof of the RBAC Model with Constraints of Conflicts[J].Journal of Computer Research and Development,2006,43(Z2). |
| |
| Authors: | Yuan Chunyang He Yeping He Jianbo Zhou Zhouyi |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 万方数据 等数据库收录！ |
|
