| 独创性声明 | 第1页 |
| 关于论文使用授权的说明 | 第3-4页 |
| 摘要 | 第4-6页 |
| ABSTRACT | 第6-8页 |
| 目录 | 第8-12页 |
| 图表目录 | 第12-13页 |
| 第一章 引言 | 第13-27页 |
| ·关键定义 | 第14-15页 |
| ·从军事安全策略到商务安全策略 | 第15-18页 |
| ·访问控制与安全策略、安全模型、安全机制 | 第18-20页 |
| ·访问控制、安全策略、安全模型及安全机制 | 第18-19页 |
| ·访问控制类型 | 第19-20页 |
| ·商务安全策略实现机制与军事安全策略实现机制比较 | 第20-22页 |
| ·军事安全策略实现机制 | 第20页 |
| ·商务安全策略实现机制 | 第20-21页 |
| ·军事安全策略和商务安全策略实现机制之间的区别与联系 | 第21-22页 |
| ·商务安全策略制模和应用 | 第22-24页 |
| ·安全模型是研究安全策略的重要手段 | 第22-23页 |
| ·商务安全策略研究所处困局及其原因分析 | 第23-24页 |
| ·商务安全策略模型开发中的形式规范和分析 | 第24页 |
| ·论文研究目标 | 第24-25页 |
| ·论文组织结构 | 第25-27页 |
| 第二章 安全策略与安全策略模型 | 第27-45页 |
| ·安全策略 | 第27-29页 |
| ·安全策略模型 | 第29-32页 |
| ·安全策略模型 | 第29页 |
| ·安全策略模型的目标 | 第29-31页 |
| ·安全策略模型在软件生命周期中所处阶段 | 第31页 |
| ·安全策略模型的性质 | 第31-32页 |
| ·理解制模 | 第32-38页 |
| ·基本元素 | 第32-34页 |
| ·有效表示 | 第34-36页 |
| ·理解计算框架 | 第36-38页 |
| ·安全制模 | 第38-42页 |
| ·安全制模 | 第38-39页 |
| ·SPM和普通模型之间的异同 | 第39-42页 |
| ·基于状态机的安全策略模型开发步骤 | 第42-44页 |
| ·本章小结 | 第44-45页 |
| 第三章 商务安全策略形式框架 | 第45-67页 |
| ·商务安全目标 | 第45-46页 |
| ·CLARK-WILSON完整性安全策略 | 第46-49页 |
| ·商务安全策略形式框架 | 第49-62页 |
| ·问题分析 | 第49-50页 |
| ·商务安全策略形式制模原理 | 第50-52页 |
| ·模型元素 | 第52-54页 |
| ·辅助函数 | 第54-55页 |
| ·模型不变量 | 第55-56页 |
| ·模型约束条件 | 第56-57页 |
| ·模型规则(状态转移函数) | 第57-62页 |
| ·商务安全策略框架模型的安全性 | 第62-64页 |
| ·安全性分析 | 第63页 |
| ·FB-FCSM是Clark-Wilson完整性策略的精化 | 第63-64页 |
| ·本章小结 | 第64-67页 |
| 第四章 商务安全策略框架特性研究 | 第67-101页 |
| ·企业级商务安全策略框架 | 第67-75页 |
| ·大型企业的结构和IT应用特征 | 第68页 |
| ·基于角色的存取控制机制 | 第68-70页 |
| ·管理RBAC | 第70-74页 |
| ·企业级商务安全策略框架 | 第74-75页 |
| ·商务安全策略框架的兼容性研究 | 第75-80页 |
| ·多策略兼容原理 | 第75-76页 |
| ·多安全级事务 | 第76-77页 |
| ·层次关系 | 第77-78页 |
| ·任务 | 第78-79页 |
| ·基于任务的职责隔离特性 | 第79-80页 |
| ·多策略安全监视框架 | 第80-99页 |
| ·多策略安全监视框架原理 | 第80-81页 |
| ·相关工作 | 第81-82页 |
| ·基于多策略的安全监视框架(MP-SMF) | 第82-85页 |
| ·安全策略关系模式 | 第85-86页 |
| ·Bell-LaPadula机密性安全策略关系模式 | 第86-88页 |
| ·Clark-Wilson完整性安全策略关系模式 | 第88-97页 |
| ·Bell-LaPadual和Clark-Wilson策略关系模式在MP-SMF中的应用 | 第97页 |
| ·分析 | 第97-99页 |
| ·本章小结 | 第99-101页 |
| 第五章 商务安全策略形式规范 | 第101-123页 |
| ·规范和形式规范 | 第101-102页 |
| ·形式描述语言——Z语言 | 第102-103页 |
| ·安全策略模型及其形式规范 | 第103-104页 |
| ·安全策略模型的形式规范方法 | 第104-107页 |
| ·安全策略规范的内容 | 第104-105页 |
| ·构造安全策略规范 | 第105-107页 |
| ·商务安全策略规范的基本数据类型和模型组件 | 第107-111页 |
| ·商务安全不变量和安全状态 | 第111-114页 |
| ·商务系统状态 | 第111-112页 |
| ·商务安全状态不变量 | 第112-113页 |
| ·商务安全系统状态 | 第113-114页 |
| ·商务安全系统初始状态 | 第114页 |
| ·商务安全约束和商务安全规则 | 第114-118页 |
| ·商务安全约束 | 第114-116页 |
| ·规则类型和参数表 | 第116-117页 |
| ·商务安全规则 | 第117-118页 |
| ·商务安全系统 | 第118-121页 |
| ·通用数学系统 | 第118-119页 |
| ·Z形式通用抽象系统 | 第119-120页 |
| ·商务安全系统 | 第120-121页 |
| ·本章小结 | 第121-123页 |
| 第六章 商务安全策略形式分析 | 第123-149页 |
| ·形式方法 | 第123-133页 |
| ·形式方法定义 | 第123-124页 |
| ·形式方法类型 | 第124-125页 |
| ·形式方法应用现状 | 第125-126页 |
| ·Z/EVES形式验证系统 | 第126-127页 |
| ·Isabelle/HOL形式验证系统 | 第127-129页 |
| ·GVE形式验证系统 | 第129-131页 |
| ·Z/EVES、Isabelle/HOL及GVE比较 | 第131-133页 |
| ·Z/EVES定理证明机制 | 第133-134页 |
| ·化简 | 第133页 |
| ·重写 | 第133-134页 |
| ·推理 | 第134页 |
| ·用户控制 | 第134页 |
| ·商务安全策略规范分析 | 第134-136页 |
| ·语法和类型错误检查 | 第134-135页 |
| ·域错误检查 | 第135页 |
| ·非一致错误检查 | 第135-136页 |
| ·商务安全策略规范研究 | 第136-139页 |
| ·模式展开 | 第137页 |
| ·前置条件计算 | 第137-138页 |
| ·初始状态存在性分析 | 第138-139页 |
| ·安全定理开发及证明 | 第139-145页 |
| ·原理 | 第139-140页 |
| ·技术路线 | 第140-141页 |
| ·证明过程 | 第141-145页 |
| ·证明结果 | 第145页 |
| ·经验和教训 | 第145-147页 |
| ·本章小结 | 第147-149页 |
| 第七章 结论 | 第149-151页 |
| ·论文的主要成果 | 第149-150页 |
| ·研究展望 | 第150-151页 |
| 参考文献 | 第151-163页 |
| 附录A Z语言简介 | 第163-169页 |
| 附录B 词汇表 | 第169-174页 |
| 作者攻读博士学位期间发表的学术论文 | 第174-175页 |
| 致谢 | 第175页 |