| 摘要 | 第1-7页 |
| Abstract | 第7-12页 |
| 图目录 | 第12-13页 |
| 表目录 | 第13-14页 |
| 第一章 绪论 | 第14-28页 |
| ·研究背景 | 第14-18页 |
| ·信息系统面临的安全威胁 | 第15-18页 |
| ·操作系统面临的安全威胁 | 第15-16页 |
| ·网络系统面临的安全威胁 | 第16-18页 |
| ·研究现状 | 第18-25页 |
| ·访问控制策略 | 第19-22页 |
| ·自主访问控制策略 | 第19-20页 |
| ·强制访问控制策略 | 第20-22页 |
| ·安全模型 | 第22-23页 |
| ·Bell-Lapadula模型 | 第22-23页 |
| ·Biba模型 | 第23页 |
| ·其他模型 | 第23页 |
| ·安全协议形式化分析方法 | 第23-24页 |
| ·基于非干扰的信息流分析方法 | 第24-25页 |
| ·研究目的和方案 | 第25-26页 |
| ·论文结构 | 第26-28页 |
| 第二章 信息流分析的一般方法 | 第28-51页 |
| ·安全进程代数SPA | 第28-35页 |
| ·SPA语法 | 第28-30页 |
| ·SPA的操作语义和等价关系 | 第30-34页 |
| ·值传递SPA | 第34-35页 |
| ·非干扰模型 | 第35-38页 |
| ·非确定系统中的信息流安全性质 | 第38-44页 |
| ·基于路径等价的性质 | 第38-40页 |
| ·基于观察等价的性质 | 第40-44页 |
| ·BNDC性质的进一步分析 | 第44-50页 |
| ·坚持BNDC | 第44-46页 |
| ·BNDC的一般化分析 | 第46-48页 |
| ·强BNDC、前进P_PBNDC | 第48-50页 |
| ·小结 | 第50-51页 |
| 第三章 概率系统中的信息流安全验证 | 第51-75页 |
| ·概率系统安全问题 | 第51-53页 |
| ·概率安全进程代数PSPA | 第53-58页 |
| ·生成-反应转换系统 | 第53-54页 |
| ·PSPA的语法 | 第54-56页 |
| ·PSPA的操作语义 | 第56-58页 |
| ·概率进程间的观察等价 | 第58-60页 |
| ·概率系统的信息流安全性质 | 第60-70页 |
| ·概率非干扰 | 第60-61页 |
| ·概率互拟组合不可演绎性质 | 第61-63页 |
| ·持久PBNDC | 第63-68页 |
| ·持久PBNDC的定义 | 第63-64页 |
| ·动态环境下的P_PBNDC性质 | 第64-65页 |
| ·P_PBNDC性质的讨论 | 第65-68页 |
| ·强PBNDC | 第68-69页 |
| ·组合PBNDC | 第69-70页 |
| ·实际系统的例子 | 第70-74页 |
| ·小结 | 第74-75页 |
| 第四章 基于信息流分析的安全协议验证 | 第75-100页 |
| ·安全协议中的非干扰 | 第75-82页 |
| ·安全协议分析 | 第75-77页 |
| ·安全协议中的非干扰 | 第77-79页 |
| ·NDC的一般化框架 | 第79-82页 |
| ·CryptoSPA演算 | 第82-86页 |
| ·CryptoSPA演算的语法 | 第82-84页 |
| ·CryptoSPA演算的语义 | 第84-86页 |
| ·环境敏感语义 | 第86-90页 |
| ·环境敏感标签转换系统 | 第86-87页 |
| ·配置间的路径和弱互拟等价 | 第87-88页 |
| ·进程间的环境敏感等价 | 第88-90页 |
| ·安全协议性质分析 | 第90-99页 |
| ·环境敏感的GNDC | 第90-91页 |
| ·组合上的不可演绎性质 | 第91-94页 |
| ·ESGNDC_(?)~α框架下的协议安全性质分析 | 第94-96页 |
| ·机密性分析 | 第95页 |
| ·一致性分析 | 第95-96页 |
| ·公平性分析 | 第96页 |
| ·一个安全协议分析的实例 | 第96-99页 |
| ·小结 | 第99-100页 |
| 第五章 安全性质的证明技术 | 第100-114页 |
| ·使用模型检查技术验证安全性质 | 第100-109页 |
| ·模态μ演算和方程μ演算 | 第101-105页 |
| ·模态μ演算 | 第101-104页 |
| ·方程μ演算 | 第104-105页 |
| ·进程的特征方程系统 | 第105-106页 |
| ·部分模型检查 | 第106-107页 |
| ·验证BNDC性质 | 第107-108页 |
| ·一般化的特征方程系统 | 第108-109页 |
| ·ESGNDC_(?)~α性质的验证 | 第109-113页 |
| ·环境敏感弱互拟语义的一般化分析 | 第110-112页 |
| ·s_BNDC~σ性质分析 | 第112-113页 |
| ·Strong BNDC~σ性质 | 第112页 |
| ·Progressing P_PBNDC~σ性质 | 第112-113页 |
| ·小结 | 第113-114页 |
| 第六章 结束语 | 第114-118页 |
| ·论文工作总结 | 第114-116页 |
| ·概率系统中的信息流安全性质 | 第115页 |
| ·基于环境敏感非干扰的安全协议分析 | 第115-116页 |
| ·部分模型检查验证NDC类性质 | 第116页 |
| ·进一步的工作 | 第116-118页 |
| 参考文献 | 第118-129页 |
| 读博期间发表的论文 | 第129页 |
| 读博期间参加的科研项目 | 第129-131页 |
| 致谢 | 第131页 |