Rule Variant Restrictions for the Tamarin Prover

Felix Linker

Paper 2026/230

Rule Variant Restrictions for the Tamarin Prover

Felix Linker

, ETH Zurich

Abstract

We introduce an optimization to the Tamarin prover that reduces its search space. The optimization applies to protocol models that use equational theories with cancellative operators, for example, when modelling Diffie-Hellman groups or bilinear pairings. We prove the optimization's soundness and evaluate its performance.

Metadata

Available format(s): PDF
Category: Cryptographic protocols
Publication info: Published elsewhere. Logic, Software, and Security - Essays dedicated to David Basin on the occasion of his 65th birthday
Keywords: Formal analysis
Contact author(s): flinker @ inf ethz ch
History: 2026-09-25: last of 2 revisions; 2026-02-11: received; See all versions
Short URL: https://ia.cr/2026/230
License: CC BY

BibTeX

@misc{cryptoeprint:2026/230,
      author = {Felix Linker},
      title = {Rule Variant Restrictions for the Tamarin Prover},
      howpublished = {Cryptology {ePrint} Archive, Paper 2026/230},
      year = {2026},
      url = {https://eprint.iacr.org/2026/230}
}