Formal Analysis And Verification Of OAuth 2.0 Protocol Improved By Key Cryptosystems

Under the background of the big data era, researchers are exploring the solutions of data fusion and sharing. At the same time, the network information security also ushered in the unprecedented challenges, hackers like to find loopholes to launch malicious attacks and steal confidential information in the network. The network information transmission mainly depends on the network protocol, how to design a safe and reliable network protocol is the key to ensure the network information security. Formal methods is a technology based on strict mathematical which can be used to verify the protocol security properties and identify potential vulnerabilities, then to guide the design and implementation of security protocols.With realizing account relevance and resources sharing, the Internet Engineering Task Force designed and released OAuth 2.0 protocol. Users needn’t disclose name and password to the third party applications to get protected resources stored in resources server from now on. The defects make OAuth 2.0 being attacked, which also brings huge losses to enterprises and users. The reasons are OAuth 2.0 over-reliance on HTTPS to transmit data and ignore per-message encryption, and that the transmission efficiency of HTTPS is too low to work well under the poor network, so that the protocol triggers hacker attacks frequently.To solve the above problems, the improved OAuth 2.0 protocol, which transmit data by the HTTP channel and encrypt messages by public key system is presented. Furthermore, Promela language is utilized to model the improved protocol based on Delvo-Yao attacker model and Linear Temporal Logic is adopted to describe security properties of the protocol. Finally SPIN is utilized to check the model. The experimental results show that it can’t guarantee the security of OAuth 2.0 by depending solely public key encryption. On this basis, the further improvement strategy is proposed by utilizing private key signature to signature on key information of the protocol. Verifying the improved protocol by the same way, no holes have been found. Comparing two verification work, a new higher security protocol is acquired, compared with different protocol modeling by three combination optimization strategies such as type checking, static analysis and syntactic reordering, an optimal security verification model of the improved protocol is obtained. Furthermore, program enumeration is presented to instead of manual to obtain the attacker’s repository. The method above can reduce the complexity of modeling attacker effectively, so that the modeling method of attacker can be applied to analyze and validate multi-principal protocols.