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:

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

# 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 ENS Lyon* - 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

*ACM SIGLOG News*, 2024, vol. 11, https://inria.hal.science/hal-04579038.

*2014 ACM SIGSAC Conference on Computer and Communications Security*, 2014, pp. 609–620, https://hal.inria.fr/hal-01102216.

*Proceedings of the 42nd IEEE Symposium on Security and Privacy (S&P’21)*, 2021, https://hal.inria.fr/hal-03172119.

*CSF 2022 - 35th IEEE Computer Security Foundations Symposium*, 2022, https://hal.archives-ouvertes.fr/hal-03500056.

*Proceedings of the 43nd IEEE Symposium on Security and Privacy (S&P’22)*, 2022, https://hal.inria.fr/hal-03620358.

*2023 38th annual ACM/IEEE symposium on logic in computer science (LICS)*, 2023, pp. 1–13, https://hal.inria.fr/hal-03981949.

*CCS*, 2024, pp. to appear, https://inria.hal.science/hal-04511718.

*CSF*, 2024, pp. 324–339, https://inria.hal.science/hal-04577828.