← 返回 PaperDaily
大模型与智能体
强化学习｜攻击也嫌贵？理性DY攻击者模型让协议安全首次可判定
这可能是今年最值得安全协议研究人员读的一篇理论文：把干了四十年的Dolev-Yao攻击者从“能力模型”升级成“激励模型”，让攻击者学会算账，收益小于成本就不攻击。论文证明理性安全可判定，还给出了可计算的阈值，并在支付协议和ThreeBallot投票两个用例中展示了如何“用钱说话”。建议所有做安全协议验证、密码学形式化、投票方案的朋友都读一下。
龙哥读论文
发布于 2026-08-28 00:20:00
阅读 1
查看原文
原论文信息如下：
在安全协议分析领域，有一个被吐槽了四十年却始终占据C位的“卷王”：Dolev-Yao攻击者（DY攻击者）。几乎所有协议验证工具都把攻击者建模成一个“永动机”——只要密码学不破，它就能无限拦截、分解、重组、注入消息，哪怕为了偷一分钱去腐蚀一千个节点也毫不犹豫。
这合理吗？显然不合理。现实中的黑客是要算账的：攻击要花钱（时间、算力、资源、风险），成功也有收益。当成本大于收益，理性攻击者根本不会动手。可传统形式化验证只问“能不能攻破”，从不问“值不值得攻破”。
本文要介绍的这篇论文，就把DY攻击者从“能力模型”升级成“激励模型”：让每个攻击动作都带价格，每次攻击成功都带收益，然后问一个更现实的问题——不是“攻击者能不能攻破”，而是“攻击者值不值得攻破”。
论文的两位作者是Ioana Boureanu和R. Ramanuj从"能不能攻击"到"值不值得攻击"：理性Dolev-Yao攻击者的诞生 聊安全协议验证，绕不开一个四十年的"老大哥"：Dolev-Yao模型（DY模型）。简单说，DY攻击者被建模成一个完全控制网络的"幽灵"，能拦截、分解、重组、注入所有消息，唯一的限制是密码学完美——没有密钥就解不开密文。四十年里，几乎所有的符号化协议验证工具（如ProVerif、Tamarin）底层都是这个思路：攻击者有多大的能力，就发动多大的攻击，完全不考虑成本。
这种"能力模型"有一个隐藏假设：攻击者是无限资源、无限耐心的。可现实世界哪儿有这种人？真正的黑客是要算账的——买工具要钱，租算力要钱，冒风险要钱，甚至花时间本身也是成本。如果一个攻击要花100块钱，收益只有1块钱，理性的人根本不会动手。DY模型恰恰不关心这个问题，它只回答"能不能攻破"，不回答"值不值得攻破"。
这篇论文干了一件很多人想过、但没人做成的事：把DY攻击者从"能力模型"升级为"激励模型"。论文定义了一个理性Dolev-Yao攻击者 不是问攻击者能不能攻破，而是问攻击者会不会愿意攻破
模型的技术底座是一个带成本标注的并发博弈结构
理性DY并发博弈结构的正式定义，其中Ag是参与方（攻击者加诚实代理），S是状态集合，s₀是初始状态，Act是各参与方的动作集合，tr是状态转移函数，K是各参与方的知识集合，c是攻击者动作的成本函数，r是目标状态上的奖励函数。
在这个结构下，一个理性攻击者的策略就是一条"在不确定中做选择"的规则。攻击者沿着一条运行轨迹行动，赚到的总效用等于目标奖励减去所有动作成本的总和：
图2：攻击者效用函数，u(λ)表示沿着运行λ的总效用，等于目标奖励r(λ)减去每个动作的成本之和。
注意这里的一个关键细节：攻击者是在不完全信息下做决策的。它只能根据自己观察到的知识来选择动作，两个它无法区分的状态，它必须做同样的选择。但动作的效果是由真实状态决定的——这就产生了一个微妙的策略权衡：同样的动作，在一个世界里可能成功拿到奖励，在另一个无法区分的世界里可能什么都没发生。理性攻击者要的是"保证正收益"，它必须在最坏情况下也能盈利才肯动手。
这里有意思的是：不是追求最大收益，而是追求"保证正收益"。
这个设定非常符合现实：黑客不会赌一把，黑客要的是稳赚不赔。这种"最坏情况保证"的思路，为后面的理性安全定义打下了基础。
加权推导系统：给攻击者的每一步行动标上价格 把攻击者变成会算账的理性人，第一步就是要让DY推导本身"有价格"。经典DY推导系统里，攻击者从已知消息集合K出发，通过一系列规则推导出新的消息。比如，知道m₁和m₂，就能拼出消息对〈m₁, m₂〉；知道消息m和密钥k，就能加密得到{m}ₖ；反过来，知道密文{m}ₖ和密钥k的逆k⁻¹，就能解出m。经典的DY推导规则就是这么四条：
图3：Dolev-Yao推导规则的四种基本形式：配对（从m₁、m₂得到〈m₁,m₂〉）、投影（从〈m₁,m₂〉得到m₁或m₂）、加密（从m、k得到{m}ₖ）、解密（从{m}ₖ、k⁻¹得到m）。
但在理性攻击者看来，每一条规则背后都是真金白银的代价。做一次配对运算要花时间，做一次解密可能要跑暴力破解的算力。论文把"每条规则实例"都赋予一个权重，并把成本来源拆成两类：
推导成本
获取成本
这样一来，一条"攻击路径"的总成本就不是拍脑袋算的，而是从推导树结构上递归加出来的：一个推导的代价，等于最后一步操作的代价加上所有子推导的代价之和。用数学的语言说，推导成本的递归定义长这样：
图4：推导成本w(Π)的递归定义。三种情况：如果Π是知识公理（m∈K），成本为0；如果Π是获取操作，成本为w_acq(m)；如果Π以规则r结尾且有子推导Π₁,...,Πₖ，则成本为w_ded(r)加上所有子推导成本之和。这条定义保证：共享的子消息只付一次钱，因为一旦推导出来就进入知识集合，后续使用免费。
基于这一定义，从知识集合K推导消息m的最小推导成本
图5：最小推导成本的定义，Δ_w(K, m) = min{w(Π) : Π推导K⊢m}，取所有推导中成本最小的那个。如果m根本不可推导，该值为无穷大。经典DY可推导性就是这里的"有限成本"特例。
这个最小推导成本还满足类似三角不等式的性质。比如，想通过配对得到〈m₁, m₂〉，成本不会超过配对操作本身的成本加上分别推导m₁和m₂的成本——因为你可以先推导出两个子消息，再执行配对操作。类似地，想加密得到{m}ₖ，成本不会超过加密成本加上推导m的成本再加上推导k的成本。这些不等式用数学语言写出来就是这样：
图6：配对的最小推导成本满足三角不等式：Δ_w(K,〈m₁,m₂〉) ≤ w_pair + Δ_w(K, m₁) + Δ_w(K, m₂)。
图7：加密的最小推导成本同样满足三角不等式：Δ_w(K,{m}ₖ) ≤ w_enc + Δ_w(K, m) + Δ_w(K, k)。
这些不等式看起来简单，却非常重要。它们说明了"先准备子消息再组合"这种策略是最优的基线，攻击者不可能找到比这更便宜的路径——除非某个子消息本来就免费在知识集合里。
更进一步，论文把这种加权推导从"单机游戏"升级成"双人博弈"。因为攻击者要推导的信息，不是凭空冒出来的，而是诚实代理按照协议流程"发射"出来的。于是有了诚实联盟推导博弈
这个博弈有一个漂亮的理论结果：在有界消息深度且权重非负的条件下，推导博弈是"确定的"，博弈值可以计算，而且这个值恰好等于攻击者能保证的最便宜攻击成本。如果这个值是无穷大，那说明根本不存在DY攻击；如果是有限值，那这个值就是"最便宜攻击的出厂价"。这个结果把DY推导理论从定性的"能不能"真正推向了定量的"多少钱"。
理性安全的形式化：当"无利可图"成为安全标准 有了带价格的推导系统，下一步就是把"理性安全"这个概念用逻辑语言严格表达出来。论文选择的载体是加权交替时序逻辑
经典的ATL（交替时序逻辑）是博弈论与逻辑学的经典结合，用来表达"一个联盟是否存在某种策略，使得无论对手怎么行动，系统都能达到某个目标"。比如⟨⟨I⟩⟩◇viol可以读作"攻击者I存在一种策略，最终能达到破坏状态viol"。这种定性表达只关心"能不能"。
wATL则在这个基础上加了一个"预算约束"。新的模态长这样：
图8：wATL的加权策略模态⟨⟨A⟩⟩^{◃▹b}◇φ，读作"联盟A存在一个策略，使得到达φ态时累计成本与预算b之间满足关系◃▹"，其中◃▹可以是小于、小于等于、等于、大于等于或大于。
它的语义也很直白：存在一个联合策略，使得在到达第一个满足φ的状态之前，联盟A累计花费的成本与预算b满足指定关系。形式化的语义定义如下：
图9：wATL的模型满足关系定义，C, s ⊨ ⟨⟨A⟩⟩^{◃▹b}◇φ当且仅当存在联盟A的联合策略，使得每条运行都在到达φ时累计成本满足约束。
其中累计成本是到达第一个φ状态之前的所有动作成本之和：
图10：到达第一个φ状态之前，联盟A累计花费的成本总和。
现在可以把理性安全
图11：理性安全的形式化定义。C, s₀ ⊭ ⟨⟨I⟩⟩^{
翻译成人话就是：任何攻击都是亏本买卖
那理性安全和传统DY安全是什么关系？论文给出了一个清晰的结论：DY安全蕴含理性安全，但反过来不成立
会话不确定下的策略博弈：为什么信息不对称反而更安全 理论落地还得看实例。论文的第一个用例是一个带会话不确定性的认证支付协议。想象这样一个场景：一个客户端向验证者V发起了一个支付请求，金额为R，客户端需要出示一个有效的认证凭证a，V验证通过后就会支付R给持有有效凭证的人。这是一个再经典不过的认证协议，协议流程长这样：
图12：基础认证协议流程。接受有效凭证a即可授权支付价值R给凭证出示者。客户端向验证者发送挑战（或开启会话），验证者生成会话标识转发给客户端，客户端返回认证凭证，验证者检查凭证是否匹配当前会话。
现在把场景搞得复杂一点：假设同时存在两个会话，攻击者看到的是两个无法区分的密文。攻击者不知道这两个密文各自对应哪个会话——这就是"会话不确定性"。攻击者必须决定：拦截哪一个密文？要不要两个都拦截？然后注入什么内容？在这种信息不完全的情况下，攻击者的策略选择就会有微妙的权衡。
图13：两个不可区分的会话示意图。攻击者看到两个无法区分的密文，第一轮必须决定拦截一个或两个，第二轮注入认证凭证，只有匹配真实会话时验证者才会接受。
这里就有意思了。如果攻击者能区分两个会话，它可以只针对那个"真实"的会话下功夫，攻击成本低。但现在它分不清哪个会话是真实的，于是必须做一个"对冲"决策：要么同时攻击两个会话（成本翻倍），要么赌一个（可能赌错，收益为0）。从攻击者角度来说，最坏情况下它得为两个会话都付出成本。而从协议设计者的角度，这正是"信息不对称带来的安全红利"——你越让攻击者看不清，攻击者要付出越高的"策略成本"才能保证收益。
论文的结论是：不完全信息严格提高了协议设计者必须定价的攻击成本
ThreeBallot投票协议：理性胁迫的量化分析 如果说支付协议展示了"攻击成本如何被信息不对称抬高"，那第二个用例——ThreeBallot投票协议——则展示了理性安全分析如何回答一个定量的"阈值"问题。
ThreeBallot是一种很有意思的投票方案，它的设计目标是不需要密码学就能实现选票的不可追踪性。选民拿到三张选票，每张选票可以标记对某个候选人的支持。选民按特定规则填写：比如要投给候选人A，就在第一张选票上标记A，另外两张选票上标记其他候选人；要反对候选人A，就在三张选票上都标记A。投完后，一张选票自己留着（作为收据），另外两张投入票箱。这样，选民的投票意图分散在三张选票里，单看一张选票无法推断选民的投票意图，从而保证了"不可收买"和"不可胁迫"。
但问题来了：一个胁迫者（比如黑恶势力）想强迫选民投某个候选人，它需要验证选民是不是真的照做了。如果选民保留的那张收据选票不够"信息量"，胁迫者就无法判断选民是否遵从，也就不愿意花钱收买。这就构成了一个理性博弈：胁迫者愿意付出一定的贿赂成本B，目的是让选民投给指定候选人，从而获得收益R（比如政治上的好处）。但它只有当能验证选民是否服从时，才愿意付这个钱。
论文分析了胁迫者的"条件攻击策略"：以一定概率ε要求选民提供额外信息（比如三张选票的照片），产生额外的验证成本c_v；选民如果配合，胁迫者支付贿赂B，但选民需要承担被发现的个人风险c_a。把这个场景建模成理性博弈后，胁迫者的期望效用可以写成：
图14：胁迫者的期望效用公式：u_I = εR − (c_a + εB + c_v)。其中ε是胁迫者要求验证的概率，R是胁迫成功后获得的政治收益，c_a是选民配合验证需要承担的风险成本，B是贿赂成本，c_v是验证过程本身的成本。
从效用公式可以看出，胁迫者只有当期望效用为正时才值得动手。不等式u_I > 0经过整理，就得到了一个漂亮的阈值条件：
图15：理性胁迫不发生的条件：R < nc。当胁迫者的总收益R小于总成本nc时，不存在理性胁迫者会发起攻击。
更准确地说，论文给出的阈值条件是ε > (c_a + c_v) / (R − B)。这意味着：胁迫者要求验证的概率必须大于某个临界值，否则整个胁迫策略无利可图。反过来，如果协议设计者能把验证成本c_v抬高到一定程度（或者说，把收据的"信息量"压到足够低），就可以让任何理性的胁迫者都自动放弃攻击。
这个结果对"抗胁迫性"（coercion-resistance）的量化分析迈出了一大步。传统的抗胁迫性分析只回答"胁迫是否可能"，这个框架直接回答"胁迫是否划算"。从"可能"到"划算"，这就是理性安全分析的核心增量。
可判定性与复杂度：理性安全验证的工程可行性 理论再好，如果不可判定，那对工程界来说就是空中楼阁。论文最"硬"的贡献之一就是证明了这个理性安全验证问题在有界条件下是可判定的
具体来说，可判定性通过两条路径共同完成。第一条路径是最小推导成本的计算：前面提到的加权推导系统，本质上是一个超图（hypergraph）上的最短路径问题。超图上的节点是消息，每条推导规则是一个从前提指向结论的超边，权重是规则成本。因为消息深度有界，所以节点集合有限，可以用Dijkstra式的饱和算法在多项式时间内算出所有消息的最小推导成本。这个结果的意义在于：一次计算就能给所有可能的目标消息同时定价
第二条路径是wATL模型检测：整个理性安全问题被化归为在有限加权并发博弈结构上的wATL模型检测。模型检测本身是自动化的，输入协议描述和安全属性，输出"安全"或"不安全"以及对应的攻击成本。因为博弈结构是有限的，模型检测可以通过反向归纳（backward induction）在预算增广的状态空间上完成。非负权重的设定保证了花费的单调性，使得预算维度是无环的，吸引子可以在多项式轮次内收敛。
在复杂度方面，论文给出了两层结果。第一层，最小推导成本的计算是多项式时间的——这是加权DY推导系统本身的性质。第二层，wATL模型检测在"无记忆策略"（memoryless strategy）假设下是Δ₂ᴾ完备的，这与不完全信息下ATL模型检测的已知复杂度结果一致。所谓"无记忆策略"是指攻击者的决策只依赖于当前状态、不依赖整个历史。这个假设不是限制，反而是一种工程上的务实选择：完全回忆（perfect recall）下ATL模型检测已经知道是不可判定的，所以"有界记忆+无记忆策略"恰恰是站在可判定性这一边的正确姿势。
但这里需要诚实指出一个工程上的边界：论文的可判定性证明是构造性的，但不是"拿来即用"的实现。要把这套理论真正变成像ProVerif或Tamarin那样好用的工具，还需要解决状态空间爆炸、权重函数标定、策略表示等工程问题。这为后续的研究指了一个明确的方向，但离"一键验证"还有距离。
龙迷三问 这篇论文到底在解决什么问题？ 本文提出理性Dolev-Yao攻击者，将攻击动作标上成本、攻击目标标上收益，用加权ATL形式化“无正效用攻击”的理性安全，证明可判定且严格细化DY安全，在支付协议与ThreeBallot投票中给出可计算的安全阈值。这篇工作最值得看的点是什么？ 论文通过两个用例（会话不确定下的认证支付和ThreeBallot投票协议）展示了框架的有效性，证明了DY不安全但理性安全的协议存在，并给出了可计算的阈值。这篇工作的边界或风险在哪里？ 优点：(1) 首次将Dolev-Yao攻击者从能力模型提升为激励模型，填补了理性安全与符号验证之间的空白；(2) 证明了理性安全的可判定性，并给出了复杂度上界；(3) 通过两个对比鲜明的用例展示了框架的普适性。缺点：(1) 可判定性依赖于有界消息深度和有限状态假设，对无界场景不适用；(2) 完美信息下的复杂度为伪多项式，实际应用中可能面临性能瓶颈；(3) 框架目前仅支持可达性逻辑，不支持更复杂的时序属性。如果你还有哪些想要了解的，欢迎在评论区留言或者讨论~
龙哥点评 论文创新性分数： ★★★★☆
将Dolev-Yao攻击者从能力模型提升为激励模型，在加权ATL逻辑中定义理性安全，通过归约到有限加权并发博弈结构上的wATL模型检验实现可判定性。实验合理度： ★★★☆☆
现有材料未完整覆盖数据划分、基线公平性和统计显著性，因此按中性评价处理。学术研究价值： ★★★★☆
将Dolev-Yao攻击者从能力模型提升为激励模型，在加权ATL逻辑中定义理性安全，通过归约到有限加权并发博弈结构上的wATL模型检验实现可判定性；更关键的是问题定义是否可复用到同类任务。稳定性： ★★★☆☆
现有材料未提供充分的极端条件、重复运行或扰动测试，稳定性暂按中性评价。适应性以及泛化能力： ★★★☆☆
现有材料未完整展示跨数据集、跨场景或分布外实验，泛化能力仍需进一步验证。硬件需求及成本： ★★★☆☆
完美信息下时间复杂度为O(|S|²·|Act|·R_max)，伪多项式复杂度复现难度： ★★★☆☆
现有材料未确认完整代码、配置、数据处理脚本和权重是否齐备，复现难度暂按中性评价。产品化成熟度： ★★★☆☆
论文验证以研究实验为主，真实部署中的时延、成本、维护和异常场景仍需补充验证。可能的问题： (1) 可判定性依赖于有界消息深度和有限状态假设，对无界场景不适用；(2) 完美信息下的复杂度为伪多项式，实际应用中可能面临性能瓶颈；
*本文仅代表个人理解及观点，不构成任何论文审核或者项目落地推荐意见，具体以相关组织评审结果为准。欢迎就论文内容交流探讨，理性发言哦～ 想了解更多原文细节的小伙伴，可以点击 "阅读原文"， 查看更多原论文细节哦！
