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.

翻译：单点登录协议通过为多个在线服务提供统一登录入口，简化用户认证流程，从而提升可用性与安全性。作为最常用的SSO协议框架之一，安全断言标记语言V2.0 Web单点登录配置规范已投入使用二十余年，主要应用于政府、教育及企业环境。尽管该规范具有关键使命属性，目前仅对其特定部署与配置进行过形式化分析。本文试图通过针对SAML V2.0服务提供方发起的POST/Artifact绑定SSO用例开展全面形式化安全分析，以弥补这一研究空白。区别于聚焦特定部署配置的研究方法，我们严格遵循规范文本，旨在涵盖标准允许的多种不同部署场景。建模与分析工作采用密码学符号模型中最先进的安全协议自动化验证工具——Tamarin证明器完成。在技术层面，我们构建了该用例的元模型，并据此实例化出八种不同的协议变体。借助Tamarin证明器，我们形式化验证了这些协议变体的多项关键安全属性，同时识别出若干设计缺陷与潜在漏洞。