具有冲突约束的RBAC模型的形式化规范与证明  

Formal Specification and Proof of the RBAC Model with Constraints of Conflicts

作　　者：袁春阳[1,2] 贺也平[2] 何建波[1,2] 周洲仪[1,2] 

机构地区：[1]中国科学院软件研究所基础软件国家工程中心,北京100080 [2]中国科学院研究生院,北京100049

出　　处：《计算机研究与发展》2006年第z2期498-508,共11页Journal of Computer Research and Development

基　　金：国家"九七三"重点基础研究发展规划基金项目(G1999035802);国家"八六三"高技术研究发展计划基金项目(2002AA141080);国家自然科学基金项目(60073022,60373054)

摘　　要：在实际应用"基于角色的访问控制"(RBAC)模型时,经常遇到由于责任分离等策略而引起的冲突问题,如权限间的互斥等.访问控制操作应满足某些约束条件,以避免冲突的存在.但这些冲突关系相当复杂,如何检测出冲突问题是模型安全实施的重要保证.借助Z语言,提出了基于状态的RBAC形式化模型,对状态转换函数进行了形式化规范,描述了操作的具体内容和应满足的冲突约束条件.根据安全不变量给出了安全性定理,分别进行数学的和形式化的证明.最后,通过实例分析,说明在实际系统中,如何形式化规约和验证RBAC系统并检测出冲突问题,从而为今后使用RBAC模型开发具有高安全保证的系统提供了一种形式化规范和证明方法.

关 键 词：基于角色的访问控制 形式化规范和证明 责任分离 冲突约束 Z语言 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]