运用SPIN 对开放授权协议OAuth 2.0的分析与验证＊

程道雷，肖美华，刘欣倩，梅映天，李 伟

（华东交通大学软件学院，江西 南昌330013）

1 引言

OAuth（Open Authorization）［1］作为一种授权标准，用户无需将用户名和密码等信息提交给第三方应用，便能在第三方应用中获取其存储于其它平台的私密资源，该标准主要用于解决账号关联与资源共享问题。OAuth 2.0是OAuth协议的最新版本，不兼容OAuth 1.0，但降低了OAuth协议的编码复杂度，且为各平台的相关应用提供了对应的认证方式。近年来，OAuth 2.0协议的安全性漏洞引发了许多互联网安全问题，包括CSDN、facebook、亚马逊、新浪微博在内的众多著名网站遭受黑客攻击。因此，OAuth 2.0协议形式化分析与验证具有重要社会价值。

Pai S等［2］运用Alloy框架对OAuth 2.0进行形式化分析；Sun San－Tsai［3］通过利用基于OAuth 2.0的单点登录系统的实例表明OAuth 2.0虽然内容简单，但不安全；陈伟等［4］运用“数字签名技术”对OAuth 2.0进行改进，并基于Blanchet演算对其进行安全性分析；王焕孝等［5］运用协议分析工具SATMC，得出OAuth 2.0协议在失去https通道保护下的危险状态。由于OAuth 2.0协议当前依赖https 通道传输相关数据，而https 要运行SSL（Secure Sockets Layer）对传输数据加密，降低了https传输效率。根据相关调查研究，在北上广深以外的中国广大城市，有20%～25% 的用户都会遇到https连接困难，排查发现问题和接入点无关，信号和网络不稳定导致https 请求很难完成，导致一旦遭遇ARP（Address Resolution Protocol）攻击或中间人攻击，用户信息将遭窃取或破坏。本文提出使OAuth 2.0脱离https通道，通过“http＋消息加密”的方式传输数据，并将公钥密钥体系运用到该协议上，使用模型检测技术对协议进行安全性验证。

形式化方法主要包括模型检测（Model Checking）［6］与 定 理 证 明［7］两 个 分 支。SPIN（Simple Promela INterpreter）［8，9］是 一 种 著 名 的 协 议 模 型检测验 证 工 具。Maggi P 等［10］以Ndddam－Schroeder协议为实例，基于Dolev－Yao攻击模型［11］的思想，提出一种用于安全协议模型检测的建模方法。本文对该方法进行扩展，运用到包含多主体的授权协议的模型检测上。

由于OAuth 2.0 是一个崭新的授权协议，可供参考的运用形式化方法对该协议安全性验证研究成果仍然不足，本文探索使用模型检测技术对OAuth 2.0协议进行形式化分析与验证。首先，将OAuth 2.0协议进行简化，并用形式化方法对其进行描述，再运用公钥加密体系对协议进行加密，在对OAuth 2.0协议进行建模后，验证该协议是否能安全用在消息传输中，模型检测实验发现了中间人攻击序列图，因此得出公钥加密体系不能够保证OAuth 2.0协议安全的方法。

本文结构安排如下：第2 节对OAuth 2.0 协议进行简化及形式化表示，并运用公钥密码体系对协议加密；第3节阐述了OAuth 2.0 协议建模过程；第4节运用SPIN 对OAuth 2.0协议进行验证与分析；第5节为结束语。

2 OAuth 2.0协议及形式化表示

OAuth是一种第三方授权协议。首先，客户端发送Authorization Request（授权申请），向Resource Owner（资源拥有者）申请Access Grant（访问授权）；然后，使用Access Grant和Client Credentials（身份证书）与Authorization Server（授权服务器）交换Access Token（访问令牌，包含持续时间、作用范围等信息），最后客户端提交Access Token至Resource Owner（资源拥有者）获取受保护资源。具体过程如图1所示。

Figure 1 Flow of the abstract protocol图1 抽象协议流程

根据图1所示的协议流程，将OAuth 2.0 协议进行形式化表示，获得如下协议：

（1）Client→Resource Owner：Authorization Request；

（2）Resource Owner→Client：Access Grant；

（3）Client→Authorization Server：Access Grant，Client Credentials；

（4）Authorization Server→Client：Access Token；

（5）Client→Resource Server：Access Token；

（6）Resource Server→Client：Protected Resource。

如果将以上协议中未加密的消息直接通过http通道传输数据，所有的信息都将被攻击者轻而易举截获。因此，将OAuth 2.0 协议简化，并用公钥加密体系对消息进行加密，得到如下OAuth 2.0协议：

（1）C→RO：｛A＿r｝PKRO；

