AI 中文总结
该研究提出理性Dolev--Yao攻击者模型，用加权交替时间时序逻辑验证协议理性安全性，证明其可判定性与复杂性，并通过认证支付和ThreeBallot案例展示其应用。
AI 中文摘要
符号协议验证将网络攻击者建模为Dolev--Yao（DY）入侵者，该入侵者会执行其知识允许的所有操作，无论是否有目的；而现实中的攻击者则会最大化效用，仅在收益为正时发动攻击。我们引入理性Dolev--Yao攻击者，即一种带有行动成本、安全违规目标带有奖励的DY入侵者，并将协议定义为理性安全的，当没有入侵者策略能在加权交替时间时序逻辑（WATL）的严格正效用下实现违规。我们证明，在有限成本标注并发游戏结构上，对于有界理性DY入侵者，该问题可判定，刻画了其复杂性，并表明其严格优于DY安全：一些协议是DY不安全的，但却是理性安全的，二者由可计算阈值分隔。我们在两个对比用例中说明该框架：会话不确定性下的认证支付，其中理性入侵者必须在无法区分的会话间制定策略，其不完备信息严格提高了设计者必须应对的攻击成本；以及ThreeBallot，一种无密码学的方案，我们确定了贿赂与收益的比率，低于该比率则无理性胁迫者发动攻击。
英文摘要
Symbolic protocol verification models the network attacker as a Dolev--Yao (DY) intruder, which does everything its knowledge permits, whether or not it serves any purpose; real adversaries instead maximise utility, attacking only when the payoff is positive. We introduce a rational Dolev--Yao attacker, a DY intruder whose actions carry costs and whose security-violating goals carry rewards, and call a protocol rationally secure when no intruder strategy achieves a violation with strictly positive utility, expressed in a weighted fragment of ATL (WATL). We prove this decidable for a bounded rational DY intruder over a finite cost-annotated concurrent game structure, characterise its complexity, and show it strictly refines DY security: some protocols are DY-insecure yet rationally secure, separated by a computable threshold. We illustrate the framework on two contrasting use-cases: an authenticated payment under session uncertainty, where a rational intruder must strategise across indistinguishable sessions and its imperfect information strictly raises the attack cost a designer must price against; and ThreeBallot, a cryptography-free scheme where we pinpoint the bribe-to-benefit ratio below which no rational coercer attacks.
