Formal Analysis and Verification of OAuth 2.0 in SSO

Loading...
Thumbnail Image
Journal Title
Journal ISSN
Volume Title
Perustieteiden korkeakoulu | Master's thesis
Date
2023-08-21
Department
Major/Subject
Security and Cloud Computing
Mcode
SCI3113
Degree programme
Master’s Programme in Security and Cloud Computing (SECCLO)
Language
en
Pages
54
Series
Abstract
This 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.
Description
Supervisor
Aura, Tuomas
Thesis advisor
Peltonen, Aleksi
Pernilä, Tommi
Keywords
formal verification, OAuth 2.0, SSO, PSPSP, OFMC, Isabelle
Other note
Citation