Paper 2026/230 Original: eprint.iacr.org/2026/230 ↗
Rule Variant Restrictions for the Tamarin Prover
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
- Preprint.
- History
- 2026-09-25: last updated
- 2026-02-11: published
- Short URL
- https://ia.cr/2026/230
- License
- https://creativecommons.org/licenses/by/4.0/
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}
}