基于密钥体系的oauth 2.0改进协议形式化分析与验证-程道雷.docx

《基于密钥体系的oauth 2.0改进协议形式化分析与验证-程道雷.docx》由会员分享，可在线阅读，更多相关《基于密钥体系的oauth 2.0改进协议形式化分析与验证-程道雷.docx（61页珍藏版）》请在得力文库 - 分享文档赚钱的网站上搜索。

1、分类号 _ 密级 _ U D C _ 编号 _ 淨 東 夂 ii A 普 硕士学位论文 基于密钥体系的 OAuth 2.0 改进协议形式化 分析与验证 学位申请人：程道雷 学科专业：计算机软件与理论 指导教师：肖美华教授 答辩日期 : 华东交通大学2016届硕士学位论文基于密钥体系的OAuth2.0改进协议形式化分析与验证软件学院程道雷 独创性声明 本人郑重声明：所呈交的学位论文是我个人在导师指导下进行的研究 工作及取得的研究成果。尽我所知，除了文中特别加以标注和致谢的地方 外，论文中不包含其他人已经发表和撰写的研究成果，也不包含为获得华 东交通大学或 其他教育机构的学位或证书所使用过的材料。

2、与我一同工作 的同志对本研究所做的任何贡献均已在论文中作了明确的说明并表示了谢 意、。 本人签名 _ 日期 . 关于论文使用授权的说明 本人完全了解华东交通大学有关保留、使用学位论文的规定，即：学 校有权保留送交论文的复印件，允许论文被查阅和借阅。学校可以公布论 文的全部或部分内容，可以采用影印、缩印或其他复制手段保存论文。 保密的论文在解密后遵守此规定，本论文无保密内容。 本人签名 _ 导师签名 _ 日期 . 摘要 基于密钥体系的 OAuth 2.0 改进协议形式化分析与验证 摘要 在大数据时代的背景下，研究人员不断探索数据融合与共享的解决方案。与此同 时，网络信息安全也迎来了前所未有的挑战

3、，黑客们乐衷于寻找网络中的漏洞来发起 恶意攻击，窃取机密信息。网络信息的传输主要依赖网络协议，如何设计出安全可靠 的网络协议是保障网络信息安全的关键途径。形式化方法作为一种基于严格数学的技 术手段，可用于验证协议的安全性质，找出潜在的漏洞，从而指导安全协议的设计与 实现。 为实现用户账号关联和资源共享，互联网工作任务组设计发布了 OAuth 2.0 协 议。该协议实现用户在不向第三方应用透露用户名密码的情况，获取存储在资源服务 器的受保护资源。但该协议由于自身的缺陷饱受攻击，给企业与用户带来巨大损失。 主要原因在于 OAuth 2.0 过度依赖 https 通道传输数据而忽视了自身数据的加密，

4、另 外 https 的传输效率低下，在网络较差的环境下经常中断，从而招致黑客攻击。 为解决上述问题，本文提出采用 http通道传输 OAuth 2.0协议数据，并运用公钥 体系对 OAuth 2.0 协议进行加密改进。基于 Delvo-Yao 攻击者模型，采用 Promela 语 言对改进协议建模，以线性时态逻辑刻画协议的安全性质。最后通过 SPIN 工具对模型 进行检测。实验结果表明，单凭公钥加密，并不能保障 OAuth 2.0 协议的安全。在此 基础之上，本文再提出采用私钥签名对协议关键信息进行签名的进一步改进方案。以 同样的方式对新协议进行验证，并没有发现新协议中的漏洞。通过两次验证工作

5、的对 比，得到具有高安全性的新协议；对比建模时采用的由类型检查、静态分析、语法重 定序构成的三种不同组合优化策略，获得新协议最优的安全验证模型。除此之外，本 文还提出通过程序枚举法代替手工求解攻击者知识 库，以降低攻击者模型构建复杂 度，使本文提出的攻击者模型建模方法适用于拥有更多主体的协议的分析与验证。 关键词 ：网络安全 ， OAuth 2.0 协议，形式化方法，模型检测，公钥体系，私钥签名 FORMAL ANALYSIS AND VERIFICATION OF OAUTH 2.0 PROTOCOL IMPROVED BY KEY CRYPTOSYSTEMS ABSTRACT Under

6、the background of the big data era, researchers are exploring the solutions of data fusion and sharing. At the same time, the network information security also ushered in the unprecedented challenges, hackers like to find loopholes to launch malicious attacks and steal confidential information in th

7、e network. The network information transmission mainly depends on the network protocol, how to design a safe and reliable network protocol is the key to ensure the network information security. Formal methods is a technology based on strict mathematical which can be used to verify the protocol secur

8、ity properties and identify potential vulnerabilities, then to guide the design and implementation of security protocols. With realizing account relevance and resources sharing, the Internet Engineering Task Force designed and released OAuth 2.0 protocol. Users neednt disclose name and password to t

9、he third party applications to get protected resources stored in resources server from now on. The defects make OAuth 2.0 being attacked, which also brings huge losses to enterprises and users. The reasons are OAuth 2.0 over-reliance on HTTPS to transmit data and ignore per-message encryption, and t

