Towards automated formal security analysis of SAML V20 Web Browser SSO standard -- the POST/Artifact use case
<|reference_start|>Towards automated formal security analysis of SAML V20 Web Browser SSO standard -- the POST/Artifact use case: 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.<|reference_end|>
@article{hartl2024towards,
    title={Towards automated formal security analysis of SAML V2.0 Web Browser SSO
  standard -- the POST/Artifact use case},
    author={Zvonimir Hartl, Ante {DJ}erek},
    journal={arXiv preprint arXiv:2403.11859},
    year={2024},
    archivePrefix={arXiv},
    eprint={2403.11859},
    primaryClass={cs.CR}
}