| 提要 | 第1-6页 |
| 第一章 引言 | 第6-9页 |
| ·课题背景 | 第6-7页 |
| ·本文的研究内容及组织结构 | 第7-9页 |
| 第二章 相关理论 | 第9-13页 |
| ·模型检测介绍 | 第9-12页 |
| ·模型检测的主要技术 | 第9-10页 |
| ·模型检测方法 | 第10-12页 |
| ·安全协议介绍 | 第12-13页 |
| 第三章 基于SAT 的安全协议模型检测器SATMC | 第13-19页 |
| ·介绍 | 第13-14页 |
| ·SATMC 的核心思想 | 第14-18页 |
| ·协议安全问题转化为规划问题 | 第14-15页 |
| ·规划问题转化为SAT 方法求解 | 第15-18页 |
| ·SATMC 的可判定性和终止性 | 第18-19页 |
| 第四章 一种新的基于SAT 的模型检测器JLU-PV | 第19-24页 |
| ·介绍 | 第19页 |
| ·算法描述和核心思想 | 第19-23页 |
| ·总结 | 第23-24页 |
| 第五章 基于归结方法的模型检测器Proverif | 第24-29页 |
| ·协议的描述 | 第24-25页 |
| ·归结方法的执行过程 | 第25-27页 |
| ·Proverif 的优势、缺陷及终止性 | 第27-29页 |
| 第六章 一个新的基于归结方法的模型检测器 | 第29-51页 |
| ·算法相关理论介绍 | 第29-35页 |
| ·IF 语言介绍 | 第29-30页 |
| ·规则库的建立 | 第30-31页 |
| ·算法的核心思想 | 第31-32页 |
| ·以协议test-attack 为例演示算法执行过程 | 第32-35页 |
| ·算法描述 | 第35-38页 |
| ·算法终止性的改进 | 第38页 |
| ·算法的实现 | 第38-46页 |
| ·例子检验 | 第46-51页 |
| ·协议test-safe 和协议test-attack 的实验结果 | 第46-48页 |
| ·以协议test-attack 为例对终止性进行比较 | 第48-51页 |
| 第七章 结论 | 第51-52页 |
| 参考文献 | 第52-56页 |
| 摘要 | 第56-59页 |
| Abstract | 第59-63页 |
| 致谢 | 第63页 |
