基于密钥体系的OAuth 2.0改进协议形式化分析与验证

发布时间：2018-04-19 08:46

本文选题：网络安全 + OAuth　；参考：《华东交通大学》2016年硕士论文

【摘要】：在大数据时代的背景下,研究人员不断探索数据融合与共享的解决方案。与此同时,网络信息安全也迎来了前所未有的挑战,黑客们乐衷于寻找网络中的漏洞来发起恶意攻击,窃取机密信息。网络信息的传输主要依赖网络协议,如何设计出安全可靠的网络协议是保障网络信息安全的关键途径。形式化方法作为一种基于严格数学的技术手段,可用于验证协议的安全性质,找出潜在的漏洞,从而指导安全协议的设计与实现。为实现用户账号关联和资源共享,互联网工作任务组设计发布了OAuth 2.0协议。该协议实现用户在不向第三方应用透露用户名密码的情况,获取存储在资源服务器的受保护资源。但该协议由于自身的缺陷饱受攻击,给企业与用户带来巨大损失。主要原因在于OAuth 2.0过度依赖https通道传输数据而忽视了自身数据的加密,另外https的传输效率低下,在网络较差的环境下经常中断,从而招致黑客攻击。为解决上述问题,本文提出采用http通道传输OAuth 2.0协议数据,并运用公钥体系对OAuth 2.0协议进行加密改进。基于Delvo-Yao攻击者模型,采用Promela语言对改进协议建模,以线性时态逻辑刻画协议的安全性质。最后通过SPIN工具对模型进行检测。实验结果表明,单凭公钥加密,并不能保障OAuth 2.0协议的安全。在此基础之上,本文再提出采用私钥签名对协议关键信息进行签名的进一步改进方案。以同样的方式对新协议进行验证,并没有发现新协议中的漏洞。通过两次验证工作的对比,得到具有高安全性的新协议;对比建模时采用的由类型检查、静态分析、语法重定序构成的三种不同组合优化策略,获得新协议最优的安全验证模型。除此之外,本文还提出通过程序枚举法代替手工求解攻击者知识库,以降低攻击者模型构建复杂度,使本文提出的攻击者模型建模方法适用于拥有更多主体的协议的分析与验证。
[Abstract]:Against the background of big data's time, researchers have been exploring solutions for data fusion and sharing.At the same time, network information security is facing unprecedented challenges. Hackers are happy to search for loopholes in the network to launch malicious attacks and steal confidential information.The transmission of network information mainly depends on network protocol. How to design a safe and reliable network protocol is a key way to ensure the security of network information.As a technical method based on strict mathematics, formal method can be used to verify the security properties of the protocol, identify potential vulnerabilities, and guide the design and implementation of the security protocol.In order to realize user account association and resource sharing, the Internet Task Force designed and published OAuth 2.0 protocol.This protocol enables users to obtain protected resources stored in resource servers without revealing user names and passwords to third parties.However, the protocol has been attacked because of its own defects, which brings huge losses to enterprises and users.The main reason is that OAuth 2.0 excessively relies on the https channel to transmit data and neglects the encryption of its own data. In addition, the transmission efficiency of https is low, and it is often interrupted in the poor network environment, which leads to hacker attacks.In order to solve the above problems, this paper proposes to use http channel to transmit OAuth 2.0 protocol data, and use public key architecture to encrypt OAuth 2.0 protocol.Based on the Delvo-Yao attacker model, the improved protocol is modeled by Promela language, and the security property of the protocol is described by linear temporal logic.Finally, the model is detected by SPIN tool.Experimental results show that public key encryption alone can not guarantee the security of OAuth 2.0 protocol.On this basis, this paper proposes a further improvement scheme to use private key signature to sign the key information of the protocol.Verification of the new protocol in the same way does not reveal any vulnerabilities in the new protocol.Through the comparison of two verification work, a new protocol with high security is obtained, and three different combinatorial optimization strategies, which are composed of type checking, static analysis and syntax reordering, are adopted in the comparison modeling.The optimal security verification model of the new protocol is obtained.In addition, in order to reduce the complexity of constructing the attacker's model, this paper proposes to replace the manual solution of the attacker's knowledge base by program enumeration.The model modeling method proposed in this paper is suitable for the analysis and verification of protocols with more agents.
【学位授予单位】：华东交通大学
【学位级别】：硕士
【学位授予年份】：2016
【分类号】：TP393.08

【相似文献】