\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#3})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

Introduction

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.

Note

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.

Note

Installation instructions are given in the README.md of the repository. The easiest way to discover Squirrel, however, is to run it in the browser via the javascript application here.

In this documention, the languages used in Squirrel are introduced in distinct sections:

  • protocols are modelled as processes from which systems are extracted;

  • 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.

Note

This documentation heavily borrows from the infrastructure of the Coq reference manual which is itself built on top of the Sphinx framework. We thank the Coq and Sphinx developpers for their precious work!

Table of contents

Reference manual

Tutorial

Appendix

Indices and tables