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

J4 ›› 2015, Vol. 37 ›› Issue (11): 2121-2127.

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

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

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

收稿日期:2015-08-10 修回日期:2015-10-10 出版日期:2015-11-25 发布日期:2015-11-25
基金资助:
国家自然科学基金资助项目(61163005)；计算机软件新技术国家重点实验室开放课题资助项目(KFKT2012B18)；江西省自然科学基金资助项目(20132BAB201033)；江西省高校科技落地计划项目(KJLD13038)；江西省对外科技合作技术资助项目（20151BDH80005）；华东交通大学研究生创新计划资助项目（YC2014X007）

Analyzing and verifying an open authorization
protocol OAuth 2.0 with SPIN

CHENG Daolei,XIAO Meihua,LIU Xinqian,MEI Yingtian,LI Wei

（School of Software,East China Jiaotong University,Nanchang 330013,China）

Received:2015-08-10 Revised:2015-10-10 Online:2015-11-25 Published:2015-11-25

摘要/Abstract

摘要：

OAuth 2.0协议是一种开放授权协议，主要用于解决用户账号关联与资源共享问题。但是，其弱安全性导致各网络公司海量用户信息泄露,且OAuth 2.0传输数据采用的https通道效率低下,成为黑客攻击对象。提出采用http通道传输OAuth 2.0协议数据，基于Promale语言及DolevYao攻击者模型对OAuth 2.0协议建模，运用SPIN进行模型检测。形式化分析结果表明，采用公钥加密体系对OAuth 2.0协议进行加密不安全。上述建模方法对类似的授权协议形式化分析有重要借鉴意义。

关键词: OAuth 2.0协议, 信息泄露, 公钥加密体系, 模型检测

Abstract:

The OAuth 2.0 is an open authorization protocol which solves the problem of user accounts associating and resources sharing. However, due to its weak security, massive user information of network companies is leaking. Besides, the https channel used by OAuth 2.0 to transmit data is inefficient, making the OAuth 2.0 an attack object of hackers. We propose an open authorization protocol, which transmits the data of the OAuth 2.0 protocol in http channels, model the protocol based on the Promale language and DolevYao attacker model, and employ the SPIN for model checking. The results of formal analysis show that the OAuth2.0 protocol encrypted by the public key encryption system is unsafe. The proposed modeling method has great significance in formal analysis of similar license agreement.

Key words: OAuth 2.0 protocol;information leakage;public key encryption system;model checking

程道雷,肖美华,刘欣倩,梅映天,李伟. 运用SPIN对开放授权协议OAuth 2.0的分析与验证[J]. J4, 2015, 37(11): 2121-2127.

CHENG Daolei,XIAO Meihua,LIU Xinqian,MEI Yingtian,LI Wei. Analyzing and verifying an open authorization
protocol OAuth 2.0 with SPIN [J]. J4, 2015, 37(11): 2121-2127.

参考文献

［1］Hardt D.The OAuth 2.0 authorization framework(draftietfoatuth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.0 using Alloy framework［C］∥Proc of 2011 International 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.0 authorization 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 2015 IEEE 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.

[1]	李召恺, 马占有, 李健祥, 郭昊. 基于模糊决策过程的模糊计算树逻辑模型检测[J]. 计算机工程与科学, 2022, 44(02): 266-275.
[2]	郑小宇, 刘冬梅, 杜益宁, 周子健, 邱玫媚, 朱鸿. 模式驱动的系统安全性设计的验证[J]. 计算机工程与科学, 2020, 42(07): 1197-1207.
[3]	袁申,魏杰林,李永明. 具有多值决策过程的广义可能性计算树逻辑模型检测[J]. 计算机工程与科学, 2019, 41(01): 88-97.
[4]	钟小妹，肖美华，李伟，谌佳，李娅楠. RFID超轻量级认证协议RCIA形式化分析与改进[J]. 计算机工程与科学, 2018, 40(12): 2183-2192.
[5]	王亚鹏，雷丽晖. 基于CTL模型检测的胃腺癌核心路径形式化验证[J]. 计算机工程与科学, 2018, 40(12): 2280-2286.
[6]	雷丽晖，郭越，张延波. 可能性测度下的CTL符号化模型检测[J]. 计算机工程与科学, 2018, 40(11): 2008-2014.
[7]	肖美华1，梅映天1,2，李伟1，李娅楠1，钟小妹1，宋子繁1. 基于时间戳私钥签名技术的Nayak-T协议安全性分析[J]. 计算机工程与科学, 2017, 39(12): 2252-2259.
[8]	袁红娟1,2,马艳芳3,潘海玉1,2. 模糊交互时态逻辑的模型检测[J]. 计算机工程与科学, 2017, 39(12): 2290-2296.
[9]	吴格格，庄雷，张坤丽，王国卿. 移动支付协议PCMS的形式化分析和验证[J]. 计算机工程与科学, 2017, 39(01): 67-73.
[10]	马占有1，2，李永明1. 广义可能性决策过程的计算树逻辑模型检测[J]. J4, 2015, 37(11): 2162-2168.
[11]	刘姣，雷丽晖. 一种基于扩展不完全Kripke结构的三值逻辑模型检测方法[J]. J4, 2015, 37(10): 1884-1889.
[12]	刘玉军，汪明辉，蔡猛，陈坤. 降低Ad hoc网络信息泄露的路由算法[J]. J4, 2015, 37(06): 1087-1092.
[13]	徐亮，刘宏. 基于SMT的TECTL性质的限界模型检测方法[J]. J4, 2013, 35(10): 166-171.
[14]	伍江江,王志英,马俊,任江春,程勇,梅松竹. 一种基于虚拟隔离的数据可信存储技术研究与实现[J]. J4, 2012, 34(5): 58-62.
[15]	周璇,汪学明. 微支付协议Millicent的改进与模型检测[J]. J4, 2012, 34(12): 22-26.