| 摘要 | 第1-4页 |
| ABSTRACT | 第4-9页 |
| 第一章 绪言 | 第9-17页 |
| ·引言 | 第9-10页 |
| ·安全协议的原理与分类 | 第10-12页 |
| ·安全协议 | 第10-11页 |
| ·安全协议的类型 | 第11页 |
| ·安全性质 | 第11-12页 |
| ·安全协议形式化分析 | 第12-14页 |
| ·形式化分析的意义 | 第12-13页 |
| ·形式化分析概述 | 第13-14页 |
| ·安全协议形式化分析的自动工具 | 第14-15页 |
| ·本文主要工作 | 第15-17页 |
| 第二章 安全协议的六种漏洞 | 第17-22页 |
| ·身份认证漏洞 | 第17-18页 |
| ·假冒攻击漏洞 | 第18页 |
| ·保密数据泄漏漏洞 | 第18页 |
| ·新鲜性漏洞 | 第18-19页 |
| ·类型攻击漏洞 | 第19页 |
| ·攻击者不当得利漏洞 | 第19-22页 |
| 第三章 一般安全协议模型的增强 | 第22-37页 |
| ·一般安全协议模型（GSPM） | 第22-27页 |
| ·GSPM 的消息空间及消息推理原理 | 第22-24页 |
| ·GSPM 的语法和语义 | 第24页 |
| ·GSPM 中定义的安全性质 | 第24-25页 |
| ·利用GSPM 分析安全协议 | 第25-26页 |
| ·GSPM 的不足 | 第26-27页 |
| ·新鲜性漏洞的检测 | 第27-32页 |
| ·新鲜性问题的产生 | 第27-28页 |
| ·新鲜性的形式化定义 | 第28-30页 |
| ·实例研究 | 第30-32页 |
| ·类型攻击漏洞的检测 | 第32-37页 |
| ·类型攻击漏洞的产生 | 第32-33页 |
| ·针对类型缺陷问题对GSPM 进行的改进 | 第33-35页 |
| ·实例研究 | 第35-37页 |
| 第四章 安全协议自动验证工具GSPMC 的实现 | 第37-48页 |
| ·系统概述 | 第37-39页 |
| ·基于XML 的GSPM 语法解析 | 第39-40页 |
| ·消息推理的算法设计 | 第40-41页 |
| ·状态空间搜索树的结构设计 | 第41-43页 |
| ·安全性质的自动分析 | 第43-44页 |
| ·工具应用实例 | 第44-48页 |
| 第五章 总结与展望 | 第48-50页 |
| ·本文工作总结 | 第48页 |
| ·未来工作展望 | 第48-50页 |
| 参考文献 | 第50-54页 |
| 附录：GSPMC 的输入规范（XML SCHEMA） | 第54-61页 |
| 致谢 | 第61-62页 |
| 攻读学位期间发表的学术论文 | 第62-64页 |