具有冲突约束的RBAC模型的形式化规范与证明
在实际应用”基于角色的访问控制”(RBAC)模型时,经常遇到由于责任分离等策略而引起的冲突问题,如权限间的互斥等.访问控制操作应满足某些约束条件,以避免冲突的存在.但这些冲突关系相当复杂,如何检测出冲突问题是模型安全实施的重要保证.借助Z语言,提出了基于状态的RBAC形式化模型,对状态转换函数进行了形式化规范,描述了操作的具体内容和应满足的冲突约束条件.根据安全不变量给出了安全性定理,分别进行数学的和形式化的证明.最后,通过实例分析,说明在实际系统中,如何形式化规约和验证RBAC系统并检测出冲突问题,从而为今后使用RBAC模型开发具有高安全保证的系统提供了一种形式化规范和证明方法.
基于角色的访问控制 形式化规范和证明 责任分离 冲突约束 Z语言
袁春阳 贺也平 何建波 周洲仪
中国科学院软件研究所基础软件国家工程中心,北京,100080;中国科学院研究生院,北京,100049 中国科学院研究生院,北京,100049
国内会议
河北保定
中文
498-508
2006-10-21（万方平台首次上网日期，不代表论文的发表时间）