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

XIAO Meihua; CHENG Daolei; LI Wei; LI Ya'nan; LIU Xinqian; MEI Yingtian

doi:10.1049/cje.2017.04.003

Volume 26 Issue 3

Turn off MathJax

Article Contents

Article Navigation > Chinese Journal of Electronics > 2017 > 26(3): 477-484

XIAO Meihua, CHENG Daolei, LI Wei, et al., “Formal Analysis and Verification of OAuth 2.0 Protocol Improved by Key Cryptosystems,” Chinese Journal of Electronics, vol. 26, no. 3, pp. 477-484, 2017, doi: 10.1049/cje.2017.04.003

Citation:

XIAO Meihua, CHENG Daolei, LI Wei, et al., “Formal Analysis and Verification of OAuth 2.0 Protocol Improved by Key Cryptosystems,” Chinese Journal of Electronics, vol. 26, no. 3, pp. 477-484, 2017, doi: 10.1049/cje.2017.04.003

Citation:

PDF( 741 KB)

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

doi: 10.1049/cje.2017.04.003

1.
School of Software, East China Jiaotong University, Nanchang 330013, China;
2.
Co-Innovation Center of the Intelligent Management and Equipment for Orchard on the Hilly Land in South China, Nanchang 330013, China

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

Abstract

Abstract

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.
- OAuth 2.0 protocol,
- Model checking,
- Public key system,
- Private key signature,
- Program enumeration

FullText(HTML)

References(19)

References

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.

Relative Articles

Supplements(0)

Cited By

Proportional views