Formal Specification And Verification Of OAuth Protocol

In the past years, Internet has become increasingly popular. A growing number of enterprises’systems need to be integrated with Internet, for promoting system performance and company profit. Meanwhile, it’s significant to share and integrate information inside the Internet for better system and service.To offer information sharing, Internet Engineering Task Force issued OAuth 1.0 in April, 2010. They gave a specification of OAuth protocol and offered a unified authorization flow. The third-party application can access users’resource without users’credentials. OAuth fixes the behaviors among the third-party application, authorization server and users, which implements the high reliable information sharing. However, how to ensure that each entity provides a trustworthy service when they communicate with each other?Considering this issue, we adopted a strict math method - formal method..Our study was based on the Authorization Code Flow in the OAuth 2.0, and adopted ASLan++ to comprehensively formalize the authorization protocol. ASLan++, the AVANTSSAR Specification Language, has been designed for formally specifying composed security-sensitive web services and service-oriented architectures, associating their security policies, as well as their trust and security properties, at both communication and application layers. We gave an analysis on confidentiality, authentication, authorization, consistency, error handling and short span access token, basing on the Authorization Code Flow formalized by ASLan++. Besides, AVANTSSAR provides many different kinds of back-ends like SATMC, they can automatically make a verification for formal model. We made a verification of those properties by SAT-based Model Checker and found some attacks such as the leakage of state & authorization and the violated consistency. At last, we gave an analysis why there are so many issues and provided solutions with solving those issues.