| 摘要 | 第1-4页 |
| Abstract | 第4-5页 |
| 目录 | 第5-7页 |
| 第一章 绪论 | 第7-17页 |
| 1．1 安全协议的背景及契机本概念 | 第7-8页 |
| 1．2 安全协议的安全性分析 | 第8-10页 |
| 1．3 安全协议的形式化分析技术概述 | 第10-14页 |
| 1．3．1 基于推理知识和信念的模态逻辑 | 第10-12页 |
| 1．3．2 基于状态搜索工具和定理证明技术 | 第12-13页 |
| 1．3．3 基于新的协议模型发展证明正确性理论 | 第13-14页 |
| 1．4 模型检测技术的研究与应用简述 | 第14-15页 |
| 1．5 本文的安排和研究成果 | 第15-17页 |
| 1．5．1 论文安排 | 第16页 |
| 1．5．2 主要研究成果 | 第16-17页 |
| 第二章 基于模型检测技术的运行模式分析法 | 第17-34页 |
| 2．1 引言 | 第17页 |
| 2．2 两方安全协议的运行模式分析法简介 | 第17-18页 |
| 2．3 基于可信第三方的安全协议的运行模式分析法研究 | 第18-24页 |
| 2．3．1 预备知识 | 第19-21页 |
| 2．3．2 基于可信第三方安全协议的运行模式分析 | 第21-24页 |
| 2．4 运行模式的数量上界及约束条件分析 | 第24-26页 |
| 2．4．1 协议的并行次数 | 第24页 |
| 2．4．2 运行模式的数量上界 | 第24-25页 |
| 2．4．3 运行模式的约束条件 | 第25-26页 |
| 2．5 运行模式组合集 | 第26-30页 |
| 2．6 多方安全协议的运行模式分析法研究 | 第30-32页 |
| 2．7 本章小结 | 第32-34页 |
| 第三章 两方协议运行模式分析法的应用 | 第34-41页 |
| 3．1 引言 | 第34页 |
| 3．2 SSL3．0基本握手协议的运行模式分析 | 第34-40页 |
| 3．2．1 SSL简介 | 第34-35页 |
| 3．2．2 建立SSL3．0基本握手协议模型 | 第35-36页 |
| 3．2．3 运行模式法分析SSL3．0基本握手协议 | 第36-39页 |
| 3．2．4 改进的SSL3．0基本握手协议模型 | 第39-40页 |
| 3．3 本章小结 | 第40-41页 |
| 第四章 基于可信第三方协议的运行模式分析法应用 | 第41-56页 |
| 4．1 只有一个可信第三方服务器协议分析实例 | 第41-48页 |
| 4．1．1 Davis Swick协议安全性分析 | 第41-43页 |
| 4．1．2 TMN协议的运行模式分析 | 第43-48页 |
| 4．2 多于一个可信第三方服务器协议分析实例 | 第48-55页 |
| 4．2．1 Kerberos协议介绍 | 第48-51页 |
| 4．2．2 Kerberos协议的形式化分析方法小结 | 第51-52页 |
| 4．2．3 Kerberos协议的运行模式分析 | 第52-55页 |
| 4．3 本章小结 | 第55-56页 |
| 第五章 关于安全协议设计原则的研究与应用 | 第56-66页 |
| 5．1 引言 | 第56页 |
| 5．2 安全协议设计原则 | 第56-61页 |
| 5．2．1 安全协议缺陷分类 | 第56-57页 |
| 5．2．2 安全协议的设计原则 | 第57-61页 |
| 5．2．3 小结 | 第61页 |
| 5．3 一个安全密钥建立协议的设计及分析 | 第61-65页 |
| 5．3．1 密钥建立协议的基本设计原则 | 第62页 |
| 5．3．2 一个安全密钥建立协议的设计 | 第62-64页 |
| 5．3．3 密钥建立协议的安全性分析 | 第64-65页 |
| 5．4 本章小结 | 第65-66页 |
| 第六章 模型检测法总结 | 第66-69页 |
| 6．1 模型检测法与其它经典形式化分析方法的比较 | 第66-68页 |
| 6．1．1 模型检测法与经典形式化分析方法的比较 | 第66-67页 |
| 6．1．2 运行模式分析法与其它方法的比较 | 第67-68页 |
| 6．2 模型检测法总体结论 | 第68-69页 |
| 结束语 | 第69-70页 |
| 致谢 | 第70-71页 |
| 参考文献 | 第71-75页 |
| 研究生阶段研究成果 | 第75页 |
