Abstract:

The OAuth 2.0 is an open authorization protocol which solves the problem of user accounts associating and resources sharing. However, due to its weak security, massive user information of network companies is leaking. Besides, the https channel used by OAuth 2.0 to transmit data is inefficient, making the OAuth 2.0 an attack object   of hackers. We propose an open authorization protocol, which transmits the data of the OAuth 2.0 protocol in http channels, model the protocol based on the Promale language and DolevYao attacker model, and employ the SPIN for model checking. The results of formal analysis show that the OAuth2.0 protocol encrypted by the public key encryption system is unsafe. The proposed modeling method has great significance in formal analysis of similar license agreement.

Key words: OAuth 2.0 protocol;information leakage;public key encryption system;model checking