Formal Verification on Oauth2.0: Using AVISPA
CSTR:
Author:
  • Article
  • | |
  • Metrics
  • |
  • Reference [18]
  • |
  • Related
  • |
  • Cited by
  • | |
  • Comments
    Abstract:

    OAuth is an protocol used to identify the client, and control resource access. Because it concerns about the privacy of the private resource owner, the security of OAuth protocol is fairly important. This paper mainly research on the OAuth2.0 protocol text, and make an abstraction on it, build an model in AVISPA, an formal verification tool for security protocols, and then verify the model in AVISPA. Finally, we find there is an attack mode that may result in leaking the private resource to attackers. We suggest a way to model the message to be authenticated as a symmetric key, which is innovative. This modelling and verification method we used on analyzing OAuth2.0 can be used in the verification of other security protocols, like the online payment protocol.

    Reference
    1 Miller SP, et al. Kerberos authentication and authorization system. Project Athena Technical Plan. 1987.
    2 Hardt D. The OAuth 2.0 authorization framework. 2012.
    3 Clarke EM, Wing JM. Formal methods: State of the art and future directions. ACM Computing Surveys (CSUR),1996, 28(4): 626-643.
    4 卿斯汉.安全协议.北京:清华大学出版社,2005.
    5 Chari S, Jutla CS, Roy A. Universally Composable Security Analysis of OAuth v2. 0. IACR Cryptology ePrint Archive, 2011: 526.
    6 Xu X, Niu L, Meng B. Automatic verification of security properties of OAuth 2.0 protocol with cryptoverif in computational model. Information Technology Journal, 2013, 12(12).
    7 Pai, Suhas, et al. Formal verification of OAuth 2.0 using Alloy framework. 2011 International Conference on Communication Systems and Network Technologies (CSNT). IEEE, 2011.
    8 AVISPA webiste. http://www.avispa-project.org/
    9 Armando A, Basin D, Boichut Y, et al. The AVISPA tool for the automated validation of internet security protocols and applications. Computer Aided Verification. Springer Berlin Heidelberg, 2005: 281-285.
    10 Moskewicz MW, Madigan CF, Zhao Y, et al. Chaff: Engineering an efficient SAT solver. Proc. of the 38th Annual Design Automation Conference. ACM. 2001. 530-535.
    11 Holzmann GJ. Algorithms for automated protocol verification. AT&T Technical Journal, 1990, 69(1): 32-44.
    12 Meadows CA. Formal verification of cryptographic protocols: A survey. Springer Berlin Heidelberg, 1995.
    13 Viganò L. Automated security protocol analysis with the AVISPA tool. Electronic Notes in Theoretical Computer Science, 2006, 155: 61-86.
    14 Hammer-Lahav DE, Hardt D. The OAuth2. 0 Authorization Protocol. IETF Internet Draft. 2011.
    15 AVISPA Team HLPSL Tutorial. European Community under the Information Society Technologies Program. http://www. AVISPA-project.org
    16 Lodderstedt T, McGloin M, Hunt P. OAuth 2.0 threat model and security considerations. http://tools.ietf.org/html/ rfc6819. 2013.
    17 Paul R. Compromising Twitter's OAuth security system. http://arstechnica.com/security/2010/09/twitter-a-case-study-on-how-to-do-oauth-wrong/.
    18 Ping0s. OAuth认证机制中普遍的安全问题, http://www. freebuf.com/articles/web/5997.html.
    Related
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

郭丹青. OAuth2.0协议形式化验证: 使用AVISPA.计算机系统应用,2014,23(11):196-202

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:March 03,2014
  • Revised:March 24,2014
  • Online: November 20,2014
Article QR Code
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-3
Address:4# South Fourth Street, Zhongguancun,Haidian, Beijing,Postal Code:100190
Phone:010-62661041 Fax: Email:csa (a) iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063