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

45 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

networking
Network protocols
Internet
consumer interest
internet community
authenticity
proliferation
privacy
integrity
website
Security systems
vulnerability
Authentication
acceptance
confidence
Formal verification
Websites
paradigm
examination
Specifications

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
Pai, Suhas ; Sharma, Yash ; Kumar, Sunil ; Pai, Radhika M. ; Singh, Sanjay. / Formal verification of OAuth 2.0 using alloy framework. Proceedings - 2011 International Conference on Communication Systems and Network Technologies, CSNT 2011. 2011. pp. 655-659
@inproceedings{e9c8fa8a8b884a02974fcb1b82e270d0,
title = "Formal verification of OAuth 2.0 using alloy framework",
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.",
author = "Suhas Pai and Yash Sharma and Sunil Kumar and Pai, {Radhika M.} and Sanjay Singh",
year = "2011",
doi = "10.1109/CSNT.2011.141",
language = "English",
isbn = "9780769544373",
pages = "655--659",
booktitle = "Proceedings - 2011 International Conference on Communication Systems and Network Technologies, CSNT 2011",

}

Pai, S, Sharma, Y, Kumar, S, Pai, RM & 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., 5966531, pp. 655-659, 2011 International Conference on Communication Systems and Network Technologies, CSNT 2011, Katra, Jammu, India, 03-06-11. https://doi.org/10.1109/CSNT.2011.141

Formal verification of OAuth 2.0 using alloy framework. / Pai, Suhas; Sharma, Yash; Kumar, Sunil; Pai, Radhika M.; Singh, Sanjay.

Proceedings - 2011 International Conference on Communication Systems and Network Technologies, CSNT 2011. 2011. p. 655-659 5966531.

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

TY - GEN

T1 - Formal verification of OAuth 2.0 using alloy framework

AU - Pai, Suhas

AU - Sharma, Yash

AU - Kumar, Sunil

AU - Pai, Radhika M.

AU - Singh, Sanjay

PY - 2011

Y1 - 2011

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=80052124769&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=80052124769&partnerID=8YFLogxK

U2 - 10.1109/CSNT.2011.141

DO - 10.1109/CSNT.2011.141

M3 - Conference contribution

SN - 9780769544373

SP - 655

EP - 659

BT - Proceedings - 2011 International Conference on Communication Systems and Network Technologies, CSNT 2011

ER -

Pai S, Sharma Y, Kumar S, Pai RM, Singh S. Formal verification of OAuth 2.0 using alloy framework. In Proceedings - 2011 International Conference on Communication Systems and Network Technologies, CSNT 2011. 2011. p. 655-659. 5966531 https://doi.org/10.1109/CSNT.2011.141