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

• Published in: Chinese Journal of Electronics 2017-05, Vol.26 (3), p.477-484
• Main Authors: Xiao, Meihua, Cheng, Daolei, Li, Wei, Li, Ya'nan, Liu, Xinqian, Mei, Yingtian
• Format: Article
• Language: English
• Subjects: attacker modeling method; attacker repository; authorisation; combination optimization strategies; formal analysis; formal verification; HTTPS; hyper text transfer protocol; hypermedia; key cryptosystems; Model checking; model checking technology; multiprincipal protocol analysis; multiprincipal protocol validation; OAuth 2.0 protocol; Open authorization 2.0 protocol; optimal security verification model; optimisation; Private key signature; Program enumeration; protocol modeling; public key cryptography; Public key system; secure socket layer; transport protocols
• ISSN: 1022-4653; 2075-5597
• DOI: 10.1049/cje.2017.04.003

The reasons which take huge losses to enterprises and users are:Open authorization(OAuth)2.0protocol 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.