恶意服务提供商环境下CAS的形式化分析：对信任感知部署的影响

《Computers & Security》：Formal analysis of CAS under malicious service providers: Implications for trust-aware deployments

　　

摘要

单点登录（SSO）协议被广泛部署为Web应用程序的核心身份组件，其中认证结果被多个下游服务消费。然而，针对CAS协议的正式分析很少将服务提供商作为主动的对抗性参与者来考察。本文使用Tamarin，在恶意服务提供商威胁模型下对Central Authentication Service（CAS）协议进行了正式分析。我们的分析评估了20个验证目标，涵盖两种威胁模型下的10类安全属性，覆盖从服务访问和重定向到票据验证、本地会话建立和资源获取的核心CAS登录与服务票据验证工作流。结果表明，CAS票据的核心机密性和真实性得到了确认，同时识别出与服务提供商真实性以及部署敏感型会话/资源隔离相关的违规问题（在部署绑定不充分的情况下）。我们进一步分析了当未保留服务来源溯源信息时，服务来源混淆可能如何影响复用SSO认证事件进行策略或信誉决策的下游系统。这些发现突显了从协议到部署的安全差距，并提出两种互补的防御措施：回调流程标识符绑定以及验证成功绑定到提交的服务票据，二者共同强制执行更严格的逐流程服务提供商状态隔离。

引言

在当今互联互通的数字生态系统中，用户经常访问多个应用程序（例如课程系统、图书馆、电子邮件），但传统的密码认证要求反复输入凭证。这导致了碎片化的用户体验，并增加了安全风险，例如由于记忆多个密码的认知负担而导致弱密码重用问题（Stobert和Biddle, 2018）。单点登录（SSO）技术通过实现集中认证来解决这些挑战。在更广泛的身份与访问控制生态系统中，相关技术承担不同角色：OAuth 2.0提供授权委托（Hardt, 2012），OIDC在OAuth 2.0之上添加身份层（Sakimura et al., 2023），SAML配置文件用于联合SSO部署（Ragouzis et al., 2008），而WebAuthn提供强用户认证机制（Balfanz et al., 2019）。在这一格局中，Central Authentication Service（CAS）协议因其开源特性、基于票据的设计以及与Web架构的兼容性，已成为教育、企业和政府领域广泛采用的轻量级Web SSO协议（Apereo Foundation, 2025, Yale University, 2025）。

尽管CAS设计轻量，其安全性不仅取决于CAS服务器和票据的加密新鲜性，还取决于服务提供商如何启动、验证并完成认证流程。在典型的CAS部署中，服务提供商决定初始重定向中使用的service参数，在认证成功后接收服务票据，向CAS服务器验证票据，并建立本地应用程序会话。这些步骤在用户目标服务、回调端点、签发的服务票据和生成的本地会话之间创建了重要的绑定。如果这些绑定不完整或仅由部署逻辑隐式强制，那么偏离预定协议行为的服务提供商可能会影响整体SSO流程的安全性，而不破坏CAS票据的加密构造。

这一担忧在大规模CAS部署中尤为相关，其中服务提供商不一定与CAS服务器由同一管理实体控制。在教育、企业和政府环境中，服务可能随时间集成，由不同部门运营，由第三方团队维护，或暴露于被入侵和错误配置的风险中。先前的SSO部署研究表明，服务提供商端的错误和集成缺陷可能导致严重的认证问题（Sun et al., 2012）。2022年Okta入侵等高调事件进一步说明，单个被入侵的身份相关组件如何影响众多下游组织和服务（Okta, 2022）。这些观察促使我们不仅将服务提供商视为诚实的协议参与者，也将其视为潜在的恶意或被入侵实体。

在本工作中，我们针对CAS协议弥补了这一差距。现有SSO协议的正式分析主要关注令牌机密性、认证和网络级攻击者，而对服务提供商本身成为主动对抗性参与者的情况关注较少。我们的目标并非质疑CAS票据生成或验证的加密强度。相反，我们提出这样一个问题：当不再假定服务提供商遵循预定协议时，围绕CAS票据的协议级和部署级绑定是否仍然充分。这一区别很重要：CAS服务器可能正确地签发和验证票据，而周围的重定向、回调、会话建立或资源访问上下文仍可能被恶意服务提供商操纵。