（2）RO→C：｛A＿g｝PKC；

（3）C→AS：｛A＿g，C＿c｝PKAS；

（4）AS→C：｛A＿t｝PKC；

（5）C→RS：｛A＿t｝PKRS；

（6）RS→C：｛P＿r｝PKC。

其中，PKC表示以C的公钥加密，任意经C的公钥加密的消息，只有C才能通过其私钥解开，其它主体类似。本文将运用模型检测技术对以上协议进行验证分析。

3 OAuth 2.0 协议建模

将OAuth 2.0 协议建模分为诚实主体建模和攻击者建模两个部分，其中，攻击者建模以Dolev－Yao攻击者模型为指导理论。

3.1 诚实主体建模

OAuth 2.0 协议的诚实主体包括Client、Resource Owner、Authorization Server 和Resource Server。结合Promela语言性质，我们分别为四个诚实主体定义各自的进程，依次命名为proctypePC（）、proctypePRO（）、proctypePAS（）和proctypePRS（）。由于诚实主体进程的定义方法非常类似，本文将以proctypePC（）的定义过程为例进行阐述。

本文所研究的内容为检测协议本身存在的漏洞，因此首先需要对模型做出如下几点假设：

（1）公钥加密算法本身没有漏洞；

（2）只有对应的密钥才能解密加密消息；

（3）攻击者可以是任何主体。

由于攻击者建模遵循Dolev－Yao攻击模型，因此诚实主体发送的所有消息都将被攻击者截获，而诚实主体所接收的消息，也全部由攻击者根据已有的知识组合生成或者直接转发截获的消息。依据该思想，建模过程需要借助Promela语言中的通道（chan）这一数据结构。将协议中传输的消息根据数据项的数目进行分类，同一类的消息使用同一个通道进行传输，因此，OAuth 2.0数据传输模拟需要两个参数不同的通道，将其进行如下定义：

chanca＝［0］of｛mtype，mtype，mtype｝

chancb＝［0］of ｛mtype，mtype，mtype，mtype｝

其中，协议中的消息（1）、（2）、（4）、（5）、（6）通过通道ca传输，消息（3）通过通道cb传输。值得注意的是ca和cb所定义的单位元素个数都比所需表示的消息元素多一项，这是因为通道中需要预留一个元素应对会话过程中的优化需要。具体原因如下：由于本文所要构建的是一个并发系统，因此各进程之间的交叉运行所产生的状态迁移量将非常庞大，甚至足以导致状态爆炸［12～15］，为了减少状态迁移的数量，在建模过程中，以ca为例，对通道作如下定义：发送语句ca！x1，x2，x3 中，x1 为消息接收者，x2是知识项，x3 是对x2 进行加密的公钥。接收语句ca？eval（x1），x2，eval（x3）中，eval函数被用作判断知识项是否与预期一致，从左到右依次判断，如果某处不一致，直接拒绝接收该消息。但是，攻击者需要截获所有诚实主体发送的消息，因此不需要通过eval来判断消息发送方，可直接定义为ca？＿，x1，x2。如此，可以减少大量无效消息。对Client的建模，具体如以下proctypePC（）的详细代码所示：

在PC进程中，self表 示 消 息 发 起 者，party1、party2、party3为消息接收者，g1和g2为泛型变量，用作表示主体C接收到的消息中的未知数据项。atomic为Promela语言中用来定义原子序列的语法规则，旨在减少进程交叉运行的次数，达到优化系统的目的。init＿start＿C＿RO、init＿commit＿C＿RO、init＿start＿C＿AS、init＿commit＿C＿AS和init＿start＿C＿RS为模型程序中定义的宏，被用来更新记录原子谓词的变量的值，这些原子谓词被用来表示协议性质。如果主体C发起对主体RO的协议会话，表示主体C参与了主体RO运行的协议。如果主体C完成了与主体RO的会话，则表明主体C提交了与主体RO的会话。根据以上原理，模型的每一条性质都需要用一个全局的Promela布尔变量表示，它们将在协议运行的特定阶段为真。通过对协议的分析，定义了如下原子谓词变量：

为了将模型中的所有性质运用到SPIN 工具的仿真过程中，本文将协议性质用LTL（线性时态逻辑）［16，17］刻画如下：

［］（（［］！commitCRO）‖（！commitCRO∪startROC））

［］（（［］！startCAS）‖（！startCAS∪commitCRO））

［］（（［］！commitCAS）‖（！commitCAS∪startASC））

［］（（［］！startCRS）‖（！startCRS∪commitCAS））

［］（（［］！commitCRS）‖（！commitCRS∪startRSC））

根据相同的规则，类似地定义主体RO的进程PRO和主体AS的进程PAS以及主体RS的进程PRS。

