Abstract: During the past several years, OAuth 2.0 protocol has been widely implemented and deployed. In order to give a strong confidence in its security to the people, in this study, Blanchet calculus in computational model is used to analyze OAuth 2.0 protocol with mechanized tool CryptoVerif. The term, process and correspondence are used to model OAuth 2.0 protocol . The authentication is formalized by non-injective or injective correspondence. The results show that OAuth 2.0 protocol has not authentication between the resource owner and authorization server, authentication between client and authorization server. The first automatic analysis on OAuth 2.0 protocol in computational model of in active adversary is implemented in this study.