本文提出“理性 Dolev-Yao 攻击者”模型，将传统符号化协议验证中的 Dolev-Yao 入侵者扩展为具有成本与收益考量的理性主体。传统 DY 入侵者在知识允许范围内执行所有可能动作，不论是否有利于达成目标；而真实对手会最大化效用，仅在攻击收益为正时发起攻击。作者将攻击动作赋予成本、将破坏安全目标赋予奖励，并在加权交替时序逻辑（WATL）中定义“理性安全”属性：不存在能使理性入侵者获得严格正效用的违规策略。针对有限成本标注并发博弈结构上的有界理性入侵者，论文证明该验证问题是可判定的，给出了复杂度特征，并证明其严格细化 DY 安全性：某些协议在 DY 模型下不安全但在理性模型下安全，二者之间存在一个可计算的阈值。作者通过两个对比性用例展示框架：一是在会话不确定下的认证支付协议，理性入侵者需在不可区分的会话间策略性行动，其不完美信息会提高设计者需要定价的防御成本；二是无密码学方案的 ThreeBallot 投票协议，通过计算贿赂与收益的比率，指出低于该比率时理性胁迫者不会发动攻击。该工作为协议安全性评估提供了更贴近真实攻击者动机的决策框架，适合安全协议设计者、形式化验证研究者及博弈论与安全交叉领域学者阅读。