The Squirrel Prover is a proof assistant dedicated to cryptographic protocols. It relies on a higher-order logic following the computationnally complete symbolic attacker approach. It thus provides guarantees in the computational model.

Getting started

A 13 minutes introduction to the basic concepts and core ideas of the Squirrel Prover can be found here.

A README provides installation instructions.

You can also try our online version here.

Documentation

The documentation can be found here.

Tutorial

You may get started with this tutorial, or commented examples available in our browser-based prover. More complete tutorials have been prepared on the occasion of several summer schols; see the events page.

A high-level introduction to the theory behind Squirrel was published in the ACM Siglog newsletter [5]. The formal technical details are inside the research papers:

the computationnally complete symbolic attacker was proposed in [12];
the tool Squirrel was introduced in [11] as a proof assistant for a meta-logic on top of the logic of [12];
the meta-logic was later adapted to support protocols with mutable state [9];
the meta-logic approach has been abandonned in favor of a self-contained higher-order logic [8];
support for user-defined cryptographic assumptions was added in [7];
the framework was adapted to post-quantum cryptography in [1].

Team

David Baelde, ENS Rennes, Univ Rennes, CNRS, IRISA
Stéphanie Delaune, Univ Rennes, CNRS, IRISA
Caroline Fontaine, Université Paris-Saclay, CNRS, LMF
Charlie Jacomme, Université de Lorraine, LORIA, Inria Nancy Grand-Est
Adrien Koutsos, Inria Paris
Joseph Lallemand, Univ Rennes, CNRS, IRISA
Clément Herouard, Univ Rennes, CNRS, IRISA
Justine Sauvage, Inria Paris

Former members:

Tito Nguyen, formerly IRISA, now at LIS / Aix-Mariseille University
Solène Moreau, formerly IRISA, now at AdaCore
Thomas Rubiano, formerly Univ Rennes, CNRS, IRISA

Source code

Squirrel is an open source project, licensed under the MIT License. All source code is available here.

Publications

[1]

D. Baelde, A. Dallon, S. Delaune, C. Jacomme, and A. Koutsos, “Robust logical foundations for mechanizing post-quantum cryptography in squirrel,” in To appear in CCS’26, 2026, https://inria.hal.science/hal-05595035.

[2]

D. Baelde, A. Koutsos, and J. Sauvage, “Leveraging cryptographic simulator synthesis for formally verifying the FOO e-voting protocol,” in Usenix 2026 - 35th Usenix security symposium, 2026, https://inria.hal.science/hal-05453231.

[3]

C. Fontaine, A. Koutsos, G. Scerri, and T. Vignon, “Interactive proofs in higher-order logic with errors and application to concrete cryptography,” in CSF, 2026, pp. 529–543, https://inria.hal.science/hal-05630926.

[4]

C. Hérouard, C. Jacomme, A. Koutsos, and J. Lallemand, “Secrecy in squirrel and the post-compromise security of a ratchet,” in To appear in CCS’26, 2026, https://hal.science/hal-05740706.

[5]

D. Baelde, S. Delaune, C. Jacomme, A. Koutsos, and J. Lallemand, “The Squirrel Prover and its Logic,” in ACM SIGLOG News, 2024, vol. 11, https://inria.hal.science/hal-04579038.

[6]

D. Baelde, C. Fontaine, A. Koutsos, G. Scerri, and T. Vignon, “A probabilistic logic for concrete security,” in CSF, 2024, pp. 324–339, https://inria.hal.science/hal-04577828.

[7]

D. Baelde, A. Koutsos, and J. Sauvage, “Foundations for cryptographic reductions in CCSA logics,” in CCS, 2024, pp. 2814–2828, https://inria.hal.science/hal-04511718.

[8]

D. Baelde, A. Koutsos, and J. Lallemand, “A higher-order indistinguishability logic for cryptographic reasoning,” in 2023 38th annual ACM/IEEE symposium on logic in computer science (LICS), 2023, pp. 1–13, https://hal.inria.fr/hal-03981949.

[9]

D. Baelde, S. Delaune, A. Koutsos, and S. Moreau, “Cracking the Stateful Nut,” in CSF 2022 - 35th IEEE Computer Security Foundations Symposium, 2022, https://hal.archives-ouvertes.fr/hal-03500056.

[10]

C. Cremers, C. Fontaine, and C. Jacomme, “A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols,” in Proceedings of the 43nd IEEE Symposium on Security and Privacy (S&P’22), 2022, https://hal.inria.fr/hal-03620358.

[11]

D. Baelde, S. Delaune, A. Koutsos, C. Jacomme, and S. Moreau, “An Interactive Prover for Protocol Verification in the Computational Model,” in Proceedings of the 42nd IEEE Symposium on Security and Privacy (S&P’21), 2021, https://hal.inria.fr/hal-03172119.

[12]

G. Bana and H. Comon-Lundh, “A Computationally Complete Symbolic Attacker for Equivalence Properties,” in 2014 ACM SIGSAC Conference on Computer and Communications Security, 2014, pp. 609–620, https://hal.inria.fr/hal-01102216.