| 摘要 | 第1-5页 |
| ABSTRACT | 第5-8页 |
| 第一章 绪论 | 第8-13页 |
| ·引言 | 第8-9页 |
| ·安全协议的介绍 | 第9-11页 |
| ·背景 | 第9-10页 |
| ·安全协议的类型 | 第10页 |
| ·安全协议的性质 | 第10-11页 |
| ·安全协议的漏洞 | 第11页 |
| ·本文主要工作 | 第11-13页 |
| 第二章 安全协议的形式化方法 | 第13-16页 |
| ·形式化方法的背景 | 第13页 |
| ·形式化分析的三种方法 | 第13-15页 |
| ·几种已有的形式化自动分析工具 | 第15-16页 |
| 第三章 GSPM 的建模及其改进. | 第16-26页 |
| ·GSPM 的概述. | 第16-20页 |
| ·GSPM 的消息空间 | 第16-17页 |
| ·GSPM 的语法和语义 | 第17-18页 |
| ·实例分析 | 第18-20页 |
| ·GSPM 基于类型攻击漏洞的改进 | 第20-26页 |
| ·类型攻击漏洞的描述 | 第20-22页 |
| ·针对类型缺陷问题对GSPM 进行的改进 | 第22-24页 |
| ·实例研究 | 第24-26页 |
| 第四章 基于GSPM 的安全协议验证算法 | 第26-34页 |
| ·消息的推理算法 | 第26-28页 |
| ·如何描述安全协议的性质 | 第28-31页 |
| ·线性时序逻辑 | 第28-30页 |
| ·用线性时序逻辑描述安全协议性质 | 第30-31页 |
| ·验证协议性质的算法 | 第31-34页 |
| 第五章 安全协议验证算法及其工具的实现 | 第34-46页 |
| ·工具概述 | 第34-35页 |
| ·安全协议建模的实现 | 第35-37页 |
| ·状态空间搜索树的结构设计 | 第37-39页 |
| ·工具演示 | 第39-43页 |
| ·结果分析 | 第43-46页 |
| 第六章 总结与展望 | 第46-48页 |
| 参考文献 | 第48-51页 |
| 附录: 安全协议数据结构和验证算法核心代码(C#) | 第51-59页 |
| 致谢 | 第59-60页 |
| 攻读学位期间发表的学术论文 | 第60页 |