Formal verification of OAuth 2.0 using alloy framework

Suhas Pai, Yash Sharma, Sunil Kumar, Radhika M. Pai, Sanjay Singh

Research output: Chapter in Book/Report/Conference proceedingConference contribution

51 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationProceedings - 2011 International Conference on Communication Systems and Network Technologies, CSNT 2011
Pages655-659
Number of pages5
DOIs
Publication statusPublished - 2011
Event2011 International Conference on Communication Systems and Network Technologies, CSNT 2011 - Katra, Jammu, India
Duration: 03-06-201105-06-2011

Conference

Conference2011 International Conference on Communication Systems and Network Technologies, CSNT 2011
CountryIndia
CityKatra, Jammu
Period03-06-1105-06-11

    Fingerprint

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications
  • Communication

Cite this

Pai, S., Sharma, Y., Kumar, S., Pai, R. M., & Singh, S. (2011). Formal verification of OAuth 2.0 using alloy framework. In Proceedings - 2011 International Conference on Communication Systems and Network Technologies, CSNT 2011 (pp. 655-659). [5966531] https://doi.org/10.1109/CSNT.2011.141