Rational Dolev--Yao Attackers: Decidable Incentive-Aware Verification of Security Protocols in Strategic Logic
2026-08-24 • Cryptography and Security
Cryptography and SecurityComputer Science and Game Theory
AI summaryⓘ
The authors propose a new way to think about attackers in protocol security by treating them as "rational" agents who weigh the costs and benefits before attacking, unlike traditional models where attackers act on all possible information regardless of cost. They introduce a formal framework called rational Dolev–Yao attacker, and define when a protocol is secure against such cost-benefit attackers. Their approach can decide if an attacker would find it worthwhile to break security, revealing cases where traditional models say a protocol is insecure but rational attackers would not attack. They demonstrate this idea with examples involving payment authentication and an anti-coercion voting scheme.
Dolev–Yao intruderprotocol verificationrational attackersecurity protocolutility maximizationweighted ATL (WATL)bounded intrudergame theoryThreeBallotconcurrent game structure
Authors
Ioana Boureanu, R. Ramanujam
Abstract
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.