在大数据时代的背景下,研究人员不断探索数据融合与共享的解决方案。与此同时,网络信息安全也迎来了前所未有的挑战,黑客们乐衷于寻找网络中的漏洞来发起恶意攻击,窃取机密信息。网络信息的传输主要依赖网络协议,如何设计出安全可靠的网络协议是保障网络信息安全的关键途径。形式化方法作为一种基于严格数学的技术手段,可用于验证协议的安全性质,找出潜在的漏洞,从而指导安全协议的设计与实现。为实现用户账号关联和资源共享,互联网工作任务组设计发布了OAuth 2.0协议。该协议实现用户在不向第三方应用透露用户名密码的情况,获取存储在资源服务器的受保护资源。但该协议由于自身的缺陷饱受攻击,给企业与用户带来巨大损失。主要原因在于OAuth 2.0过度依赖https通道传输数据而忽视了自身数据的加密,另外https的传输效率低下,在网络较差的环境下经常中断,从而招致黑客攻击。为解决上述问题,本文提出采用http通道传输OAuth 2.0协议数据,并运用公钥体系对OAuth 2.0协议进行加密改进。基于Delvo-Yao攻击者模型,采用Promela语言对改进协议建模,以线性时态逻辑刻画协议的安全性质。最后通过SPIN工具对模型进行检测。实验结果表明,单凭公钥加密,并不能保障OAuth 2.0协议的安全。在此基础之上,本文再提出采用私钥签名对协议关键信息进行签名的进一步改进方案。以同样的方式对新协议进行验证,并没有发现新协议中的漏洞。通过两次验证工作的对比,得到具有高安全性的新协议;对比建模时采用的由类型检查、静态分析、语法重定序构成的三种不同组合优化策略,获得新协议最优的安全验证模型。除此之外,本文还提出通过程序枚举法代替手工求解攻击者知识库,以降低攻击者模型构建复杂度,使本文提出的攻击者模型建模方法适用于拥有更多主体的协议的分析与验证。