| 摘要 | 第4-5页 |
| Abstract | 第5-6页 |
| 第一章 绪论 | 第12-18页 |
| 1.1 研究背景及意义 | 第12-13页 |
| 1.2 研究现状与分析 | 第13-16页 |
| 1.2.1 安全协议形式化分析方法研究历史与现状 | 第13-14页 |
| 1.2.2 安全协议形式化分析方法应用现状 | 第14-16页 |
| 1.3 论文的主要工作 | 第16-17页 |
| 1.4 论文的结构安排 | 第17-18页 |
| 第二章 相关技术分析 | 第18-30页 |
| 2.1 攻击者模型 | 第18-19页 |
| 2.2 安全协议 | 第19-23页 |
| 2.2.1 基本概念 | 第19页 |
| 2.2.2 安全属性 | 第19-20页 |
| 2.2.3 安全协议分类 | 第20页 |
| 2.2.4 典型攻击方法 | 第20-23页 |
| 2.3 项重写系统 | 第23-24页 |
| 2.4 智能规划问题 | 第24-26页 |
| 2.5 布尔可满足性问题 | 第26-29页 |
| 2.5.1 基本概念 | 第26-27页 |
| 2.5.2 完备求解算法 | 第27-29页 |
| 2.5.3 局部搜索算法 | 第29页 |
| 2.6 本章小结 | 第29-30页 |
| 第三章 基于SAT的安全协议惰性形式化分析方法 | 第30-54页 |
| 3.1 安全协议惰性模型检测方法SAT-LMC | 第30-32页 |
| 3.2 基于变量保持的惰性初始状态描述 | 第32-35页 |
| 3.2.1 基本初始状态 | 第32-33页 |
| 3.2.2 惰性的初始状态 | 第33-34页 |
| 3.2.3 初始状态的深度优化 | 第34-35页 |
| 3.3 支持多种攻击类型检测的惰性协议重写规则描述 | 第35-41页 |
| 3.3.1 基于变量保持的协议重写规则 | 第35-37页 |
| 3.3.2 类型缺陷攻击支持 | 第37-39页 |
| 3.3.3 并行会话攻击支持 | 第39-40页 |
| 3.3.4 惰性的攻击者与协议重写规则 | 第40-41页 |
| 3.4 安全协议形式化分析安全属性描述 | 第41-42页 |
| 3.4.1 保密性安全属性的描述 | 第41-42页 |
| 3.4.2 认证性安全属性的描述 | 第42页 |
| 3.5 布尔命题公式的构造 | 第42-47页 |
| 3.5.1 协议转换系统 | 第43页 |
| 3.5.2 协议不安全问题 | 第43-44页 |
| 3.5.3 基于智能规划的协议不安全问题SAT编码技术 | 第44-47页 |
| 3.6 基于中间解加速的启发式复合SAT求解算法 | 第47-53页 |
| 3.6.1 复合求解算法概述 | 第47-49页 |
| 3.6.2 基于文字概率与子句权值的局部搜索模块 | 第49-50页 |
| 3.6.3 基于文字权值的冲突消除模块 | 第50-51页 |
| 3.6.4 以中间解为输入的完备搜索模块 | 第51-53页 |
| 3.7 本章小结 | 第53-54页 |
| 第四章 形式化分析系统的设计、实现及测试分析 | 第54-68页 |
| 4.1 设计目标 | 第54页 |
| 4.2 系统框架设计 | 第54-55页 |
| 4.3 系统核心模块实现 | 第55-60页 |
| 4.3.1 形式化描述模块 | 第55-58页 |
| 4.3.2 数据解析模块 | 第58-59页 |
| 4.3.3 协议分析模块 | 第59-60页 |
| 4.4 系统测试与分析 | 第60-66页 |
| 4.4.1 SAT求解器测试 | 第60-63页 |
| 4.4.2 系统功能测试与分析 | 第63-64页 |
| 4.4.3 系统性能测试与比较 | 第64-66页 |
| 4.5 本章小结 | 第66-68页 |
| 第五章 开放授权协议OAuth2.0 的安全性形式化分析 | 第68-88页 |
| 5.1 开放授权协议OAuth2.0 | 第68-73页 |
| 5.1.1 协议介绍 | 第68-70页 |
| 5.1.2 协议主体 | 第70-71页 |
| 5.1.3 用户授权方式分类 | 第71-72页 |
| 5.1.4 授权码授权模式的流程规范 | 第72-73页 |
| 5.2 基于SAT-LMC方法的OAuth2.0 的安全性形式化分析 | 第73-82页 |
| 5.2.1 OAuth2.0 协议的形式化描述 | 第73-78页 |
| 5.2.2 OAuth2.0 的形式化分析结果 | 第78-82页 |
| 5.3 形式化分析结果的有效性验证 | 第82-85页 |
| 5.4 形式化分析结果的统计与分析 | 第85-86页 |
| 5.5 本章小结 | 第86-88页 |
| 结束语 | 第88-90页 |
| 一、论文工作总结 | 第88页 |
| 二、难点与创新点 | 第88-89页 |
| 三、下一步工作展望 | 第89-90页 |
| 附录 OAuth2.0的HLPSL描述（情景1） | 第90-93页 |
| 致谢 | 第93-94页 |
| 参考文献 | 第94-98页 |
| 作者简介 | 第98页 |
