XIAO Meihua, CHENG Daolei, LI Wei, LI Ya'nan, LIU Xinqian, MEI Yingtian. Formal Analysis and Verification of OAuth 2.0 Protocol Improved by Key Cryptosystems[J]. Chinese Journal of Electronics, 2017, 26(3): 477-484. doi: 10.1049/cje.2017.04.003
Citation: XIAO Meihua, CHENG Daolei, LI Wei, LI Ya'nan, LIU Xinqian, MEI Yingtian. Formal Analysis and Verification of OAuth 2.0 Protocol Improved by Key Cryptosystems[J]. Chinese Journal of Electronics, 2017, 26(3): 477-484. doi: 10.1049/cje.2017.04.003

Formal Analysis and Verification of OAuth 2.0 Protocol Improved by Key Cryptosystems

doi: 10.1049/cje.2017.04.003
Funds:  This work is supported by the National Natural Science Foundation of China (No.61163005, No.61562026), the Natural Science Foundation of Jiangxi Province of China (No.20132BAB201033, No.20161BAB202063), the Science and Technology College in Jiangxi Province Ground Project (No.KJLD13038), the Co-Innovation Center of the Intelligent Management and Equipment for Orchard on the Hilly Land in South China, the Foreign Science and Technology Cooperation Project of Jiangxi Province (No.20151BDH80005), and the Project of Soft Science Research Project of Jiangxi Province (No.20151BBA10042).
  • Received Date: 2016-04-11
  • Rev Recd Date: 2016-07-07
  • Publish Date: 2017-05-10
  • The reasons which take huge losses to enterprises and users are:Open authorization (OAuth) 2.0 protocol is excessively dependent on Hyper text transfer protocol over secure socket layer (HTTPS) to transmit data and ignores per-message encryption, and the transmission efficiency of HTTPS is too low to work well under poor network. The improved OAuth 2.0 modified by Hyper text transfer protocol (HTTP), public key system and private key signature is proposed. With verifying the security of OAuth 2.0 by model checking technology, an improved protocol of higher security is acquired. Comparing different protocol modeling optimized by three combination optimization strategies which involve technologies such as type checking, static analysis and syntactic reordering, an optimal security verification model of the improved protocol is obtained. Program enumeration is presented to compute the repository of attacker. The modeling method of attacker above can effectively reduce the complexity of attacker modeling, consequently those methods can be applied to analyze and validate multi-principal protocols.
  • loading
  • D. Hardt, "The OAuth 2.0 Authorization Framework", IETF RFC 6749(Proposed Standard), https://tools.ietf.org/html/rfc6749, 2012-10.
    M. Jones and D. Hardt, "The OAuth 2.0 authorization framework:Bearer token usage", IETF RFC 6750, https://tools.ietf. org/html/rfc6750, 2012-10.
    Eran Hammer, "OAuth 2.0 and the road to hell", http://hueniverse.com/2012/07/26/oauth-2-0-and-the-road-to-hell/, 2012-7-26.
    WANG Huan-xiao, GU Chun-xiang and ZHENG Yong-hui, "Formal security analysis of OAuth2.0 authorization protocol", Journal of Information Engineering University, Vol.15, No.2, pp.141-147, 2014. (in Chinese)
    Pai S, Sharma Y, Kumar S, et al., "Formal verification of OAuth 2.0 using alloy framework", 2011 International Conference on Communication Systems and Network Technologies (CSNT), Jammu, India, pp.655-659, 2011.
    Bai G., Lei J., Meng G., et al., "AUTHSCAN:Automatic extraction of Web authentication protocols from implementations", Proceedings of 20th Annual Network and Distributed System Security Symposium, San Diego, California, USA, pp.24-27, 2013.
    CHENG Dao-lei, XIAO Mei-hua, LIU Xin-qian, et al., "Analyzing and verifying an open authorization protocol OAuth 2.0 with SPIN", Computer Engineering and Science, Vol.37, No.11, pp.2121-2127, 2015. (in Chinese)
    Paolo Maggi and R. Sisto, "Using SPIN to verify security properties of cryptographic protocols", Proc. of the 9th International SPIN Workshop on Model Checking of Software, LNCS 2318, Grenoble, France, pp.187-204, 2002.
    Dolev D. and Yao A.C., "On the security of public key protocols", IEEE Transactions on Information Theory, Vol.29, No.2, pp.198-208, 1983.
    Shan, Laixiang and Z. Qin. "LTL formulae to Buchi automata translation using on-the-Fly De-generalization", Chinese Journal of Electronics, Vol.24, No.4, pp.674-678, 2015.
    Andrade J.O. and Kameyama Y., "Efficient multi-valued bounded model checking for LTL over quasi-boolean algebras", IEICE Transactions on Information & Systems, Vol.95, No.5, pp.1355-1364, 2012.
    XIAO Meihua, CHENG Daolei and HU Lei, "Efficiently verify security properties of Woo-Lam protocol with spin/promela", Computer and Digital Engineering, Vol.42, No.10, pp.1768-1772, 1928, 2014. (in Chinese)
    Methni, Amira, Belgacem Ben Hedia, Matthieu Lemerre, et al., "State space reduction strategies for model checking concurrent C programs", In 9th Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS'15), Vol.1431, pp.65-76, 2015.
    J.F. Groote, T.W.D.M. Kouters and A. Osaiweran, "Specification guidelines to avoid the state space explosion problem", Software Testing, Verification and Reliability, Vol.25, No.1, pp.4-33, 2015.
    Cong Tian, S. Liu and Z. Duan, "Test case generation from conjunctions of predicates with model checking", Chinese Journal of Electronics, Vol.23, No.2, pp.271-277, 2014.
    S. Kolesnikov, A.V. Rhein, C. Hunsen, et al., "A comparison of product-based, feature-based, and family-based type checking", In ACM SIGPLAN Notices, Vol.49, No.3, pp.115-124, 2013.
    Kant G, Laarman A, Meijer J, et al., "Ltsmin:Highperformance language-independent model checking", Tools and Algorithms for the Construction and Analysis of Systems, Springer Berlin Heidelberg, pp.692-707, 2015.
    XIAO Meihua, JIANG Yun and LIU Qiaowei, "On formal analysis of cryptographic protocols and supporting tool", Chinese Journal of Electronics, Vol.19, No.2, pp.223-228, 2010.
    M. Xiao and J. Xue, "Formal automatic verification of security protocols", Proceedings of 2006 IEEE International Conference on Granular Computing, Atlanta, USA, pp.566-569, 2006.
  • 加载中


    通讯作者: 陈斌, bchen63@163.com
    • 1. 

      沈阳化工大学材料科学与工程学院 沈阳 110142

    1. 本站搜索
    2. 百度学术搜索
    3. 万方数据库搜索
    4. CNKI搜索

    Article Metrics

    Article views (183) PDF downloads(473) Cited by()
    Proportional views


    DownLoad:  Full-Size Img  PowerPoint