| 摘要 | 第1-4页 |
| Abstract | 第4-6页 |
| 第一章 绪论 | 第6-10页 |
| ·安全协议简介 | 第6-7页 |
| ·研究的背景 | 第7-8页 |
| ·研究的内容和意义 | 第8-9页 |
| ·本文的组织和结构 | 第9-10页 |
| 第二章 鉴别协议 | 第10-22页 |
| ·鉴别的基本知识 | 第10-12页 |
| ·鉴别协议的介绍 | 第12-16页 |
| ·鉴别协议的攻击 | 第16-22页 |
| 第三章 模型检测技术 | 第22-32页 |
| ·形式化方法介绍 | 第22-24页 |
| ·模型检测概述 | 第24-26页 |
| ·线性时序逻辑（LTL） | 第26-29页 |
| ·模型检测器NuSMV | 第29-32页 |
| 第四章 鉴别协议的分析及设计 | 第32-50页 |
| ·鉴别协议分析的形式化方法 | 第32-35页 |
| ·鉴别协议的建模 | 第35-36页 |
| ·改进的 Helsinki 协议的验证 | 第36-42页 |
| ·一种新的鉴别协议的设计方法 | 第42-45页 |
| ·Test 协议的设计及其验证 | 第45-49页 |
| ·进一步的讨论 | 第49-50页 |
| 第五章 结束语 | 第50-51页 |
| 致谢 | 第51-52页 |
| 参考文献 | 第52-55页 |
| 研究成果 | 第55-56页 |