迈向 SAML V2.0 Web 浏览器 SSO 标准的自动化形式化安全分析——POST/Artifact 用例
密码学与安全
2026-01-21 v2
摘要
单点登录 (SSO) 协议通过为多个在线服务提供统一登录来简化用户身份验证，从而提高可用性和安全性。最常见的 SSO 协议框架之一——安全断言标记语言 V2.0 (SAML) Web SSO 配置文件——已使用二十多年，主要用于政府、教育和企业环境。尽管其具有关键任务性质，但仅对 Web SSO 配置文件的某些部署和配置进行了形式化分析。本文试图通过执行对 SAML V2.0 SP 发起的带有 POST/Artifact 绑定的 SSO 用例的全面形式化安全分析来弥补这一差距。我们未专注于特定的部署和配置，而是密切遵循规范，旨在捕获标准允许的许多不同部署。建模和分析使用 Tamarin prover 进行，这是在密码学符号模型中进行安全协议自动化验证的 SOTA 工具。在技术上，我们构建了该用例的元模型，并将其实例化为八种不同的协议变体。使用 Tamarin prover，我们正式验证了这些协议变体的若干关键安全属性，同时识别了某些缺陷和潜在漏洞。
引用
@article{arxiv.2403.11859,
title = {Towards automated formal security analysis of SAML V2.0 Web Browser SSO standard -- the POST/Artifact use case},
author = {Zvonimir Hartl and Ante Đerek},
journal= {arXiv preprint arXiv:2403.11859},
year = {2026}
}