除定义好诚实主体进程之外，还要对初始进程作如下定义：

主体C作为整个协议的发起者，在协议模型中，他有可能向任意主体发起协议，如主体RO和主体HACKER。

3.2 攻击者建模

攻击者建模中，攻击者知识库创建最为关键，其主要由两部分知识项构成：第一部分为攻击者本身的初始知识库；另一部分知识项学习方法如下：攻击者每拦截到一条新消息后，便将学到的知识添加到知识库中。其添加方式分为两种：如截获的消息未经加密，则可直接获取其所有知识项并添加入库；如截获的消息已加密或者部分加密，则未经加密部分或者可以解密部分，直接或者解密后添加入库，如无法解密，将整个密文部分存入知识库中，以备需要时提取使用。

为简化知识项表示，攻击者知识项表示须遵循以下两点原则：（1）不表示攻击者不可能学会的知识项；（2）不表示诚实主体拒绝接受的消息（通过类型检查的方式判断）。基于以上两点，可以计算出需要表示的攻击者知识，如图2所示，攻击者潜在能学会的知识和攻击者需要学会的知识的交集为攻击者模型需要表示的知识。

Figure 2 Schematic of the attacker acquiring the knowledge which need to be indicated图2 攻击者模型中需要表示的知识项求解示意图

首先求解攻击者可以学会的知识。因为攻击者可以学会的知识，都是通过截获诚实主体发送的消息并对其进行相应处理所得，故可通过对诚实主体的发送消息语句进行分析，获得所需知识。攻击者 初 始 知 识 库 为 ｛C，RO，AS，RS，H，gD，R，PKH，PKRO，PKRS，PKAS，PKC｝，变量g1～g5的取值范围为｛C，RO，AS，RS，H，gD，PKH，PKRO，PKRS，PKAS，PKC｝，因此，可获得如表1所示的攻击者可学会的知识。

Table 1 Knowledge elements that the intruder can acquire表1 攻击者可学会的知识

接下来需要求解的是攻击者需学会的知识项。攻击者需要学会的知识，就是组成攻击者发送给诚实主体的消息的知识项。故可通过对诚实主体的接收消息语句进行分析，根据变量的不同取值，组合得到如表2所示的攻击者需要学会的知识。

Table 2 Knowledge elements the intruder needs表2 攻击者需要学会的知识项

由表1和表2的第2列求交集，可得到攻击者模型中需要表示的知识项，具体如图3所示。

Figure 3 Knowledge elements that need to be indicated in the attacker model图3 攻击者模型中需要表示的知识项

根据以上的研究基础与理论，编写攻击者模型代码，框架如下所示：

在Windows 7 64位系统、Cygwin 2.510.2.2以及SPIN 5.2.0构建的环境下进行仿真实验，发现了如图4所示的OAuth 2.0协议的中间人攻击序列。

Figure 4 Attack sequence diagram图4 攻击序列图

4 实验结果与分析

使用SPIN 工具，对上述模型进行验证，获得了如图4所示的攻击序列，并得到如下攻击过程：

（1）C→HACKER： ｛A＿r｝PKHACKER；HACKER→RO：｛A＿r｝PKRO；

（2）RO→HACKER：｛A＿g｝PKC；HACKER→C：｛A＿g｝PKC；

（3）C→HACKER： ｛A＿g，C＿c｝PKAS；HACKER→AS：｛A＿g，C＿c｝PKAS；

（4）AS→HACKER：｛A＿t｝PKC；HACKER→C：｛A＿t｝PKC；

（5）C→HACKER： ｛A＿t｝PKHACKER；HACKER→RS：｛A＿t｝PKRS；

（6）RS→HACKER： ｛P＿r｝PKHACKER；HACKER→C：｛P＿r｝PKC。

协议运行的第（6）步，资源服务器将受保护资源加密发送出来后，被攻击者截获后利用自己的私钥解密，从而窃取受保护资源，而C 并不知道自己接收到的消息实际是HACKER 转发而来的。

5 结束语

OAuth 2.0协议关系到用户账号、密码等个人隐私信息，与人们生活息息相关。本文提出使用http通道对OAuth 2.0协议数据进行传输，运用模型检测技术，通过Promela语言以及SPIN 工具对经公钥体系加密的OAuth 2.0协议运行过程进行仿真，发现一条中间人攻击路径。仿真结果表明，利用公钥加密体系对OAuth 2.0协议加密并不安全。下一步工作将尝试利用私钥体系对OAuth 2.0进行加密改进，并对其安全性进行验证。

［1］ Hardt D.The OAuth 2.0authorization framework（draft－ietfoatuth－v2－31）［EB/OL］.［2012－08－01］.https：//tools.ietf.org/id/draft－ieft.org/id/draft－ietf－oauth－v2－31.html.

