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 

机构地区：[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

出　　处：《Chinese Journal of Electronics》2017年第3期477-484,共8页电子学报（英文版）

基　　金：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);the Project of Soft Science Research Project of Jiangxi Province(No.20151BBA10042)

摘　　要：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.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.

关 键 词：OAutb 2.0 protocol Model checking Public key system Private key signature Program enumeration. 

分 类 号：TN918.4[电子电信—通信与信息系统]