| title | Squirrel Prover |
|---|---|
| pagetitle | Index |
| mainpagetitle | |
| navigation | false |
| next_page | |
| next_page_url | |
| prev_page | |
| prev_page_url | |
| bibliography | biblio.bib |
| csl | ieee.csl |
| link-citations | true |
| nocite | @* |
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.
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.
The documentation can be found here.
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 [@BDJKL24]. The formal technical details are inside the research papers:
- the computationnally complete symbolic attacker was proposed in [@BC14];
- the tool Squirrel was introduced in [@BDKJM-sp21] as a proof assistant for a meta-logic on top of the logic of [@BC14];
- the meta-logic was later adapted to support protocols with mutable state [@BDKM-csf22];
- a post-quantum sound variant of the logic, meta-logic and tool have been given in [@CFJ-sp22];
- recently, the meta-logic approach has been abandonned in favor of a self-contained higher-order logic [@BKL23].
- 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
Squirrel is an open source project, licensed under the MIT License. All source code is available here.