| 摘要 | 第1-4页 |
| Abstract | 第4-7页 |
| 第一章 引言 | 第7-11页 |
| ·背景介绍 | 第7-9页 |
| ·课题来源 | 第9页 |
| ·选题意义 | 第9页 |
| ·本人所做的工作 | 第9-10页 |
| ·本文结构 | 第10-11页 |
| 第二章 安全协议 | 第11-19页 |
| ·安全协议的概念 | 第11页 |
| ·安全协议的类型 | 第11-12页 |
| ·安全协议的缺陷 | 第12-13页 |
| ·安全协议的设计准则 | 第13-19页 |
| 第三章 安全协议的形式化分析方法 | 第19-38页 |
| ·安全协议形式化分析概述 | 第19-21页 |
| ·应用形式化方法分析安全协议的历史和现状 | 第19-21页 |
| ·基于知识与信念推理的模态逻辑方法 | 第21-26页 |
| ·BAN逻辑 | 第22-23页 |
| ·GNY逻辑 | 第23页 |
| ·AT逻辑 | 第23-24页 |
| ·SVO逻辑 | 第24页 |
| ·Kailar逻辑 | 第24-25页 |
| ·CS逻辑 | 第25页 |
| ·KG逻辑 | 第25-26页 |
| ·基于状态穷举的搜索工具 | 第26-31页 |
| ·Murφ方法 | 第26-27页 |
| ·进程演算与安全性质 | 第27-28页 |
| ·模型检测 | 第28-31页 |
| ·一种重要的模型: Dolev-Yao的攻击者模型 | 第31页 |
| ·基于协议模型的证明结构性理论 | 第31-35页 |
| ·串空间模型方法 | 第32-33页 |
| ·Paulson归纳法 | 第33-34页 |
| ·Schneider秩函数 | 第34-35页 |
| ·几种形式化验证工具比较 | 第35-38页 |
| ·几种形式化验证工具原理比较 | 第35页 |
| ·几种常见的形式化验证工具 | 第35-38页 |
| 第四章 安全协议形式化分析方法的融合性研究 | 第38-47页 |
| ·单一形式化研究方法的不足 | 第38-40页 |
| ·模态逻辑技术的不足 | 第38-39页 |
| ·状态穷举技术的不足 | 第39-40页 |
| ·定理证明结构性方法的不足 | 第40页 |
| ·融合性的安全协议研究方法概述 | 第40-42页 |
| ·BAN逻辑验证工具和模型检测工具相结合 | 第41页 |
| ·模型检测与串空间模型相结合 | 第41-42页 |
| ·实例:一种基于CAPSL的融合性安全协议研究方法 | 第42-47页 |
| ·CAPSL规范语言 | 第42-43页 |
| ·通过CAPSL语言构建安全协议分析工具连接 | 第43-47页 |
| 第五章 总结和展望 | 第47-49页 |
| ·论文总结 | 第47-48页 |
| ·展望 | 第48-49页 |
| 致谢 | 第49-50页 |
| 参考文献 | 第50-51页 |