Source-linked AI summary
Rational Dolev--Yao Attackers: Decidable Incentive-Aware Verification of Security Protocols in Strategic Logic
Ioana Boureanu, R. Ramanujam
TL;DR
Qualitative DY verification asks whether an attack is possible, but does not represent whether an adversary would find it worthwhile. The paper introduces a costed, reward-aware DY attacker in weighted ATL, proves bounded verification decidable, and shows rational security can be strictly finer than DY security in applications including session uncertainty and ThreeBallot.
Problem
Qualitative DY models express attack possibility but not whether a self-interested attacker finds an attack profitable.
Method
The paper models a rational DY intruder with costly actions, rewarded goals, uniform imperfect-information strategies, and weighted-ATL verification over finite concurrent game structures.
Results
Bounded rational DY verification is decidable, and DY-insecure protocols can nevertheless be rationally secure under a computable attack-cost threshold.
Takeaways & Limitations
Rational security is a computable, strictly finer guarantee than DY security, with applications to authenticated payments under session uncertainty and cryptography-free ThreeBallot coercion.
Takeaways & Limitations
The decidability results rely on bounded message depth and benefit from restricting information flow to a decidable A-cast setting.
Abstract
from arXiv · showhide
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.
1 Introduction
The paper replaces the capability-only Dolev–Yao attacker with an incentive-aware attacker whose costs and rewards determine whether an attack is worthwhile. It develops a decidable weighted-ATL framework and uses it to distinguish rational security from qualitative DY security.
- The DY model treats security as the impossibility of reaching an attack state using any knowledge-permitted action.
- A cost-indifferent DY intruder can perform attacks that are possible but economically pointless, unlike a self-interested adversary.
- The framework assigns costs to intruder actions and rewards to security-violating goals within weighted ATL, making no-positive-utility attack a syntactic criterion.
- Decidability is proved for bounded rational DY intruders by reducing verification to weighted-ATL model checking over finite weighted concurrent game structures.
- DY-insecurity and rational security can coexist, separated by a computable threshold; the framework also covers session uncertainty and ThreeBallot coercion.
2 Related Work
The paper positions rational DY verification between qualitative strategic security analysis and resource-bounded reasoning. Its distinction is to retain explicit utilities and deduction costs while addressing imperfect information within a bounded decidable setting.
- Unlike prior rational-verification approaches, the framework targets DY intruders with explicit deduction closure and decidable strategic reasoning.
- Earlier protocol analyses commonly treat attackers as capabilities and therefore express whether coercion is possible, not whether it is profitable.
- ThreeBallot provides a qualitative ATL precedent, whereas this paper adds quantitative costs and benefits to coercion resistance.
- Under perfect recall, ATL model checking with imperfect information is undecidable, while memoryless reasoning is ΔP^2-complete.
- The bounded memoryless formulation remains decidable, with A-cast information-flow restrictions offered as a route beyond the bounded case.
- Capacity-constrained strategic reasoning also uses a budget dimension to keep augmented state spaces finite, but its purpose differs from this paper’s incentive model.
3 The Rational Dolev–Yao Attacker
The rational DY attacker is modeled as an imperfect-information player in a finite cost-annotated concurrent game structure. Uniform strategies constrain choices by observations, while true states determine effects and utility evaluates guaranteed payoff.
- The model records intruder knowledge in a concurrent game structure and annotates intruder transitions with costs.
- Perfect cryptography and bounded message depth make the DY knowledge space finite and symbolic reachability decidable.
- The rational DY structure combines honest and intruder agents, observable knowledge, protocol actions, true-state transitions, action costs, goal rewards, and propositions.
- Observation determines which intruder actions are enabled, but the true state determines their consequences, allowing opaque ciphertexts to behave differently across indistinguishable worlds.
- The intruder’s indistinguishability relation compares equal knowledge states and synchronously lifts this comparison to histories.
- Uniform strategies require identical actions on indistinguishable histories, while memoryless strategies depend only on the current state.
- A rational intruder maximizes guaranteed utility across indistinguishable outcomes and attacks only when some uniform strategy guarantees strictly positive utility.
4 Game-Theoretic Dolev–Yao Deduction
The paper turns DY derivability into a weighted deduction calculus and embeds it in a costed game against honest protocol execution. Boundedness and non-negative costs make cheapest attacks and game values computable.
- The central object is the cheapest derivation of a goal message, rather than merely whether the message is derivable.
- Weighted DY systems assign costs to cryptographic deduction rules and to acquisitions such as interception, injection, blocking, and corruption.
- Compound derivations add the costs of final operations and sub-derivations, while reused derived messages are paid for once.
- The cheapest derivation refines qualitative DY derivability: a message is derivable exactly when its deduction cost is finite.
- For finite knowledge and bounded message depth, all deduction costs are computable in polynomial time in the bounded message-space size.
- Because honest agents follow fixed local-state strategies, they emit protocol-mandated messages rather than strategically withholding premises from the intruder.
- The deduction-game value is the cost of the cheapest DY attack available against the protocol run.
- Finite arenas and non-negative weights permit budget-augmented backward induction, yielding computable game values.
5 Rational Security in Weighted ATL
The paper expresses rational security in weighted ATL as the absence of any strategy that reaches a rewarded violation at cost below its reward. This criterion is equivalent to cheapest-derivation security and strictly refines qualitative DY security.
- The Logic wATL: wATL adds cost-bounded strategic reachability, requiring a uniform coalition strategy to reach φ while accumulated cost satisfies a relation to budget b.The budget is accumulated along the path, and reachability is the only temporal operator.
- Rational Security: Rational security means that no intruder strategy reaches a violation of value R at total cost below R.Equivalently, every attack has non-positive utility.
- Rational Security: DY security implies rational security, but some DY-insecure protocols are rationally secure because every attack is too costly relative to its reward.The framework therefore distinguishes possible attacks from worthwhile attacks.
- Rational Security: The separation is governed by the computable threshold R ≶ nc, where n forged messages each cost c and the violation reward is R.When R < nc, the protocol is DY-insecure yet rationally secure; crossing the cheapest attack cost reverses rational security.
- Rational Security via Deduction Value: Deduction-rational security is equivalent to rational security because positive-utility wATL strategies correspond exactly to weighted DY derivations cheaper than the violation reward.The correspondence schedules proof-DAG rule applications as a uniform intruder strategy and preserves total cost.
- Rational Security via Deduction Value: Weighted deduction costs compose additively, making the cheapest attack an actionable design target: raise its cost above the violation’s value.This replaces the binary goal of eliminating all attacks with pricing the canonical cheapest attack.
6 Decidability and Complexity
For bounded rational DY intruders, finite message depth yields a finite weighted game in which rational security is decidable. Perfect information permits pseudo-polynomial analysis, while unrestricted uniform-strategy reasoning under imperfect information is PSPACE-hard.
- Decidability: Rational security is decidable for finite rational DY CGSs with bounded message depth and integer costs and rewards.The depth bound makes each state’s derivable messages and enabled intruder actions finite.
- Decidability: The decision procedure checks a finite conjunction of cost-bounded reachability formulas, one for each reward value.Each formula asks whether the intruder can reach a value-R violation while spending less than R.
- Decision Procedure: The budget-augmented arena has |S|·(R+1) positions, pairing protocol states with accumulated spending capped by R.Backward-induction attractor computation determines whether the intruder can force the target.
- Complexity: Under perfect information, rational security is decidable in time polynomial in |C| and Rmax, specifically O(|S|2 · |Act| · Rmax) overall.The dependence on numerical weights is pseudo-polynomial.
- Complexity: Under imperfect information with uniform strategies, rational-security verification is PSPACE-hard.Setting all costs to 0 and rewards to 1 reduces qualitative imperfect-information ATL reachability to the weighted problem.
- Complexity: The tractability loss arises from unrestricted uniform-strategy quantification, whereas suitable information-flow restrictions preserve decidability with budget augmentation.The A-cast/DS-knowledge property prevents information sets from growing unboundedly along a strategy.
7 Main Use-case: Rational Attacks under Session Uncertainty
The authenticated-payment use-case shows how a rational intruder attacks across indistinguishable sessions, where deduction, cumulative costs, and imperfect information jointly determine rational security. Because the intruder must hedge across sessions, uncertainty raises the attack cost above the single-session lucky-guess cost.
- 7.1 Single session: a one-shot decision: The protocol authorises payment R when V accepts authenticator {n}k, while the intruder can either relay a genuine response or forge one by corrupting P.Relay and forge costs are priced by the weighted DY derivation system.
- 7.1 Single session: a one-shot decision: A single-session protocol is rationally secure whenever the transaction ceiling R is below the cheapest attack cost, even though it remains DY-insecure.The threshold is R ≤ Δw(K, a⋆) = min(crelay, cforge).
- 7.2 Two indistinguishable sessions: a strategic game: Two sessions are indistinguishable because opaque ciphertexts conceal which session carries the real transaction, forcing the intruder to commit before learning the true state.The same uniform action is available in both worlds, but its effect depends on the hidden session.
- 7.2 Two indistinguishable sessions: a strategic game: Guessing one ciphertext guarantees no reward in the wrong world, yielding negative worst-case utility, whereas intercepting both guarantees success at cost 2 wintercept + winject.The hedge removes uncertainty and is the intruder’s best guaranteed strategy.
- 7.2 Two indistinguishable sessions: a strategic game: Rational security therefore holds iff R ≤ 2 wintercept + winject, strictly higher than the single-session lucky-guess cost wintercept + winject.The gap is attributed to imperfect information and changes the price a designer must use.
- 7.2 Two indistinguishable sessions: a strategic game: The analysis depends on sunk round-1 costs, DY deduction closure, and uniform strategies whose consequences vary across indistinguishable states.These ingredients turn a one-shot cost comparison into a strategic hedging problem.
8 Use-case: Rational Coercion in ThreeBallot
ThreeBallot demonstrates the framework at its cryptography-free extreme: indistinguishability prevents a coercer from verifying compliance, making coercion unprofitable under perfect resistance. When receipt leakage is introduced, the analysis yields a quantitative threshold separating unprofitable from profitable attacks.
- The ThreeBallot Protocol: ThreeBallot uses three scrambled ribbons and a receipt ribbon that individually remains consistent with many possible votes.The receipt supports individual verifiability without proving how the voter voted.
- Setting: A Rational Coercer: A coercer demands a vote for x, offers bribe B, and requests a receipt ribbon as proof, while the voter may resist with a ribbon equally consistent with x.The model assigns costs to approaching, paying, and verifying.
- Modelling and Analysis: Comply and resist histories are indistinguishable, so any uniform coercer strategy receives the same observation and cannot condition payment on genuine compliance.This is the mechanism underlying the coercer’s unprofitable attack.
- Modelling and Analysis: With perfect coercion-resistance, the coercer’s expected utility is negative after paying approach, bribe, and verification costs, so ThreeBallot is rationally secure.The witness formula is unsatisfiable even though a complying state is qualitatively reachable.
- The Threshold: When compliance leaks with probability ϵ, attacks become rational only above the derived leakage threshold, for R > B.Below the threshold no rational coercer attacks; above it, coercion pays off.
- The Threshold: The framework therefore measures protection by the margin between permitted leakage and the coercer’s cost-to-net-benefit ratio, not only by the binary case ϵ = 0.The threshold analysis quantitatively relaxes perfect coercion-resistance.
9 Conclusions & Future Work
The paper concludes that rational DY security is computable and strictly finer than ordinary DY security, while identifying unbounded message depth and probabilistic incentives as future directions.
- Conclusions: Rational DY security is a computable, strictly finer guarantee than DY security.The conclusion states that the rational attacker can be incorporated into strategic logic while preserving computability.
- Future Work: Decidability currently rests on bounded message depth, motivating future work on unbounded message spaces.The conclusion identifies this as a direct scope boundary.
- Future Work: The threshold analysis also motivates stochastic wATL in which a coercer maximises expected payoff.This extends the incentive analysis toward probabilistic settings.