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

This tutorial and some commented examples allow to start discovering Squirrel. A more complete tutorial has been prepared on the occasion of the Cyber in Nancy summer school; see the events page.

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

Team

Former members:

Source code

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

Publications

[1]
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.
[2]
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.
[3]
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.
[4]
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.
[5]
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.
[6]
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.
[7]
D. Baelde, A. Koutsos, and J. Sauvage, “Foundations for cryptographic reductions in CCSA logics,” in CCS, 2024, pp. to appear, https://inria.hal.science/hal-04511718.
[8]
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.