该问题在现代IAM部署中也可能产生下游后果，其中SSO认证事件被复用到即时登录决策之外。例如，零信任架构强调持续评估并避免对内部组件的隐式信任（Rose et al., 2020, Wang et al., 2025）；类似地，基于信誉的、风险自适应的或信任感知的访问控制系统可能消费认证日志作为后续授权决策的证据。在这种情况下，组合的安全性取决于事件记录是否保留了关于发起服务提供商、回调端点以及用户最终到达的服务的充分溯源信息。如果缺少这些溯源信息，攻击者诱导的认证事件可能仅被归因于用户，即使它们是由恶意或被入侵的服务提供商导致的。下游策略引擎可能根据其配置的策略做出反应；部署风险在于事件归因的不完整性，而非策略引擎本身。

基于这些观察，本工作在恶意服务提供商威胁模型下分析CAS协议。我们开发了CAS认证工作流的Tamarin模型，并验证涵盖票据机密性、认证一致性、服务提供商真实性、本地会话建立和资源访问的安全属性。我们在受HTTPS通道抽象约束的符号网络攻击者模型下，以及服务提供商可能偏离预定协议的扩展模型下分析该模型。

这一分析使我们能够区分由CAS票据机制保留的安全属性与那些一旦服务提供商被允许操纵重定向、回调或应用级会话行为就变得敏感于部署上下文的属性。特别是，我们的结果表明CAS票据机密性和票据一致性仍然健壮，而与服务提供商真实性、本地会话处理和资源访问相关的属性可能在重定向、回调或应用级会话上下文未被部署充分约束时失效。

我们的主要贡献总结如下：

• 据我们所知，本工作首次公开了CAS 3.0核心登录和服务票据验证工作流在选择性服务提供商损坏下的Tamarin模型。

• 我们通过纳入超越标准Dolev-Yao网络攻击者的恶意服务提供商场景扩展了传统正式分析。我们的模型明确捕获服务提供商偏离诚实行为以操纵重定向、回调、验证或本地会话流的威胁，反映了大规模SSO部署中的现实条件。

• 我们的系统验证识别出六项失败的验证结果和16个反例轨迹，这些反例汇聚为少数重复出现的违规模式。我们将这些发现分类为服务来源真实性失败、部署敏感型会话和资源隔离失败，以及一个属于CAS票据验证范围之外的密码钓鱼轨迹。值得注意的是，虽然我们确认了协议在保持CAS票据机密性和真实性方面的核心强度，但我们识别出当服务提供商表现恶意行为或并发流程未被充分隔离时变得关键的交互级弱点。

• 我们提出两种具体的修复机制——流程标识符绑定和ST成功绑定——并使用Tamarin证明器对强化后的CAS变体进行正式重新验证。结果表明，流程标识符绑定消除了服务来源混淆反例，ST成功绑定防止会话和资源混淆，二者的组合修复了两类违规。

SSO协议的正式分析。广泛的研究已将形式化方法应用于分析Web SSO协议，主要关注SAML、OpenID Connect（OIDC）和OAuth 2.0。这些研究表明SSO安全性不仅取决于令牌机密性和认证，还取决于浏览器重定向、服务身份、协议会话和本地应用状态之间的正确绑定。我们的工作遵循这一研究方向，但在协议范围和威胁模型上有所不同：我们聚焦于Central Authentication Service（CAS），一种基于票据的SSO协议，并分析当服务提供商本身可能偏离预定协议时的行为。

SAML与基于浏览器的SSO。Armando等人（2008）的早期工作发现了SAML 2.0部署中的关键漏洞，包括由基于浏览器SSO流程中认证上下文绑定不足引起的攻击。Armando等人（2013）的后续工作进一步分析了基于浏览器SSO协议中的认证缺陷，并展示了恶意或行为异常的服务提供商如何干扰用户的认证尝试。最近，Hartl和Derek（2025）探索了使用Tamarin对SAML V2.0 POST/Artifact配置文件的自动化分析。

