Decidability of Parameterised Dolev-Yao Secrecy

• URL: http://arxiv.org/abs/2608.02838v1
• Date: Mon, 03 Aug 2026 19:51:46 GMT
• Title: Decidability of Parameterised Dolev-Yao Secrecy
• Abstract summary: We study the verification of parameterised secrecy for cryptographic protocols in the Dolev-Yao model.<n>We obtain a cut-off theorem: secrecy violations in systems with arbitrarily many sessions are always witnessed in systems of bounded size.
• Score: 3.9737423502459106
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: 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.

Related papers

• AI Slop and Hallucinations in Vulnerability Assessment: A Survey on Reasoning Failures and Trustworthy Mitigation [48.55515767840701]
  "AI slop" is artifacts, hallucinated vulnerabilities, plausible but incorrect patches, and semantically repackaged bug reports.<n>This paper surveys the empirical evidence, identifies a unifying mechanism, and traces a path toward trustworthy triage.
  arXiv  Detail & Related papers  (2026-08-26T11:48:38Z)
• Logit-Boundary Geometric Belief Interfaces and Sparse Sheaf-Enclave Protocols: A Self-Contained Substrate for Secure Network Electronic Health Record (EHR) Interoperability [2.894286977279531]
  This paper details a mathematical and engineering architecture for that interface.<n>The organizing idea is the logit boundary: a discovery model may propose pre-threshold scores over a local categorical decision, but a deterministic judgment substrate decides whether the proposal is admissible.<n>The resulting Geometric Belief Interface (GBI) combines finite boundary semantics, local Dirichlet evidence, cellular-sheaf and mapping-cone diagnostics, advisory audit charts, and a Decentralized Cryptographic Sheaf-Enclave protocol sketch for fail-closed deployment.
  arXiv  Detail & Related papers  (2026-08-10T23:10:53Z)
• Constraint-Driven Synthesis of Hyper Petri Nets [46.9047309711542]
  This paper addresses the modeling and synthesis of constrained robotic system behaviors using Petri nets (PNs)<n>It investigates how to construct models in which all observable system states satisfy given logical constraints while remaining consistent with executable transition semantics.<n>The proposed method introduces an explicit execution semantics over observable states, induced by admissible (atomic) firing sequences.
  arXiv  Detail & Related papers  (2026-07-24T07:57:19Z)
• LeanDY: Type-Based and Trace-Based Symbolic Protocol Verification in Lean [9.293322518056357]
  We present an approach that combines type-based reasoning with trace-based reasoning, enabling modular verification of stateful and unbounded protocols.<n>We implement this framework as the LeanDY library for the Lean proof assistant, building on and extending the design of DY*.<n>We formalize SegWit-style blockchain primitives in LeanDY and demonstrate its expressiveness by carrying out an in-depth formalization of payment channels.
  arXiv  Detail & Related papers  (2026-07-03T15:12:30Z)
• Compiling Activation Steering into Weights via Null-Space Constraints for Stealthy Backdoors [48.881343993730844]
  Safety-aligned large language models (LLMs) are increasingly deployed in real-world pipelines.<n> adversaries can distribute backdoored checkpoints that behave normally under standard evaluation but jailbreak when a hidden trigger is present.<n>Recent post-hoc weight-editing methods offer an efficient approach to injecting such backdoors.
  arXiv  Detail & Related papers  (2026-04-14T06:48:33Z)
• AlignSAE: Concept-Aligned Sparse Autoencoders [47.18866175760984]
  We introduce AlignSAE, a method that aligns SAE features with a defined ontology through a "pre-train, then post-train" curriculum.<n>After an initial unsupervised training phase, we apply supervised post-training to bind specific concepts to dedicated latent slots.<n>This separation creates an interpretable interface where specific relations can be inspected and controlled without interference from unrelated features.
  arXiv  Detail & Related papers  (2025-12-01T18:58:22Z)
• Formal Verification of Physical Layer Security Protocols for Next-Generation Communication Networks (extended version) [1.5997757408973357]
  We re-model the Needham-Schroeder protocol using an Isabelle formalism that generates sound animation.<n>Our findings reveal an uncommon but expected outcome: authenticity is preserved across all examined scenarios.<n>We have proposed a PLS-based Diffie-Hellman protocol that integrates watermarking and jamming.
  arXiv  Detail & Related papers  (2025-08-26T20:59:16Z)
• Invariant-Based Cryptography [0.0]
  Scheme encodes a secret integer through a four-point algebraic identity preserved under controlled parameterization.<n>We develop the full analytic and modular framework, prove exact identities, define index-recovery procedures, and analyze security assumptions.
  arXiv  Detail & Related papers  (2025-05-08T21:18:59Z)
• Is Vertical Logistic Regression Privacy-Preserving? A Comprehensive Privacy Analysis and Beyond [57.10914865054868]
  We consider vertical logistic regression (VLR) trained with mini-batch descent gradient. We provide a comprehensive and rigorous privacy analysis of VLR in a class of open-source Federated Learning frameworks.
  arXiv  Detail & Related papers  (2022-07-19T05:47:30Z)
• Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
  We construct the first fully homomorphic encryption scheme with certified deletion. Our main technical ingredient is an interactive protocol by which a quantum prover can convince a classical verifier that a sample from the Learning with Errors distribution in the form of a quantum state was deleted.
  arXiv  Detail & Related papers  (2022-03-03T10:07:32Z)
• Sharing classical secrets with continuous-variable entanglement: Composable security and network coding advantage [0.913755431537592]
  We show that multi-partite entangled resources achieve a genuine advantage over point-to-point protocols for quantum communication. This is the first concrete compelling examples of multi-partite entangled resources achieving a genuine advantage over point-to-point protocols for quantum communication.
  arXiv  Detail & Related papers  (2021-04-21T17:37:28Z)
• SMT-based Safety Verification of Parameterised Multi-Agent Systems [78.04236259129524]
  We study the verification of parameterised multi-agent systems (MASs) In particular, we study whether unwanted states, characterised as a given state formula, are reachable in a given MAS.
  arXiv  Detail & Related papers  (2020-08-11T15:24:05Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.