| 摘要 | 第3-5页 |
| ABSTRACT | 第5-6页 |
| 第一章 绪论 | 第9-14页 |
| 1.1 引言 | 第9-10页 |
| 1.2 安全协议形式化分析研究历史与现状 | 第10-12页 |
| 1.3 论文的工作 | 第12-13页 |
| 1.4 论文的组织结构 | 第13-14页 |
| 第二章 BAN逻辑及其在安全协议形式化分析中的应用 | 第14-24页 |
| 2.1 BAN逻辑介绍 | 第14页 |
| 2.2 BAN逻辑的基本框架 | 第14-18页 |
| 2.2.1 BAN逻辑中的基本术语 | 第14-15页 |
| 2.2.2 BAN的六条基本推理规则 | 第15-17页 |
| 2.2.3 BAN逻辑推理过程中所基于的假设 | 第17-18页 |
| 2.3 BAN逻辑形式化分析的步骤及其流程图 | 第18-19页 |
| 2.4 基于BAN逻辑的YAHALOM协议的形式化分析 | 第19-24页 |
| 2.4.1 YAHALOM协议描述及协议各主体发送消息转换图 | 第19-20页 |
| 2.4.2 YAHALOM协议消息发送的自然语言描述 | 第20页 |
| 2.4.3 基于BAN逻辑理想化YAHALOM协议 | 第20-21页 |
| 2.4.4 基于BAN的YAHALOM协议初始化状态及假设 | 第21页 |
| 2.4.5 基于BAN逻辑规则设定的协议目标 | 第21-22页 |
| 2.4.6 基于BAN逻辑规则的推理证明过程 | 第22-24页 |
| 第三章 基于符号化模型检测的安全协议的形式化分析 | 第24-51页 |
| 3.1 模型检测的诞生 | 第24-25页 |
| 3.2 符号化模型检测(SMV—Symbolic Model Verifier)概述 | 第25-26页 |
| 3.3 SMV语言概述 | 第26-29页 |
| 3.3.1 数据类型和类型声明 | 第26-28页 |
| 3.3.2 ASSIGN声明和SPEC说明 | 第28页 |
| 3.3.3 公平性约束声明—FARINESS | 第28页 |
| 3.3.4 SMV语言程序的整体框架—模块 | 第28-29页 |
| 3.4 计算树逻辑(Computing tree logic)相关知识介绍 | 第29-30页 |
| 3.5 YAHALOM协议的小系统模型分析 | 第30-31页 |
| 3.6 SMV的一个short.smv实例 | 第31-33页 |
| 3.7 基于符号化模型检测SMV的YAHALOM协议形式化分析 | 第33-51页 |
| 3.7.1 协议的消息描述 | 第33-35页 |
| 3.7.2 YAHALOM协议中各诚实主体的有限状态系统模型表示 | 第35-38页 |
| 3.7.2.1 初始者AA的有限状态系统模型 | 第36页 |
| 3.7.2.2 响应者BB的有限状态系统模型 | 第36-37页 |
| 3.7.2.3 服务器SS的有限状态系统模型 | 第37-38页 |
| 3.7.3 非法主体Ⅱ有限状态系统模型 | 第38-39页 |
| 3.7.4 协议运行中诚实主体的状态转化的自然语言描述 | 第39-40页 |
| 3.7.5 基于CTL的协议安全属性描述 | 第40-41页 |
| 3.7.6 协议编程详细过程说明 | 第41-51页 |
| 3.7.6.1 认证性编程框架以及运行结果说明 | 第41-46页 |
| 3.7.6.2 保密性验证模块编程框架及其运行结果说明 | 第46-48页 |
| 3.7.6.3 安全性验证编程框架以及运行结果说明 | 第48-49页 |
| 3.7.6.4 完整性编程框架以及运行结果说明 | 第49-51页 |
| 第四章 两种验证方法对比 | 第51-53页 |
| 第五章 总结和展望 | 第53-55页 |
| 5.1 论文总结 | 第53-54页 |
| 5.2 研究展望 | 第54-55页 |
| 参考文献 | 第55-60页 |
| 附录：主要SMV代码 | 第60-67页 |
| 攻读硕士学位期间主要的研究成果 | 第67-68页 |
| 致谢 | 第68-70页 |