10、hat the transmission efficiency of HTTPS is too low to work well under the poor network, so that the protocol triggers hacker attacks frequently. To solve the above problems, the improved OAuth 2.0 protocol, which transmit data by the HTTP channel and encrypt messages by public key system is present

11、ed. Furthermore, Promela language is utilized to model the improved protocol based on Delvo-Yao attacker model and Linear Temporal Logic is adopted to describe security properties of the protocol. Finally SPIN is utilized to check the model. The experimental results show that it cant guarantee the s

12、ecurity of OAuth 2.0 by depending solely public key encryption. On this basis, the further improvement strategy is proposed by utilizing private key signature to signature on key information of the protocol. Verifying the improved protocol by the same way, no holes have been found. Comparing two ver

13、ification work, a new higher security protocol is acquired, compared with different protocol modeling by three combination optimization strategies such as type checking, static analysis and syntactic reordering, an optimal security verification model of the improved protocol is obtained. Furthermore

14、, program enumeration is presented to instead of manual to obtain the attackers repository. The method above can reduce the complexity of modeling attacker effectively, so that the modeling method of attacker can be applied to analyze and validate multi-principal protocols. Key Words: network securi

15、ty, OAuth 2.0 protocol, Formal methods, model checking, public key system, private key signature 目录 目录 主要符号说明 . I 第 1 章绪论 . 1 1.1 研究背景及意义 . 1 1.2 研究现状 . 3 1.3 研究内容 . 3 1.4 本文结构 . 4 第二章 OAuth 2.0 协议 . 5 2.1 OAuth 2.0 协议流程 . 5 2.2 客户端的授权模式 . 6 2.2.1 授权码模式 . 6 2.2.2 隐式许可模式 . 7 2.2.3 用户密码证书模式 . 8 2.2.4

16、客户端私有证书模式 . 8 2.3 OAuth 2.0 安全问题 . 8 第三章形式化方法与模型检测技术理论基础 . 10 3.1 形式化方法概述 . 10 3.1.1 基于模态逻辑的协议分析方法 . 10 3.1.2 基于模型检测的协议分析方法 . 11 3.1.3 基于定理证明的协议分析方法 . 11 3.2 模型检测工具 SPIN . 12 3.2.1 SPIN 工作原理 . 13 3.2.2 模型描述语言 Promela . 13 3.2.3 线性时态逻辑 LTL . 15 第四章基于公钥体系的 OAuth 2.0 改进协议模型检测 . 16 4.1 基于公钥体系的 OAuth 2.0

17、 改进协议形式化表示 . 16 4.2 运用 LTL 公式刻画 OAuth 2.0 协议安全性质 . 17 4.3 诚实主体建模 . 18 4.3.1 消息通道构建 . 18 4.3.2 诚实主体行为描述 . 19 4.4 攻击者建模 . 22 4.4.1 攻击者知识库构建 . 22 4.4.2 攻击者行为描述 . 24 4.5 初始进程构建 . 26 4.6 模型检测结果与分析 . 27 第五章基于私钥签名的 OAuth 2.0 改进协议模型检测 . 30 5.1 运用私钥签名对 OAuth 2.0 协议进一步 改进 . 30 5.2 改进协议建模 . 31 5.2.1 消息通道改进 . 3

18、1 5.2.2 诚实主体行为改进 . 31 5.2.3 运用程序枚举法求解攻击者知识库 . 32 5.3 改进协议的模型检测结果与分析 . 35 5.4 模型优化与分析 . 36 第六章总结与廳 . 38 6.1 工作总结 . 38 6.2 未来工作廳 . 38 参考文献 . 40 附录 A 基于私钥签名的 OAuth 2.0 改进协议模型 Promela 代码 . 43 附录 B 攻击者可以学会的知识 C+求解代码 . 48 附录 C 攻击者需要学会的知识 C+求解代码 . 49 附录 D 攻击者需要表示的知识 C+求解代码 . 51 个人简历在读期间的科研成果 . 52 致谢 . 53 主

19、要符号说明 C RO AS RS H Ar A_g P_r PKro PKc PKas PKrs PKh PRro PRc PRas PRrs 主要符号说明 C/e 故缩写，指客户端； Resource Owwer 缩写，资源拥有者，即用户； A 如 hor/za“+o Server 缩写，指授权服务器； Resource Server 缩写，指资源服务器； Hacker 的缩写，指攻击者； Au,hor+za“+o Regues,的简写，指授权请求； Access GTa 故的简写，指授权许可； C/+e 故 Cree a/s 的简写，指客户端私有证书； Access Tofew 的简写，指