［2］ Pai S，Sharma Y，Kumar S，et al.Formal verification of OAuth 2.0using Alloy framework［C］∥Proc of 2011International Conference on Communication Systems and Network Technologies（CSNT），2011：655－659.

［3］ Sun San－Tsai.Simple but not secure：An empirical security analysis of OAuth2.0－based single sign－on systems［D］.Vancouver：University of British Columbia，2012.

［4］ Chen Wei，Yang Yi－tong，Niu Le－yuan.Improved OAuth2.0 protocol and analysis of its security［J］.Computer Systems＆Applications，2014，23（3）：25－30.（in Chinese）

［5］ Wang Huan－xiao，Gu Chun－xiang，Zheng Yong－hui.Formal security analysis of OAuth 2.0authorization protocol［J］.Journal of Information Engineering University，2014，15（2）：141－147.（in Chinese）

［6］ Yu Peng，Wei Ou，Han Lan－sheng，et al.Model checking network transmission intervention policies［J］.Journal of Frontiers of Computer Science and Technology，2014，8（8）：906－918.（in Chinese）

［7］ Xiao M H，Ma C L，Deng C Y，et al.A novel approach to automatic security protocol analysis based on authentication event logic［J］.Chinese Journal of Electronics，2014，23（2）：235－241.

［8］ Holzmann G J.The model checker SPIN［J］.IEEE Transactions on Software Engineering，1997，23（5）：279－295.

［9］ Hu Liang－wen，Ma Jin－jing，Sun Bo.SPIN－based verification framework for SysML activity diagram［J］.Journal of Frontiers of Computer Science and Technology，2014，8（7）：836－847.（in Chinese）

［10］ Maggi P，Sisto R.Using SPIN to verify security properties of cryptographic protocols［C］∥Proc of the 9th International SPIN Workshop Grenoble，2002：187－204.

［11］ Dolev D，Yao A C.On the security of public key protocols［J］.IEEE Transactions on Information Theory，1983，29（2）：198－208.

［12］ Hou Gang，Zhou Kuan－jiu，Yong Jia－wei，et al.Survey of state explosion problem in model checking［J］.Computer Science，2013，40（z1）：77－85.（in Chinese）

［13］ Jamal B，Mohamed El－M，Hongyang Q，et al.Communicative commitments：Model checking and complexity analysis［J］.Knowledge－Based Systems，2012，35：21－34.

［14］ Yang Yuan－yuan，Ma Wen－ping，Liu Wei－bo.The construction of changeable intruder model in model checking［J］.Journal of Beijing University of Posts and Telecommunications，2011，34（2）：54－57.（in Chinese）

［15］ Li Xing－feng，Zhang Xin－chang，Yang Mei－hong，et al.Study on modularized model checking method based on SPIN［J］.Journal of Electronics ＆Information Technology，2011，33（4）：902－907.（in Chinese）

［16］ Xiao Mei－hua，Xue Jin－yun.Formal description of properties of concurrency system by temporal logic［J］.Journal of Naval University of Engineering，2004，16（5）：10－13.（in Chinese）

［17］ Salamah S，Ochoa O，Jacquez Y.Using pairwise testing to verify automatically－generated formal specifications［C］∥Proc of 2015IEEE 16th International Symposium on High Assurance Systems Engineering（HASE），2015：279－280.

附中文参考文献：

［4］ 陈伟，杨伊彤，牛乐园.改进的OAuth2.0协议及其安全性分析［J］.计算机系统应用，2014，23（3）：25－30.

［5］ 王焕孝，顾纯祥，郑永辉.开放授权协议OAuth2.0的安全性形式化分析［J］.信息工程大学报，2014，15（2）：141－147.

［6］ 余鹏，魏欧，韩兰胜，等.模型检测网络传播干预策略［J］.计算机科学与探索，2014，8（8）：906－918.

［9］ 胡良文，马金晶，孙博.基于SPIN 的SysML 活动图验证框架［J］.计算机科学与探索，2014，8（7）：836－847.

［12］ 侯刚，周宽久，勇嘉伟，等.模型检测中状态爆炸问题研究综述［J］.计算机科学，2013，40（z1）：77－85.

［14］ 杨元原，马文平，刘维博.模型检测中可变攻击者模型的构造［J］.北京邮电大学学报，2011，34（2）：54－57.

［15］ 李兴锋，张新常，杨美红，等.基于SPIN 的模块化模型检测方法研究［J］.电子与信息学报，2011，33（4）：902－907.

［16］ 肖美华，薛锦云.时态逻辑形式化描述并发系统性质［J］.海军工程大学学报，2004，16（5）：10－13.