Formal Analysis and Verification of OAuth 2.0 in SSO

dc.contributorAalto-yliopistofi
dc.contributorAalto Universityen
dc.contributor.advisorPeltonen, Aleksi
dc.contributor.advisorPernilä, Tommi
dc.contributor.authorVasudevan, Anand
dc.contributor.schoolPerustieteiden korkeakoulufi
dc.contributor.supervisorAura, Tuomas
dc.date.accessioned2023-08-27T17:10:57Z
dc.date.available2023-08-27T17:10:57Z
dc.date.issued2023-08-21
dc.description.abstractThis thesis examines the OAuth 2.0 protocol within Single Sign-On (SSO) systems through modelling and formal analysis. The versatile Performing Security Proofs of Stateful Protocols (PSPSP), a theory for the Isabelle/HOL proof assistant was used to carry out the verification. Additionally the Open-Source Fixedpoint Model-Checker (OFMC), was used in this verification for its accessibility. PSPSP notably supports the modelling of mutable long-term state, a feature not common in many similar tools. The challenge lies in crafting a model that accurately mirrors real-world scenarios while integrating the OAuth 2.0 protocol on top of the TLS 1.2 protocol. The goal is to produce a model that is both realistic and doesn't induce false attack vectors in its abstraction. The complexity of combining SSO, OAuth, and TLS often necessitates simplifications for effective verification. This study explores the modelling of OAuth components without drastic over-simplifications, verifying each in isolation, and then applying compositional reasoning available in PSPSP/Isabelle to introduce the TLS protocol as well. This process necessitates a well-defined interface between components and verification of all components individually and in the composition. Both tools confirm the lack of detectable vulnerabilities in the OAuth 2.0 protocol, reinforcing its security and prominence in SSO systems. The research explores the process of modelling and formally verifying security protocols, and deepens the understanding of OAuth 2.0's role in SSO systems.en
dc.format.extent54
dc.format.mimetypeapplication/pdfen
dc.identifier.urihttps://aaltodoc.aalto.fi/handle/123456789/122826
dc.identifier.urnURN:NBN:fi:aalto-202308275167
dc.language.isoenen
dc.programmeMaster’s Programme in Security and Cloud Computing (SECCLO)fi
dc.programme.majorSecurity and Cloud Computingfi
dc.programme.mcodeSCI3113fi
dc.subject.keywordformal verificationen
dc.subject.keywordOAuth 2.0en
dc.subject.keywordSSOen
dc.subject.keywordPSPSPen
dc.subject.keywordOFMCen
dc.subject.keywordIsabelleen
dc.titleFormal Analysis and Verification of OAuth 2.0 in SSOen
dc.typeG2 Pro gradu, diplomityöfi
dc.type.ontasotMaster's thesisen
dc.type.ontasotDiplomityöfi
local.aalto.electroniconlyyes
local.aalto.openaccessyes
Files
Original bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
master_Vasudevan_Anand_2023.pdf
Size:
895.99 KB
Format:
Adobe Portable Document Format