| 摘要 | 第5-6页 |
| ABSTRACT | 第6-7页 |
| 符号对照表 | 第11-12页 |
| 缩略语对照表 | 第12-15页 |
| 第一章 绪论 | 第15-21页 |
| 1.1 研究背景及意义 | 第15-16页 |
| 1.2 安全协议自适应模型检测框架简介 | 第16-17页 |
| 1.3 模型检测技术研究现状 | 第17-18页 |
| 1.4 论文主要工作与内容安排 | 第18-19页 |
| 1.5 本章小结 | 第19-21页 |
| 第二章 安全协议及其形式化分析方法 | 第21-29页 |
| 2.1 引言 | 第21页 |
| 2.2 安全协议 | 第21-23页 |
| 2.2.1 安全协议分类 | 第22页 |
| 2.2.2 安全协议的安全性质 | 第22-23页 |
| 2.3 形式化方法 | 第23-26页 |
| 2.3.1 形式逻辑方法 | 第23-24页 |
| 2.3.2 模型检测方法 | 第24页 |
| 2.3.3 定理证明方法 | 第24-26页 |
| 2.4 模型检测技术 | 第26-28页 |
| 2.4.1 模型检测基本思想 | 第26页 |
| 2.4.2 模型检测工具比较 | 第26-27页 |
| 2.4.3 自适应模型检测策略 | 第27-28页 |
| 2.5 本章小结 | 第28-29页 |
| 第三章 自动机学习算法 | 第29-45页 |
| 3.1 引言 | 第29页 |
| 3.2 预备知识 | 第29-31页 |
| 3.2.1 确定型有穷接收器 | 第29-30页 |
| 3.2.2 3 个值的确定型有穷自动机 | 第30-31页 |
| 3.3 L*学习算法 | 第31-33页 |
| 3.3.1 算法背景 | 第31-32页 |
| 3.3.2 算法描述 | 第32-33页 |
| 3.4 修正学习算法 | 第33-41页 |
| 3.4.1 向缺乏经验的教师学习 | 第33页 |
| 3.4.2 符号学习算法 | 第33-36页 |
| 3.4.3 修正学习算法La* | 第36-38页 |
| 3.4.4 正确性证明和复杂度分析 | 第38-39页 |
| 3.4.5 学习算法实例分析 | 第39-41页 |
| 3.5 相关工作 | 第41-42页 |
| 3.6 本章小结 | 第42-45页 |
| 第四章 安全协议自适应分析框架设计及其实现 | 第45-71页 |
| 4.1 引言 | 第45页 |
| 4.2 安全协议自适应模型检测方案 | 第45-53页 |
| 4.2.1 安全协议自适应模型检测流程 | 第46-48页 |
| 4.2.2 建模 | 第48-49页 |
| 4.2.3 模型检测 | 第49-51页 |
| 4.2.4 反例分析 | 第51-52页 |
| 4.2.5 模型修正 | 第52-53页 |
| 4.2.6 协议改进 | 第53页 |
| 4.3 仿真实现 | 第53-69页 |
| 4.3.1 基于AVISPA/SPAN工具的RSA协议模型检测 | 第53-58页 |
| 4.3.2 基于AVISPA/SPAN工具的DenningSaccoSharedKey协议模型检测 | 第58-61页 |
| 4.3.3 基于AVISPA/SPAN工具的Gong协议模型检测 | 第61-65页 |
| 4.3.4 基于Scyther工具的NS协议模型检测 | 第65-68页 |
| 4.3.5 基于Scyther工具的NSL协议模型检测 | 第68-69页 |
| 4.4 仿真实验结果分析 | 第69-70页 |
| 4.5 本章小结 | 第70-71页 |
| 第五章 总结与展望 | 第71-73页 |
| 5.1 总结 | 第71-72页 |
| 5.2 展望 | 第72-73页 |
| 参考文献 | 第73-77页 |
| 致谢 | 第77-79页 |
| 作者简介 | 第79-80页 |
