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.

A basic tutorial and some commented examples allow to start discovering it. A more complete tutorial has been prepared on the occasion of the Cyber in Nancy summer school; see below.

The technical details are inside the research papers:

the computationnally complete symbolic attacker was proposed in [1];
the tool Squirrel was introduced in [2] as a proof assistant for a meta-logic on top of the logic of [1];
the meta-logic was later adapted to support protocols with mutable state [3];
a post-quantum sound variant of the logic, meta-logic and tool have been given in [4];
recently, the meta-logic approach has been abandonned in favor of a self-contained higher-order logic [5].

Event: Cyber in Nancy

Slides are available here.

The school featured a Squirrel tutorial, consisting of a series of exercises of increasing difficulty, covering:

the basic logical constructs and tactics manipulating them,
several cryptographic assumptions,
accessibility properties (authentication, injective authentication),
equivalence properties (unlinkability),
stateful protocol, and
protocol composition.

As support material to go through the exercises, we provide syntax documentation here, and tactics documentation there.

The files of the tutorial are now part of the official Squirrel distribution, under the examples/tutorial/ directory. They are also accessible directly below:

Event: MOVEP

Slides are available here.

Examples used for the presentation are here.

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, Inria Paris
Adrien Koutsos, Inria Paris
Joseph Lallemand, Univ Rennes, CNRS, IRISA
Thomas Rubiano, Univ Rennes, CNRS, IRISA
Clément Herouard, Univ Rennes, CNRS, IRISA
Justine Sauvage, Inria Paris

Former members:

Tito Nguyen, formerly IRISA, now at ENS Lyon
Solène Moreau, formerly IRISA, now at AdaCore

Source code

Squirrel is an open source project, licensed under the GNU General Public License v3.0. All source code is available here.

Publications

[1]

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.

[2]

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.

[3]

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.

[4]

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.

[5]

D. Baelde, A. Koutsos, and J. Lallemand, “A Higher-Order Indistinguishability Logic for Cryptographic Reasoning,” 2023.