| 目录 | 第1-7页 |
| 摘要 | 第7-8页 |
| ABSTRACT | 第8-9页 |
| 第一章 绪论 | 第9-24页 |
| ·安全协议研究 | 第9-12页 |
| ·安全协议概念及分类 | 第9-10页 |
| ·安全协议的安全性质 | 第10-11页 |
| ·安全协议的缺陷及所受攻击 | 第11-12页 |
| ·典型安全协议分析验证方法 | 第12-17页 |
| ·基于逻辑推理的分析方法--BAN类逻辑 | 第12-13页 |
| ·定理证明方法(归纳证明、串空间、阶函数) | 第13-15页 |
| ·基于模型检测的方法 | 第15-16页 |
| ·模型检测与定理证明的混合方法—NRL协议分析器 | 第16页 |
| ·互模拟等价模型下的系统—SPI演算 | 第16-17页 |
| ·概率互模拟和安全协议分析的PPT-演算 | 第17页 |
| ·进程代数的研究进展及其在安全协议分析验证中的应用 | 第17-21页 |
| ·进程代数的研究进展 | 第17-20页 |
| ·进程代数在安全协议分析验证中应用 | 第20-21页 |
| ·论文研究目标 | 第21-22页 |
| ·通过研究要解决的问题 | 第21-22页 |
| ·研究目标 | 第22页 |
| ·本文主要内容 | 第22-24页 |
| 第二章 CSP安全协议分析方法 | 第24-42页 |
| ·CSP简介 | 第24-28页 |
| ·进程的表达 | 第24页 |
| ·基本定律及运算符号 | 第24-26页 |
| ·迹模型 | 第26-28页 |
| ·CSP安全协议模型分析 | 第28-36页 |
| ·模型中的数据类型 | 第28-29页 |
| ·模型中的事件 | 第29页 |
| ·模型中的结构 | 第29页 |
| ·模型中的进程 | 第29-31页 |
| ·并归网络 | 第31-32页 |
| ·实例化 | 第32页 |
| ·安全协议的安全性质 | 第32-36页 |
| ·基于CSP的安全协议建模 | 第36-40页 |
| ·执行进程 | 第36-39页 |
| ·说明进程 | 第39-40页 |
| ·CSP安全协议模型中存在的不足 | 第40-41页 |
| ·小结 | 第41-42页 |
| 第三章 数据独立技术 | 第42-52页 |
| ·一般的数据独立分析 | 第42页 |
| ·Roscoe的数据独立技术 | 第42-49页 |
| ·Roscoe的重要推论 | 第43-46页 |
| ·Roscoe重要推论的意义 | 第46-47页 |
| ·说明进程的约束 | 第47-49页 |
| ·保证数据独立技术使用的模型条件 | 第49-50页 |
| ·数据类型 | 第49页 |
| ·可信代理模型 | 第49-50页 |
| ·入侵者模型 | 第50页 |
| ·小结 | 第50-52页 |
| 第四章 基于数据独立技术的CSP协议模型设计 | 第52-65页 |
| ·扩展的CSP协议模型 | 第52-60页 |
| ·可信代理模型 | 第53-54页 |
| ·实例化 | 第54页 |
| ·Manager进程模型 | 第54-58页 |
| ·入侵者模型 | 第58页 |
| ·说明进程 | 第58-60页 |
| ·模型的正确性验证 | 第60-64页 |
| ·数据类型独立的验证 | 第61页 |
| ·可信代理进程的验证 | 第61-62页 |
| ·入侵者进程的验证 | 第62-63页 |
| ·Manager进程的验证 | 第63-64页 |
| ·小结 | 第64-65页 |
| 第五章 扩展CSP协议模型的应用 | 第65-85页 |
| ·CSP_M语言 | 第65-66页 |
| ·身份标识 | 第65页 |
| ·序列 | 第65-66页 |
| ·集合 | 第66页 |
| ·局部定义 | 第66页 |
| ·ProBE | 第66-67页 |
| ·FDR | 第67-71页 |
| ·工作原理 | 第67-68页 |
| ·FDR的提炼检测算法 | 第68-69页 |
| ·反例 | 第69-70页 |
| ·本章验证使用的提炼检测算法 | 第70-71页 |
| ·TMN协议的验证 | 第71-82页 |
| ·扩展的CSP_M脚本 | 第72-76页 |
| ·验证 | 第76-82页 |
| ·Otway-Rees协议的验证 | 第82-84页 |
| ·小结 | 第84-85页 |
| 结束语 | 第85-87页 |
| 致谢 | 第87-89页 |
| 参考文献 | 第89-93页 |
| 附录A TMN协议的CSP_M脚本 | 第93-119页 |
| 附录A1 TMN协议的CSP_M脚本 | 第93-105页 |
| 附录A2 TMN协议扩展的CSP_M脚本 | 第105-119页 |
| 附录B Otway-Rees协议的CSP_M脚本 | 第119-153页 |
| 附录B1 Otway-Rees协议的CSP_M脚本 | 第119-135页 |
| 附录B2 Otway-Rees协议扩展的CSP_M脚本 | 第135-153页 |
| 附录C 作者在学期间取得的学术成果 | 第153页 |
