Formal Analysis and Verification of OAuth 2.0 Protocol Improved by Key Cryptosystems
Meihua Xiao, Daolei Cheng, Wei Li, Yanan Li, Xinqian Liu, Yingtian Mei · Chinese Journal of Electronics · 2017
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.