文摘
英文文摘
第一章 绪论
1.1 研究背景及意义
1.2 国内外研究现状
1.3 本文的主要工作
1.4 本文的组织结构
第二章 模型检测理论
2.1 模型检测技术
2.1.1 模型检测原理
2.1.2 模型检测的特点
2.2 时态逻辑
2.2.1 线性时态逻辑
2.2.2 计算树逻辑
2.2.3 LTL和CTL公式描述能力的比较
2.3 模型检测算法
2.3.1 LTL模型检测算法
2.3.2 CTL模型检测算法
2.4 安全协议的模型检测的现状及问题
2.5 小结
第三章 谓词抽象和小系统模型理论
3.1 抽象解释理论
3.2 谓词抽象
3.3 小系统模型理论
3.3.1 安全协议的假设
3.3.2 小系统模型
3.4 小系统模型实例
3.5 组合抽象方法
3.6 小结
第四章 SSL3.0握手协议的模型检测
4.1 模型检测工具简介
4.1.1 新型符号模型检测工具NuSMV
4.1.2 其他模型检测工具简介
4.2 SSL协议的概述
4.3 SSL3.0握手协议的分析
4.3.1 SSL3.0握手协议的小系统模型
4.3.2 SSL3.0握手协议的性质描述
4.3.3 SSL握手协议模型检测结果分析
4.4 小结
第五章 总结与展望
5.1 工作总结
5.2 展望
参考文献
致谢
攻读硕士期间发表的论文
附录 :SSL3.0握手协议模型检测的NuSMV源代码