基于密钥体系的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
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 基于 密钥 体系 oauth2 改进 协议 形式化 分析 验证 程道雷
限制150内