Formal Verification of OAuth 2.0 Using Alloy Framework

Over the past few years, the paradigm of social networking has grown to such a degree that social networking websites have evolved into full-fledged platforms, catering to a wide range of consumer interests. The near-ubiquity of Internet access has facilitated the proliferation of users that indulge in social networking. However, this wide spread usage of the Internet and social networking in particular brings with it the need to design and implement a plethora of security enhancing and privacy preserving protocols and standards. Several protocols and security mechanisms have been proposed to ensure primary security features such as confidentiality, integrity, authenticity and non repudiation. However, ensuring the correctness of these protocols is crucial in ensuring user confidence in system security. Therefore, these protocols need to be verified in some formal sense that involves an exhaustive examination of the protocol flow and its state transitions. In this paper, we formalize OAuth, an authentication standard which has found wide acceptance in the Internet community. We formalize the protocol using a method called knowledge flow analysis, using the Alloy modeling language for specification and the Alloy Analyzer for verification. We show how the Alloy Analyzer successfully discovers the known security vulnerability in OAuth.