The Squirrel Prover is an interactive prover for protocols. While reasoning inside a first-order logic, it allows to obtain computational guarantees.

Getting started

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 [1].

Core Team

Source code

Squirrel is an open source project, licensed under the GNU General Public License v3.0. All source code is available here.


[1] 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,