# Less Effort, Shorter Proofs: Reinforcement Learning for Security Protocol Analysis in Tamarin

arXiv: https://arxiv.org/abs/2605.23643 · HTML: https://mlsanity.com/paper/2605.23643/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Adversarial robustness and RL in finance, one of 15 directions in Deep reinforcement learning methods.
- Builds on 8 of its 40 references that are in the map.
- First posted on arXiv 22 May 2026.

## Placed in

- Deep reinforcement learning methods / [Adversarial robustness and RL in finance](https://mlsanity.com/deeprl/adversarial-robustness-and-rl-in-finance/)

## Builds on (most cited first, 8 of 8)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Pointer Networks](https://mlsanity.com/paper/1506.03134/) (2015)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving](https://mlsanity.com/paper/2305.16366/) (2023)
- [Monte-Carlo Graph Search for AlphaZero](https://mlsanity.com/paper/2012.11045/) (2020)
- [Verifying Security Protocols using Dynamic Strategies](https://mlsanity.com/paper/1807.00669/) (2018)

## Abstract (arXiv)

Tools like Tamarin and ProVerif have achieved notable success in analyzing and verifying complex real-world protocols such as EMV, 5G, and WPA2, even detecting zero-day exploits. Despite these successes, verifying such protocols remains a time-consuming, challenging task, often requiring significant human effort and expertise. In this paper, we present a reinforcement learning (RL) framework inspired by AlphaZero and AlphaProof that implements a new style of proof search for Tamarin. We have developed a stateless API for Tamarin that acts as a classical RL environment. We guide a Monte Carlo Tree Search (MCTS) by a neural heuristic that learns from completed subproofs. We evaluate our framework on 16 case studies, ranging from classical protocol models to challenging state-of-the-art protocol models from recent publications. Our method finds more proofs automatically than Tamarin's standard search and produces shorter proofs than both the standard and human-engineered heuristics. Our pipeline is applicable out of the box to assist Tamarin users in active research, reducing the human effort required. Moreover, our standardized interface provides a programmatic way for users to interact with Tamarin. Finally, our work demonstrates the promising potential of adapting RL-based methods to the Tamarin domain.