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

《基于密钥体系的oauth 2.0改进协议形式化分析与验证》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、分类号______________________________密级______________________________ＵＤＣ______________________________编号______________________________硕士学位论文基于密钥体系的OAuth2.0改进协议形式化分析与验证学位申请人：程道雷学科专业：计算机软件与理论指导教师：肖美华教授答辩日期：独创性声明本人郑重声明：所呈交的学位论文是我个人在导师指导下进行的研究工作及取得的研究成果。尽我所知，除了文中特别

2、加以标注和致谢的地方外，论文中不包含其他人已经发表和撰写的研究成果，也不包含为获得华东交通大学或其他教育机构的学位或证书所使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中作了明确的说明并表示了谢意。本人签名_______________日期____________关于论文使用授权的说明本人完全了解华东交通大学有关保留、使用学位论文的规定，即：学校有权保留送交论文的复印件，允许论文被查阅和借阅。学校可以公布论文的全部或部分内容，可以采用影印、缩印或其他复制手段保存论文。保密的论文在解密后遵守此

3、规定，本论文无保密内容。本人签名____________导师签名__________日期___________基于密钥体系的OAuth2.0改进协议形式化分析与验证摘要在大数据时代的背景下，研究人员不断探索数据融合与共享的解决方案。与此同时，网络信息安全也迎来了前所未有的挑战，黑客们乐衷于寻找网络中的漏洞来发起恶意攻击，窃取机密信息。网络信息的传输主要依赖网络协议，如何设计出安全可靠的网络协议是保障网络信息安全的关键途径。形式化方法作为一种基于严格数学的技术手段，可用于验证协议的安全性质，找出潜在的漏洞，从而

4、指导安全协议的设计与实现。为实现用户账号关联和资源共享，互联网工作任务组设计发布了OAuth2.0协议。该协议实现用户在不向第三方应用透露用户名密码的情况，获取存储在资源服务器的受保护资源。但该协议由于自身的缺陷饱受攻击，给企业与用户带来巨大损失。主要原因在于OAuth2.0过度依赖https通道传输数据而忽视了自身数据的加密，另外https的传输效率低下,在网络较差的环境下经常中断，从而招致黑客攻击。为解决上述问题，本文提出采用http通道传输OAuth2.0协议数据，并运用公钥体系对OAuth2.0协议进

5、行加密改进。基于Delvo-Yao攻击者模型，采用Promela语言对改进协议建模，以线性时态逻辑刻画协议的安全性质。最后通过SPIN工具对模型进行检测。实验结果表明，单凭公钥加密，并不能保障OAuth2.0协议的安全。在此基础之上，本文再提出采用私钥签名对协议关键信息进行签名的进一步改进方案。以同样的方式对新协议进行验证，并没有发现新协议中的漏洞。通过两次验证工作的对比，得到具有高安全性的新协议；对比建模时采用的由类型检查、静态分析、语法重定序构成的三种不同组合优化策略，获得新协议最优的安全验证模型。除此之

6、外，本文还提出通过程序枚举法代替手工求解攻击者知识库，以降低攻击者模型构建复杂度，使本文提出的攻击者模型建模方法适用于拥有更多主体的协议的分析与验证。关键词：网络安全，OAuth2.0协议，形式化方法，模型检测，公钥体系，私钥签名IFORMALANALYSISANDVERIFICATIONOFOAUTH2.0PROTOCOLIMPROVEDBYKEYCRYPTOSYSTEMSABSTRACTUnderthebackgroundofthebigdataera,researchersareexploringthe

7、solutionsofdatafusionandsharing.Atthesametime,thenetworkinformationsecurityalsousheredintheunprecedentedchallenges,hackersliketofindloopholestolaunchmaliciousattacksandstealconfidentialinformationinthenetwork.Thenetworkinformationtransmissionmainlydependson

8、thenetworkprotocol,howtodesignasafeandreliablenetworkprotocolisthekeytoensurethenetworkinformationsecurity.Formalmethodsisatechnologybasedonstrictmathematicalwhichcanbeusedtoverifytheprotocolsecuritypr