The Squirrel Prover is an interactive prover for protocols. While reasoning inside a first-order logic, it allows to obtain computational guarantees.
A 13 minutes introduction to the base concepts and core ideas of the Squirrel Prover can be found here. Otherwise, a README provides installation instructions and a tutorial allows to start discovering it. The technical details are inside the paper .
- David Baelde, LMF, ENS Paris-Saclay & CNRS, Université Paris-Saclay;
- Stéphanie Delaune, Univ Rennes, CNRS, IRISA;
- Charlie Jacomme, CISPA Helmholtz Center for Information Security;
- Adrien Koutsos, Inria Paris;
- Solène Moreau, Univ Rennes, CNRS, IRISA;
Squirrel is an open source project, licensed under the GNU General Public License v3.0. All source code is available here.
 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-03172119v1.