| 摘要 | 第1-6页 |
| Abstract | 第6-10页 |
| 第1章 引言 | 第10-15页 |
| ·课题的研究背景及意义 | 第10-11页 |
| ·安全协议形式化分析方法 | 第11-13页 |
| ·本文的主要研究内容 | 第13页 |
| ·文章安排 | 第13-15页 |
| 第2章 形式化分析方法基础 | 第15-25页 |
| ·基本术语 | 第15页 |
| ·串和串空间 | 第15-17页 |
| ·丛和因果次序 | 第17-19页 |
| ·子项 | 第19-20页 |
| ·入侵者模型 | 第20-21页 |
| ·入侵者初始密钥集 | 第20页 |
| ·入侵者串 | 第20-21页 |
| ·协议分析举例 | 第21-24页 |
| ·协议串空间 | 第21-22页 |
| ·协议分析 | 第22-24页 |
| ·本章小结 | 第24-25页 |
| 第3章 串空间理论的发展 | 第25-35页 |
| ·诚实与理想 | 第25-26页 |
| ·认证测试理论 | 第26-29页 |
| ·基本概念 | 第26-27页 |
| ·认证测试方法分类 | 第27-28页 |
| ·认证测试方法步骤 | 第28-29页 |
| ·改进型Otway-Rees 协议分析 | 第29-34页 |
| ·改进后的Otway-Rees 协议 | 第29-30页 |
| ·改进型Otway-Rees 协议的串空间模型分析 | 第30-34页 |
| ·本章小结 | 第34-35页 |
| 第4章 串空间理论的扩展 | 第35-42页 |
| ·串空间模型扩展的必要性 | 第35页 |
| ·串空间模型扩展 | 第35-38页 |
| ·消息项扩展 | 第36页 |
| ·自由假设扩展 | 第36-37页 |
| ·子项关系扩展 | 第37页 |
| ·攻击者模型扩展 | 第37-38页 |
| ·诚实与理想的扩展 | 第38-39页 |
| ·认证测试理论 | 第39-41页 |
| ·基本概念扩展 | 第39页 |
| ·认证测试方法的扩展 | 第39-41页 |
| ·认证测试规则的扩展 | 第41页 |
| ·本章小结 | 第41-42页 |
| 第5章 应用实例分析 | 第42-51页 |
| ·一种电子邮件传输的非否认协议 | 第42-45页 |
| ·协议及协议中的假设与说明 | 第42-43页 |
| ·协议的仲裁 | 第43页 |
| ·协议的串空间模型 | 第43-45页 |
| ·用扩展后的认证测试方法分析协议 | 第45-47页 |
| ·协议的验证 | 第45-47页 |
| ·用扩展后的诚实理想分析协议 | 第47-50页 |
| ·本章小结 | 第50-51页 |
| 总结与展望 | 第51-53页 |
| 参考文献 | 第53-56页 |
| 致谢 | 第56-57页 |
| 攻读学位期间取得学术成果 | 第57页 |