A rational Dolev--Yao attacker is introduced, a DY intruder whose actions carry costs and whose security-violating goals carry rewards, and a protocol is called rationally secure when no intruder strategy achieves a violation with strictly positive utility, expressed in a weighted fragment of ATL (WATL).
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.
We study the verification of parameterised secrecy for cryptographic protocols in the Dolev-Yao model, where the number of protocol sessions is unbounded and treated as a parameter. This differs fundamentally from classical Dolev-Yao secrecy, which asks whether a protocol leaks a secret irrespective of the number of executions; our question is whether secrecy holds uniformly across all system sizes, where such a size is a parameter. This parameterised perspective captures how attacks scale with the number of participants and provides a formal basis for the empirical effectiveness of small-instance analysis. Secrecy (parameterised or not) is undecidable in general, even under bounded freshness or bounded message size. We identify two structural restrictions that make parameterised secrecy decidable: (i) global bounded freshness per role, and (ii) a Dolev-Yao intruder restricted to well-typed substitutions. Under these assumptions, protocol executions admit a finite representation up to a collapsing map on agents and terms. Our main result is that parameterised secrecy is decidable in this setting. We obtain a cut-off theorem: secrecy violations in systems with arbitrarily many sessions are always witnessed in systems of bounded size. The cut-off is self-contained; more strongly, the induced transition system forms a well-structured transition system (WSTS) under a bound-based ordering, so secrecy also reduces to a coverability problem in WSTS. This provides a structural explanation for the existence of finite witnesses in symbolic protocol analysis and connects Dolev-Yao verification with parameterised verification techniques.
Ioana Boureanu, R. Ramanujam, Srinibas Swain· 0 citations
A deployable mechanism combining history-dependent challenges, reputation-weighted slashing, and stake vesting is proposed, which restores infinite-horizon subgame-perfect incentive compatibility against stationary mixed-strategy deviations above an explicit discount-factor threshold without per-query cryptographic verification.
In the context of probabilistic programs, an oblivious adversary resolves nondeterminism without seeing the outcomes of random draws. Obliviousness is a common assumption in online algorithms and distributed protocols, but the complex interaction between random draws and adversarial choices makes it challenging to reason about correctness. While there has been significant progress toward reasoning about programs that combine randomization with nondeterminism, most of the work has focused on the adaptive model, whose omniscient view of program state is too powerful to establish correctness for certain classes of programs. We introduce Oblivious Probabilistic Outcome Logic (opOL), a new logic for reasoning about probabilistic programs with nondeterminism controlled by an oblivious adversary. Building on Outcome Logic and Probabilistic Separation Logic, opOL models adversarial choice as a resource and uses probabilistic independence to ensure that random outcomes are hidden from the adversary. The opOL proof system provides expressive and compositional rules for case analysis on both random and nondeterministic outcomes, and for proving almost-sure termination. Expressivity is tested through several case studies, including a paging algorithm and a leader election protocol. The opOL metatheory and case studies are mechanized in Lean 4.
Hanxi Chen, Noam Zilberstein, Andrew C. Myers et al.· 0 citations
We propose a variant of classic information flow analysis that permits transmission of secrets over a public network, provided that secrets are suitably encrypted. In the style of Dolev and Yao, the intruder controls the network, observing all messages sent, but can only decrypt messages for which they know the decryption key, i.e., those keys which correspond to the security level of the intruder. In contrast to similar previous works we allow the intruder to send arbitrary bit strings as input to the program without any assumption that these inputs are in some sense well-typed. This means that cryptographic messages can enter program variables that were not meant to hold cryptographic messages and become part of computations and conditions. Despite this strong intruder model, we show that a program that satisfies our information-flow analysis also enjoys Dolev-Yao noninterference, a variant of standard noninterference where the intruder cannot break cryptography. The underlying model, which combines operating on actual bit strings with a symbolic intruder model, and the entire result are formalized and proved in Isabelle/HOL.
S. Lund, Sebastian Mödersheim· IEEE Computer Security Found...· 0 citations
An automated formal verification study of the Secure Aggregation protocol using ProVerif is presented, demonstrating how automated formal verification can support trustworthy and verifiable federated learning software systems.
Yuping Yan, Zi-Cen Zhao, Ming Fei et al.· International Conference on...· 0 citations
Service uptime monitoring infrastructure is a high-value target for data-integrity attacks: a single compromised or dishonest monitoring provider can fabricate availability records, retroactively suppress outage evidence, or silently alter historical data, and clients today have no cryptographic means of detecting such manipulation. This study develops a threat model for monitoring-data integrity attacks—covering provider-side tampering, evidence suppression, Sybil-identity flooding, and submission replay—and presents a verification architecture engineered to resist each threat in that model. Independent validator nodes sign availability observations with Ed25519 keys; a quorum-based aggregation rule tolerates up to f < Q/2 Byzantine validators, SHA-256 content-hash commitments bind off-chain evidence to an immutable on-ledger record that any third party can independently re-derive and check without trusting the aggregator; and stake-bonded registration imposes a quantifiable capital cost on Sybil identities. We formalize the adversary model, prove signature unforgeability under the Elliptic Curve Discrete Logarithm assumption, derive the capital cost of quorum capture, and bound the residual attack surface—selective evidence inclusion and round-stalling—that persists even under a semi-honest aggregator. A seven-day, five-validator, three-region deployment achieves 99.7% quorum agreement, sub-6-second worst-case attestation latency, and zero false positives or negatives across 200 independently re-verified historical rounds, confirming that the architecture removes the central point of trust that lets a single compromised provider corrupt monitoring evidence undetected.
Unknown authors· International Journal of Adv...· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
