Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Towards automated formal security analysis of SAML V2.0 Web Browser SSO standard -- the POST/Artifact use case

Zvonimir Hartl, Ante Đerek

TL;DR

This work tackles the problem of providing formal security guarantees for the SAML V2.0 Web Browser SSO POST/Artifact use case by employing the Tamarin prover to model the standard across eight protocol variants. The authors instantiate a meta-model to capture sensitive optional features and under-specified mechanisms, build a comprehensive formal model, and verify a broad set of security properties from the client, SP, and IdP perspectives, uncovering an artifact-session confusion vulnerability and proposing a mitigation. Key contributions include the first formal POST/Artifact model for SAML, automated proofs for critical secrecy, authenticity and freshness properties, and concrete guidance for mitigating identified weaknesses, alongside a discussion of the practical limitations of symbolic analysis. The results demonstrate that the POST/Artifact flow can satisfy core Web SSO security goals under many configurations, while highlighting how unspecified standard details can influence guarantees and informing future standard improvements and deployment practices.

Abstract

Single Sign-On (SSO) protocols streamline user authentication with a unified login for multiple online services, improving usability and security. One of the most common SSO protocol frameworks - the Security Assertion Markup Language V2.0 (SAML) Web SSO Profile - has been in use for more than two decades, primarily in government, education and enterprise environments. Despite its mission-critical nature, only certain deployments and configurations of the Web SSO Profile have been formally analyzed. This paper attempts to bridge this gap by performing a comprehensive formal security analysis of the SAML V2.0 SP-initiated SSO with POST/Artifact Bindings use case. Rather than focusing on a specific deployment and configuration, we closely follow the specification with the goal of capturing many different deployments allowed by the standard. Modeling and analysis is performed using Tamarin prover - state-of-the-art tool for automated verification of security protocols in the symbolic model of cryptography. Technically, we build a meta-model of the use case that we instantiate to eight different protocol variants. Using the Tamarin prover, we formally verify a number of critical security properties for those protocol variants, while identifying certain drawbacks and potential vulnerabilities.

Towards automated formal security analysis of SAML V2.0 Web Browser SSO standard -- the POST/Artifact use case

TL;DR

This work tackles the problem of providing formal security guarantees for the SAML V2.0 Web Browser SSO POST/Artifact use case by employing the Tamarin prover to model the standard across eight protocol variants. The authors instantiate a meta-model to capture sensitive optional features and under-specified mechanisms, build a comprehensive formal model, and verify a broad set of security properties from the client, SP, and IdP perspectives, uncovering an artifact-session confusion vulnerability and proposing a mitigation. Key contributions include the first formal POST/Artifact model for SAML, automated proofs for critical secrecy, authenticity and freshness properties, and concrete guidance for mitigating identified weaknesses, alongside a discussion of the practical limitations of symbolic analysis. The results demonstrate that the POST/Artifact flow can satisfy core Web SSO security goals under many configurations, while highlighting how unspecified standard details can influence guarantees and informing future standard improvements and deployment practices.

Abstract

Single Sign-On (SSO) protocols streamline user authentication with a unified login for multiple online services, improving usability and security. One of the most common SSO protocol frameworks - the Security Assertion Markup Language V2.0 (SAML) Web SSO Profile - has been in use for more than two decades, primarily in government, education and enterprise environments. Despite its mission-critical nature, only certain deployments and configurations of the Web SSO Profile have been formally analyzed. This paper attempts to bridge this gap by performing a comprehensive formal security analysis of the SAML V2.0 SP-initiated SSO with POST/Artifact Bindings use case. Rather than focusing on a specific deployment and configuration, we closely follow the specification with the goal of capturing many different deployments allowed by the standard. Modeling and analysis is performed using Tamarin prover - state-of-the-art tool for automated verification of security protocols in the symbolic model of cryptography. Technically, we build a meta-model of the use case that we instantiate to eight different protocol variants. Using the Tamarin prover, we formally verify a number of critical security properties for those protocol variants, while identifying certain drawbacks and potential vulnerabilities.
Paper Structure (30 sections, 3 figures, 4 tables)

This paper contains 30 sections, 3 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Related work
  3. Background
  4. SAML Framework
  5. Web Browser SSO Profile
  6. SP-initiated SSO with POST/Artifact Bindings
  7. Tamarin prover
  8. Formal model
  9. Methodology and Model Variants
  10. Communication channels
  11. System setup
  12. SAML parties -- the SP and the IdP
  13. Client modeling
  14. Threat Model and The Adversary
  15. Limitations
  16. ...and 15 more sections

Figures (3)

  • Figure 1: An example protocol execution of SAML V2.0 SSO SP-Initiated SSO with POST/Artifact bindings use case. Steps outside the scope of SAML Web Browser SSO Profile are grayed out.
  • Figure 2: Prerequisites Rules state machine. Initialized agent can become one of three honest parties or become compromised. Clients (and the adversary) can register resources at SPs (honest or compromised). Client (and the adversary) can register at IdPs (honest or compromised). Finally, any two SAML parties (SP and IdP) can establish trust.
  • Figure :