20、访问令牌； ProtecteResource 的简写，指存储在资源服务器上的受保护的资源 ; RO 的公钥； C 的公钥； AS 的公钥； RS 的公钥； H 的公钥； RO 的私钥； C 的私钥； AS 的私钥； RS 的私钥。 第 一 章 绪 论 1.1 研究背景及意义 随着互联网和移动互联网技术的飞速发展，我们己经渐渐进入了 DT ( Data Technology， 数据科技）时代。在这样的大背景下，我国在网络安全方面所面临挑战日 益巨大，保障信息安全己经成为保证国防安全、国家政体安全的重要任务。 2013 年， 英国简氏战略报告对各国信息防护能力进行评估，我国是信息安全问题最为严峻

21、的国家之一，所有接入互联网的网络管理中心中，超过 95%都遭受到国内外黑客侵 袭，并且大部分黑客的攻击行为都针对 银行、证券等金融机构。美国 “ 斯诺登事件 ” 爆发，更让全世界深刻认识到网络安全问题的严峻性。 为保障网络信息安全，我国政府采取了一系列重大措施以加速网络安全和信息化 发展，并且特设中央网络安全和信息化领导小组，由习主席担任组长，标志着我国的 信息安全问题己经成为国家重要发展战略。因此，网络安全的研究具有非常重大的意 义和价值。 在网络数据传输过程中，计算机之间需按一定规则进行通信，这些规则构成了网 络协议。网络协议规范了数据的传输方式，它的安全性和效率决定着网络通信是否安 全可

22、靠，但是网络协议的缺陷往往会招致 攻击者攻击。 有如下场景：某用户需要使用两种网络服务，既可以通过服务 A 打印照片（如网 易印像派），也可以将照片保存到服务 B (如 QQ 空间），如下图所示： 图 1-1 第三方平台下资源共享问题实例 Fig.1-1 Instances of Resource Sharing Problem under The Third Party Platform 因为 A、 B 这两种服务由不同的公司提供，因此，为获取这两种服务，该用户必 须分别在这两家公司的网站注册个人账户。如果该用户想要通过服务 A 打印存放在服 务B 上的照片时，一般情况下有两种不同的方法：第

23、一种方法，从服务 B 直接下载照 片后发送至服务 A 打印，该方法虽安全，却繁琐低效；第二种方法，用户将服务 B 的 账号密码直接提供给服务 A， 由服务 A 自己从服务 B 下载照片完成打印，但在这种情 况下，服务 A 也许会非法获取用户的其它隐私信息。 为解决这类难题， Google、 Yahoo 和 Facebook 等各大服务提供商开始研发对外授 权接口，第三方应用获取用户授权后，即可通过调用这些接口访问用户存储在服务器 上的资源。在这种模式下，用户需在登录服务器后，对第三方应用进行授权，而不用 向第三方应用提供账号密码。在服务器中，用户既可设置第三方应用访问资源的范 围、时间等，也可

24、选择性地取消对某些第三方应用的授权。第三方应用的研发人员必 须集成各服务提供商的授权接口，而各个服务提供商的对外授权接口的标准不一 ，导 致该项工作变得非常困难。服务提供商提供统一标准的授权接口成了迫在眉睫的问 题。 2006 年 11 月， Blaine Cook 研发 Twitter 的 OpenlD 之际， Ma.gnolia (现更名为 Gnolia， 是一个社会书签网站 ） 需要一个解决方案，允许使用 OpenID 的成员授权 Dashboard 访问他们提供的服务。 Blaine Cook、 Chris Messina、 Larry Half (Ma.gnolia 的员工 ） 与

25、David Recordon 在一起商讨如何在 Twitter 和 Ma.gnolia API 上使用 OpenID 进行委托授权。讨论结果为，还没有开放标准用于实现 API 访问的委托。因此，在 2007年 4 月，他们成立了 OAuth 讨论组，研究出第一份 OAuth 协议的提议草案。 2007 年 7月，团队起草了最初的规范，并且在 Eran Hammer 加入团队后，创建了更加正式 的草案。 2007 年 10 月，发布 OAuth Core 1.01。 2008 年 11 月，在明尼阿波利斯 （ Minneapolis)举行的 IETF (Internet Engineering

26、Task Force， 互联网工作任务组）第 73 次会议上，讨论将 OAuth 2.0 协议交给 IETF 做 进一步规范工作。 2010 年 4 月， OAuth 1.0 作为 RFC 5849 (Request for Comments 5849)发布。 2009 年 4 月 23 日， IETF 声明 OAuth1.0 协议存在一个固定会话攻击漏 洞，并因此发布了 OAuth Core 1.0a。 2012 年 10 月， IETF 在 RFC 6749 中发布 OAuth 2.0 框架 2。 OAuth 2.0 并不兼容 OAuth 1.0。 OAuth 2.0 作为一个崭新的开放授

27、权协议，主要解决了用户账号关联和资源共享等 问题。目前， OAuth 2.0 并没有完全取缔 OAuth 1.0a。 比如 Weibo3、 Microsoft4、 Google5、Facebook6、 豆瓣 7等服务提供商在使用 OAuth 2.0，而百度 8、 Twitter9等 服务提供商仍在使用 OAuth 1.0a， 究其原因在于 OAuth 2.0 的安全问题一直饱受诟病。 近年来，由 0Auth 2.0 导致的安全事故，使 Facebook、 Google、 腾讯 QQ、 Weibo、 支 付宝、Amazon 等大量知名网站用户信息遭窃。因此，对 OAuth 2.0 协议的安全性进行 研究具有非常重要的价值与意义。