| 摘要 | 第1-4页 |
| ABSTRACT | 第4-9页 |
| 第1章 引言 | 第9-12页 |
| ·研究背景 | 第9页 |
| ·安全协议的发展及国内外研究现状 | 第9-10页 |
| ·本人主要工作 | 第10-11页 |
| ·论文组织结构 | 第11-12页 |
| 第2章 安全协议 | 第12-18页 |
| ·密码协议 | 第12-13页 |
| ·密码协议的安全属性 | 第12页 |
| ·密码协议分类 | 第12-13页 |
| ·密码协议的安全性分析 | 第13页 |
| ·安全协议的形式化方法 | 第13-16页 |
| ·逻辑推理 | 第14-15页 |
| ·定理证明 | 第15页 |
| ·模型检测 | 第15-16页 |
| ·安全协议的非形式化分析 | 第16-18页 |
| 第3章 模型检测技术 | 第18-23页 |
| ·模型检测基本原理 | 第18页 |
| ·模型检测工具SPIN | 第18-21页 |
| ·SPIN工作原理及特征 | 第18-19页 |
| ·基于SPIN的协议分析 | 第19-21页 |
| ·Promela建模 | 第21-23页 |
| 第4章 基于SPIN的SSL 3.0握手协议模型检测 | 第23-30页 |
| ·SSL3.0握手协议简介 | 第23页 |
| ·建立SSL3.0握手协议的Promela模型 | 第23-30页 |
| ·诚信主体建模 | 第26-27页 |
| ·攻击者建模 | 第27-28页 |
| ·LTL描述协议性质 | 第28-29页 |
| ·分析及验证 | 第29-30页 |
| 第5章 网络安全协议验证系统 | 第30-42页 |
| ·系统平台搭建 | 第30-33页 |
| ·系统功能介绍 | 第30-31页 |
| ·系统PDL语言描述及数据输入规则 | 第31-33页 |
| ·平台设计与实现 | 第33-37页 |
| ·设计类图描述 | 第33页 |
| ·SSL3.0握手协议的PDL描述 | 第33-35页 |
| ·系统流程图及实现 | 第35-37页 |
| ·搜索优化算法 | 第37-42页 |
| ·协议主体建模算法步骤 | 第38-40页 |
| ·改进的攻击者建模算法步骤 | 第40-42页 |
| 第6章 静态分析技术在安全协议中的应用 | 第42-51页 |
| ·静态分析技术基本原理 | 第42页 |
| ·NS公钥认证协议分析 | 第42-46页 |
| ·NS协议简介 | 第42-43页 |
| ·协议实例模型 | 第43页 |
| ·静态分析结果 | 第43-46页 |
| ·TMN协议分析 | 第46-51页 |
| ·TMN协议简介 | 第46-47页 |
| ·TMN协议实例模型 | 第47页 |
| ·静态分析结果 | 第47-51页 |
| 第7章 结论与展望 | 第51-53页 |
| ·结论 | 第51页 |
| ·进一步工作的方向 | 第51-53页 |
| 致谢 | 第53-54页 |
| 参考文献 | 第54-57页 |
| 攻读学位期间的研究成果 | 第57页 |