基于OAuth2.0协议的安全授权模型研究

王婷婷+赵松泽

摘 要：本文在OAuth2.0授权码模型的基础上做出改进，采用HLPSL语言对授权码模型进行形式化建模，建立OAuth2.0协议授权码模型形式化模型，找到授权码模型出现安全漏洞的根本原因是客户端凭证可以被攻击者窃取。结合惰性无限状态方法和惰性攻击者优化方法对形式化模型分析和验证。提出OAuth2.0安全授权码模型，并分析和验证其在理论上无安全漏洞。通过的研究，本文可以提供一套安全的OAuth2.0授权协议模型，对目前安全要求高的开放平台的授权是有指导意义的。

关键词：OAuth2.0；安全；授权码模型；形式化

中图分类号：TP309 文献标识码：A

1 引言（Introduction）

近些年来，随着OAuth2.0協议的广泛应用，其安全性受到了人们的重点关注。2012至2014年期间，腾讯、新浪微博、Twitter、Facebook、Google等国内外大量知名网站因使用OAuth授权的开放平台而受到安全威胁，曾数次紧急公布修复方案。目前最主流的开放平台授权协议OAuth的授权模型的安全性一直受到企业应用者的关注，实质上是保证不同角色在交互过程中提供安全可信任的服务。OAuth2.0授权码模型是功能最完整、流程最严密的授权模式，也正因此授权码模型被广泛应用，但是频频曝出安全漏洞问题。从20世纪80年代以来，国内外出现了很多对安全协议进行形式化分析的方法，根据方法的性质不同，也出现很多不同的分类方法，本文根据形式化分析方法的表达能力分将其大致分为基于模型检测的安全协议分析方法、基于模型检测的安全协议分析方法和基于证明的安全协议分析方法。

OAuth在“客户端”与“服务提供商”之间，设置了一个授权层（authorization layer）。“客户端”不能直接登录“服务提供商”，只能登录授权层，以此将用户与客户端区分开来。“客户端”登录授权层所用的令牌（token），与用户的密码不同。用户可以在登录的时候，指定授权层令牌的权限范围和有效期。“客户端”登录授权层以后，“服务提供商”根据令牌的权限范围和有效期，向“客户端”开放用户储存的资料。

2 基于模型检测的安全协议形式化分析方法研究（Research on formal analysis method of security protocol based on model detection）

基于模型检测的安全协议分析和验证方法的基本思路是利用有限状态机理论，通过定义状态集合及状态迁移函数为安全协议建立模型；通过穷尽搜索状态空间来判断一些特殊的状态是否可达，或者是否可以生成一条特殊的状态转移路径，并以此检测该模型是否具备期望的安全性质。通用的做法是把安全协议看成一个分布式系统，单个主体涉及的协议执行部分称为局部状态，所有局部状态构成系统的全局状态；协议执行过程中，主体收发消息的动作会引起局部状态的改变，进而也引起全局状态的改变；在安全协议全局状态上定义安全属性或不变关系，则安全协议是否满足安全目标定价与系统可达的每个全局状态上安全属性或不变关系是否都能得到满足。

安全协议的模型检测分析方法取得了很大的成功，其优点是自动化程度高，可以借助自动分析工具来完成分析过程而不需要用户的参与，并且安全协议存在缺陷时能够自动生成相应的攻击实例。模型检测方法是基于Dolev-Yao模型。

本文采用基于模型检测的安全协议形式化分析验证方法，并使用OFMC形式化检测工具，OFMC是AVISPA平台的主要检测工具，也被称为On-the-Fly模型检测器，基于惰性攻击者思想，结合两种分析验证方法来优化和证明协议的正确性和完整性，第一种是使用惰性数据类型建立高效的无限状态空间；第二种是将符号技术和惰性Dolev-Yao攻击者模型最优化相结合的方法。