这些研究与我们的工作密切相关，因为它们强调了将浏览器中介的重定向绑定到预期服务身份和协议会话的重要性。然而，它们聚焦于SAML配置文件和基于XML的断言处理。CAS使用不同的基于票据的工作流，以票据授予票据、服务票据、服务参数、回调处理和服务端票据验证为中心。因此，CAS需要一个独立的正式模型来分析当其票据和回调工作流在服务提供商不被假定为诚实时是否仍然安全。

OpenID Connect与OAuth 2.0。对于OIDC，Fett等人（2017）提供了全面的正式分析，在一个富表达力的Web模型中证明了认证和会话完整性属性。后续工作将这一分析扩展到金融级API（Fett et al., 2019, Hosseyni et al., 2024），纳入了详细的浏览器语义和更强的安全要求。OAuth 2.0也已使用不同的正式框架进行了严格分析，包括ProVerif（Bansal et al., 2012）、Alloy（Pai et al., 2011）和可组合安全模型（Chari et al., 2011）。这些分析揭示了令牌替换、跨站登录伪造和授权流程混淆等重要问题（Wang et al., 2012）。

与这些工作相比，我们的贡献并非一般性地声称先前的SSO分析忽略了所有恶意参与者。我们的贡献是CAS特定的。现有的OAuth/OIDC分析研究具有不同制品、重定向语义和客户端角色的协议。它们没有提供在恶意CAS服务提供商模型下对CAS票据授予票据、服务票据、回调、验证和本地会话工作流的Tamarin模型。因此，我们的分析通过考察类似的绑定和会话上下文问题如何在CAS中产生，补充了先前的OAuth/OIDC工作。

CAS的安全分析与部署。与SAML和OIDC/OAuth相比，CAS协议从形式化验证社区获得的关注有限。CAS规范将CAS定义为一种基于票据的单点登录协议，用户向CAS服务器认证一次并获得服务票据以访问受保护的应用程序（Apereo Foundation, 2025, Yale University, 2025）。现有关于CAS安全的公开证据大多与实现或部署相关。已报告的问题包括开放重定向漏洞，如CVE-2024-11207（National Vulnerability Database, 2026b）、旧版本中的LDAP注入，如CVE-2015-1169（National Vulnerability Database, 2026a），以及通过IP地址欺骗绕过多因素认证，如CVE-2023-4612（National Vulnerability Database, 2026）。这些报告表明CAS部署可能受到实现和配置错误的影响，但它们没有提供在恶意服务提供商威胁模型下对CAS的协议级保证。

我们的工作通过构建CAS特定的Tamarin正式模型并验证涵盖完整认证工作流的安全属性来弥补这一差距，从服务访问和重定向到票据验证、本地会话建立和资源获取。该分析区分了由CAS票据机制保留的属性与一旦允许服务提供商操纵重定向、回调、验证或应用级会话行为就变得敏感于部署上下文的属性。

风险感知访问控制中的SSO事件。零信任架构强调持续评估并避免对内部组件的隐式信任（Rose et al., 2020）。在此类环境中，以及在其它风险感知或基于信誉的访问控制系统中，SSO认证事件可能被复用到即时登录决策之外，作为策略、日志或行为评估的一部分。这促使我们不仅考察CAS票据是否保持机密和真实，还考察恶意服务提供商是否可以通过影响下游系统如何解释认证事件的方式来操纵CAS流程。

因此，我们分析了服务来源混淆的一个下游影响。如果攻击者诱导的CAS认证流程在记录时没有充分的服务来源溯源信息，生成的事件可能被仅归因于用户而非诱导该流程的恶意或被入侵的服务提供商。这并不意味着下游策略引擎必然有错误；它突显了当CAS认证事件被信任感知的访问控制机制复用时在部署级的归因假设问题。

据我们所知，尚无任何先前工作在恶意服务提供商威胁模型下提供针对CAS的特定形式化分析，同时也检验了由此产生的下游事件归因后果。

**节选片段**

**CAS单点登录协议**

