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

单点登录（SSO）协议通过为多个在线服务提供统一的登录方式简化了用户身份验证，提高了可用性和安全性。其中最常见的SSO协议框架之一——安全声明标记语言V2.0（SAML）Web SSO Profile已经在政府、教育和企业环境中使用了二十多年。尽管它具有关键任务，但Web SSO Profile的某些部署和配置仅被正式分析过一次。本文试图通过对SAML V2.0 SP-initiated SSO with POST/Artifact Bindings use case进行全面的正式安全分析来弥补这一空白。我们不是专注于特定的部署和配置，而是紧密遵循规范，旨在捕捉标准允许的许多不同部署。我们使用Tamarin prover进行建模和分析，这是一种在密码学符号模型中自动验证安全协议的最先进工具。从技术上讲，我们构建了一个用例的元模型，我们将其实例化为八个不同的协议变体。使用Tamarin prover，我们正式验证了这些协议变体的许多关键安全属性，同时确定了某些缺点和潜在漏洞。

对SAML V2.0 SP-initiated SSO with POST/Artifact Bindings使用案例进行全面的形式化安全分析，以验证其安全性和识别潜在漏洞。

使用Tamarin prover工具，建立一个元模型并将其实例化为八个不同的协议变体，对这些变体验证一些关键的安全属性，同时识别出某些缺陷和潜在漏洞。

使用了Tamarin prover作为自动验证安全协议的工具，实现了对SAML V2.0 SP-initiated SSO with POST/Artifact Bindings使用案例的全面形式化安全分析，并识别出了潜在漏洞。

最近的相关研究包括：1.《基于SAML的Web单点登录协议的形式化安全验证》，2.《基于安全协议形式化验证技术的研究综述》。