The Squirrel Prover is a proof assistant for cryptographic protocols. It is based on a higher-order version of the Bana-Comon logic, and provides guarantees in the computational model. You may find more information on the Squirrel homepage or get the source code of the tool from our repository.
The Squirrel project started in 2020, and the tool is still under active development. This documentation is even more recent, and under construction. Please bear with us and do not hesitate to contact us to report problems or ask for clarifications.
You are reading the user’s documentation. This documentation is not meant as a first introduction to Squirrel; a linear read for people unfamiliar with all the high level concepts will be difficult. To discover Squirrel, several materials are available:
For a first high-level introduction to the core concepts, we recommend to start with the tutorial.
Going through the reference manual after or in parallel to this tutorial is then possible.
In the squirrel repository, an example repository contains some documented examples.
A long tutorial with exercises and a step by step approach is also available there.
In this documention, the languages used in Squirrel are introduced in distinct sections:
properties of these systems are expressed using the local and global formulas of our logic;
finally, proving these properties is done using a tactic language.
A Squirrel file consists of a list of directives that impact the prover state:
declarations, which introduce new function symbols, cryptographic assumptions, processes, systems, and lemmas/theorems;
commands, which are used to enter or exit the proof mode, query the current state of the prover (e.g. find lemmas about a given function symbol) or tweak the tool’s behaviour (e.g. control timeouts);
finally, when in proof mode, tactics are used to reduce the first subgoal to new subgoals.
For a more theoretical perspective on Squirrel, you may read some of the associated publications: [BDJ+21] for the original paper, [BDKM22] for the extension to stateful protocols, [CFJ22] for the extension to post-quantum attackers and [BKL23] for the up to date presentation of the logic.
Table of contents¶
- Documenting Squirrel with Sphinx
- TODO list generation
- Squirrel objects
- Squirrel directives
- Squirrel roles
- Common mistakes
- Tips and tricks