中央认证服务（CAS）是一种广泛部署的开源单点登录（SSO）协议，最初由耶鲁大学开发（Apereo Foundation, 2025, Yale University, 2025）。根据CAS协议3.0规范，CAS通过单一可信服务器集中进行用户认证，以实现"一次登录，处处访问"。尽管该规范正式定义了五个实体（Client、CAS Client、CAS Server、Application和Back-end Service），我们的形式化模型……

**威胁模型与部署假设**

为评估CAS协议的安全性，我们考虑两种对抗能力：网络对手和潜在恶意的服务提供商（SP）。网络对手捕获对消息传递的攻击，而恶意SP模型捕获参与CAS工作流的应用程序的偏差行为。我们的Tamarin模型通过在默认符号网络模型之上添加显式的角色偏差和妥协规则来编码这些能力。

**网络对手。** 我们假设……

**CAS的形式化模型**

我们将CAS协议模型结构化为三个部分。第4.1节定义了模型中使用的通信信道抽象和对手接口。第4.2节介绍了参与者初始化和后续威胁模型限制中使用的信任标签。第4.3节则呈现了CAS认证的主要工作流，从初始服务请求到票据签发、票据验证、本地会话建立以及资源访问。

我们的模型针对核心工作流……

**安全属性规范**

本节建立了CAS协议的形式化安全属性，涵盖两种对手模型下的20项属性：标准Dolev-Yao模型和带有恶意服务提供商的扩展模型。

我们首先将协议形式化定义为??CAS=(??,?)，其中??是谓词和函数的签名，?由协议转换的22条多重集重写规则组成。基于实体初始化标签（第4.2节），我们定义了两个公式来表示这些……

**结果**

本节呈现了CAS协议形式化验证的综合安全分析结果。我们的系统检查揭示了既保留的安全保证，也揭示了取决于所选威胁和部署假设的形式化弱点。

**实验设置。** 所有实验均在配备Intel(R) Xeon(R) Gold 5218R CPU @ 2.10 GHz的服务器上执行，具有503 GB内存，使用最多8个线程进行并行证明搜索。所有验证任务均使用Tamarin版本1.10.0。

**CAS变体与重新验证**

受第6节报告的违规情况启发，我们引入了两种协议级别的加固机制，并将其纳入Tamarin中修订后的CAS模型。第一种机制将前向通道回调绑定到本地发起的认证流程，第二种机制将每个后向通道验证响应绑定到SP提交的精确服务票据。基于这些机制，我们构建并验证了三种加固的CAS变体。此分析服务于两个目的：首先，……

**讨论**

**安全影响。** 我们的分析表明，CAS的安全性不仅取决于票据的保密性和真实性，还取决于这些票据被签发、重定向、验证和消费时所处认证环境的完整性。一旦放松了对可信服务提供商（SP）的假设，原始CAS模型表现出??Sess、??Res、??Pwd和??SP-Auth的违规。这些违规并不意味着CAS票据生成在密码学上已被破解。相反，……

**结论**

我们呈现了恶意服务提供商威胁模型下中央认证服务（CAS）协议的形式化分析。我们的结果表明，尽管CAS保持了核心票据的保密性和真实性，但当周围环境中的认证上下文被操纵时，有效的协议消息仍可能被滥用。我们识别了涉及密码保密性、服务提供商真实性和会话/资源隔离的违规情况，并表明服务来源混淆可能造成下游的……

**CRediT作者贡献声明**

Liujia Cai：撰写——初稿，形式化分析。Siqi Lu：方法论，形式化分析。Jingyi Wang：形式化分析，概念化。Zhaoxuan Li：方法论，概念化。Qingjun Yuan：调查，概念化。Guangsong Li：指导，经费获取，数据管理。Yongjuan Wang：验证，资源，数据管理。

**利益冲突声明**

作者声明不存在任何已知的竞争性财务利益或个人关系可能影响本文所述工作。

Liujia Cai | Siqi Lu | Jingyi Wang | Zhaoxuan Li | Qingjun Yuan | Guangsong Li | Yongjuan Wang

信息工程大学，河南郑州，中国