BMC4TimeSec: Verification Of Timed Security Protocols

Agnieszka M. Zbrzezny

cs.CRFeb 19, 2026

BMC4TimeSec: Verification Of Timed Security Protocols

Authors: Agnieszka M. Zbrzezny

Organizations: Department of Computer Science, Faculty of Design, SWPS University, Warsaw, Poland

Abstract

We present BMC4TimeSec, an end-to-end tool for verifying Timed Security Protocols (TSP) based on SMT-based bounded model checking and multi-agent modelling in the form of Timed Interpreted Systems (TIS) and Timed Interleaved Interpreted Systems (TIIS). In BMC4TimeSec, TSP executions implement the TIS/TIIS environment (join actions, interleaving, delays, lifetimes), and knowledge automata implement the agents (evolution of participant knowledge, including the intruder). The code is publicly available on GitHub, as is a video demonstration.

Figures & tables

Explore similar work

Less Effort, Shorter Proofs: Reinforcement Learning for Security Protocol Analysis in Tamarin
May 22, 2026Matthias Cosler, Cas Cremers, Bernd Finkbeiner +2Reinforcement Learning Automated Theorem Proving
CISPA Helmholtz Center for Information Security, Saarbrücken, Germany · Technical University of Munich, Munich, Germany
Measuring Security Without Fooling Ourselves: Why Benchmarking Agents Is Hard
May 21, 2026Sahar Abdelnabi, Chris Hicks, Konrad Rieck +1AI Agent Evaluation AI Agent Security
ELLIS Institute Tübingen & MPI-IS & Tübingen AI Center, Germany · The Alan Turing Institute, London, UK · BIFOLD & Technische Universität Berlin, Germany +1
The Prover Is the Judge: Verified Security Software from AI Coding Agents in Ada/SPARK
Jul 15, 2026Tobias PhilippAI Coding Agents Code Generation
secunet Security Networks AG, Essen, Germany

May 22, 2026J/K move · Enter open · S save

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

Matthias Cosler, Cas Cremers, Bernd Finkbeiner, Mohamed Ghanem+1

CISPA Helmholtz Center for Information Security, Saarbrücken, Germany · Technical University of Munich, Munich, Germany

Reinforcement Learning Automated Theorem Proving Cybersecurity Formal Verification

Open paper AskPDF 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.

Abstract

Explore similar work

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

Measuring Security Without Fooling Ourselves: Why Benchmarking Agents Is Hard

The Prover Is the Judge: Verified Security Software from AI Coding Agents in Ada/SPARK