• 中国计算机学会会刊
  • 中国科技核心期刊
  • 中文核心期刊

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

• 论文 • 上一篇    下一篇

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

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

  1. (华东交通大学软件学院,江西 南昌 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   

  1. (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

摘要:

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