Rational Dolev--Yao Attackers: Decidable Incentive-Aware Verification of Security Protocols in Strategic Logic

本文提出“理性 Dolev-Yao 攻击者”模型，将传统符号化协议验证中的 Dolev-Yao 入侵者扩展为具有成本与收益考量的理性主体。传统 DY 入侵者在知识允许范围内执行所有可能动作，不论是否有利于达成目标；而真实对手会最大化效用，仅

历史摘要 · 未重新核验 · arXiv cs.CR