From security protocols to pushdown automata
type: Dataset
contact point: Organization
  fn: CCSD
keyword: infoeu-reposemanticsreport
keyword: infoinfo-crcomputer-science-cscryptography-and-security-cscr
keyword: reports
landing page: https://inria.hal.science/hal-00817230
description: Formal methods have been very successful in analyzing security protocols for reachability properties such as secrecy or authentication. In contrast, there are very few results for equivalence-based properties, crucial for studying e.g. privacy-like properties such as anonymity or vote secrecy. We study the problem of checking equivalence of security protocols for an unbounded number of sessions. Since replication leads very quickly to undecidability (even in the simple case of secrecy), we focus on a limited fragment of protocols (standard primitives but pairs, one variable per protocol's rules) for which the secrecy preservation problem is known to be decidable. Surprisingly, this fragment turns out to be undecidable for equivalence. Then, restricting our attention to deterministic protocols, we propose the first decidability result for checking equivalence of protocols for an unbounded number of sessions. This result is obtained through a characterization of equivalence of protocols in terms of equality of languages of (generalized, real-time) deterministic pushdown automata.
identifier: Report N°: RR-8290
issued: 2026-05-11T08:22:48.767027
language: en
modified: 2026-05-11T08:22:48.767031

From security protocols to pushdown automata
type: Distribution
access URL: https://inria.hal.science/hal-00817230
format: HTML
issued: 2026-05-11T08:22:48.768586
modified: 2026-05-11T08:22:48.761272

test_moissonnage_selune
type: Agent