| 摘要 | 第4-5页 |
| Abstract | 第5页 |
| 第一章 绪论 | 第8-13页 |
| 1.1 研究背景与意义 | 第8-10页 |
| 1.2 国内外研究现状 | 第10页 |
| 1.3 本文工作 | 第10-11页 |
| 1.4 研究目标与方法 | 第11页 |
| 1.5 本文组织结构 | 第11-13页 |
| 第二章 研究基础 | 第13-24页 |
| 2.1 OAuth2.0概述及授权码模型 | 第13-18页 |
| 2.1.1 OAuth2.0概述 | 第13-16页 |
| 2.1.2 OAuth2.0授权码模型架构及详细流程 | 第16-18页 |
| 2.2 安全协议形式化分析方法分类 | 第18-20页 |
| 2.2.1 基于模型检测的安全协议分析方法 | 第18-19页 |
| 2.2.2 基于逻辑分析的安全协议分析方法 | 第19-20页 |
| 2.2.3 基于证明的安全协议分析方法 | 第20页 |
| 2.3 AVISPA形式化模型架构理论研究 | 第20-24页 |
| 2.3.1 AVISPA介绍 | 第20-22页 |
| 2.3.2 HLPSL语言简介 | 第22-24页 |
| 第三章 基于模型检测的安全协议形式化分析方法研究 | 第24-27页 |
| 3.1 惰性无限状态方法 | 第24-25页 |
| 3.2 惰性攻击者优化方法 | 第25-27页 |
| 3.2.1 约束 | 第25页 |
| 3.2.2 约束规约 | 第25-27页 |
| 第四章 OAuth2.0授权码模型形式化分析与验证 | 第27-40页 |
| 4.1 OAuth2.0授权码模型 | 第27-28页 |
| 4.2 OAuth2.0授权码模型形式化需求 | 第28-29页 |
| 4.3 形式化建模的总体方案 | 第29页 |
| 4.4 用AVISPA工具验证OAuth2.0授权码模型的安全性 | 第29-40页 |
| 4.4.1 OAuth2.0授权码模型形式化描述 | 第29-35页 |
| 4.4.2 对OAuth2.0授权码模型性质分析 | 第35页 |
| 4.4.3 OAuth2.0授权码模型的攻击模拟 | 第35-39页 |
| 4.4.4 OAuth2.0授权码模型验证结果分析 | 第39-40页 |
| 第五章 安全授权码模型的建立 | 第40-50页 |
| 5.1 安全授权码模型 | 第40-42页 |
| 5.2 用AVISPA工具验证安全授权码模型的安全性 | 第42-50页 |
| 5.2.1 安全授权码模型形式化描述 | 第42-46页 |
| 5.2.2 安全授权码模型的攻击检测 | 第46-50页 |
| 第六章 总结与展望 | 第50-52页 |
| 6.1 总结 | 第50-51页 |
| 6.2 展望 | 第51-52页 |
| 参考文献 | 第52-54页 |
| 附录授权码形式化模型源代码 | 第54-58页 |
| 附录安全授权码形式化模型源代码 | 第58-63页 |
| 致谢 | 第63页 |
