| 摘要 | 第1-4页 |
| ABSTRACT | 第4-10页 |
| 1 绪论 | 第10-25页 |
| ·网络安全概述 | 第10-11页 |
| ·密码学基础 | 第11-14页 |
| ·密码学概述 | 第11-12页 |
| ·对称密码体制 | 第12-13页 |
| ·非对称密码体制 | 第13-14页 |
| ·安全协议理论基础 | 第14-16页 |
| ·安全协议概念 | 第14-15页 |
| ·安全协议的分类 | 第15-16页 |
| ·安全协议系统模型 | 第16页 |
| ·安全协议形式化方法概述 | 第16-23页 |
| ·安全协议形式化方法的发展过程简述 | 第17-18页 |
| ·基于推理的结构性方法 | 第18-20页 |
| ·基于攻击的结构性方法 | 第20-22页 |
| ·基于证明的结构性方法 | 第22-23页 |
| ·论文主要工作 | 第23页 |
| ·论文结构 | 第23-24页 |
| ·本章小结 | 第24-25页 |
| 2 SVO 逻辑方法 | 第25-37页 |
| ·SVO 逻辑符号定义 | 第25-26页 |
| ·SVO 逻辑方法原理 | 第26-28页 |
| ·SVO 逻辑语言 | 第26页 |
| ·SVO 逻辑系统 | 第26-27页 |
| ·SVO 逻辑分析方法和步骤 | 第27-28页 |
| ·SVO 逻辑分析目标 | 第28页 |
| ·对SVO 逻辑方法的改进 | 第28-35页 |
| ·对SVO 逻辑的扩展 | 第28-29页 |
| ·对SVO 逻辑认证目标缺陷的分析和改进 | 第29-33页 |
| ·应用改进后的SVO 逻辑方法分析MAKAP-2 协议 | 第33-35页 |
| ·本章小结 | 第35-37页 |
| 3 STRAND SPACE 理论及其验证模型 | 第37-55页 |
| ·STRAND SPACE 理论基础 | 第37-42页 |
| ·基本概念 | 第37-40页 |
| ·消息项和密码运算 | 第40页 |
| ·自由性假设 | 第40-41页 |
| ·攻击者模型 | 第41页 |
| ·理想和诚实 | 第41-42页 |
| ·认证测试方法 | 第42-45页 |
| ·元素 | 第43页 |
| ·可入侵密钥集和安全密钥集 | 第43页 |
| ·认证测试 | 第43-45页 |
| ·STRAND SPACE 模型中的DIFFIE-HELLMAN 密钥交换机制 | 第45-50页 |
| ·代数学扩展 | 第45-47页 |
| ·攻击者行为扩展 | 第47页 |
| ·安全属性 | 第47页 |
| ·串空间中基于D-H 模型协议的认证测试方法扩展 | 第47-50页 |
| ·用STRAND SPACE 方法证明基于DH 问题的认证协议 | 第50-54页 |
| ·正确性概念 | 第50页 |
| ·一个基于DH 问题的相互认证协议 | 第50-52页 |
| ·用strand space 方法分析MA 协议 | 第52-53页 |
| ·对MA 协议的未知共享密钥攻击及改进 | 第53-54页 |
| ·本章小结 | 第54-55页 |
| 4 可相互认证的密钥协商协议设计与分析 | 第55-61页 |
| ·可相互认证的密钥协商协议MAKAP-3 | 第55-56页 |
| ·MAKAP-3 协议描述 | 第55页 |
| ·MAKAP-3 协议性能分析 | 第55-56页 |
| ·用改进的SVO 逻辑方法分析MAKAP-3 协议 | 第56-58页 |
| ·用扩展的STRAND SPACE 方法分析MAKAP-3 协议 | 第58-60页 |
| ·本章小结 | 第60-61页 |
| 5 总结与展望 | 第61-63页 |
| ·总结 | 第61页 |
| ·研究展望 | 第61-63页 |
| 致谢 | 第63-64页 |
| 参考文献 | 第64-69页 |
| 附录： | 第69页 |
| 攻读硕士学位期间发表的论文 | 第69页 |
| 参加科研项目情况 | 第69页 |
