David Baelde, Stéphanie Delaune, Charlie Jacomme, Adrien Koutsos, and Joseph Lallemand. The Squirrel Prover and its Logic. ACM SIGLOG News, 11(2):62–83, 2024.
The Squirrel system is an interactive prover for the verification of cryptographic protocols. It relies on a dedicated higher-order logic and provides security guarantees akin to those classically obtained by cryptographers, against attackers modeled as arbitrary probabilistic polynomial-time Turing machines. In this paper, we provide a high-level introduction to the logic behind Squirrel, and briefly describe some of the interesting technical challenges encountered during its construction.
@article{BDJKL-siglog24,
abstract = {The Squirrel system is an interactive prover for the verification of cryptographic protocols.
It relies on a dedicated higher-order logic and provides security guarantees akin to those classically obtained by cryptographers,
against attackers modeled as arbitrary probabilistic polynomial-time Turing machines.
In this paper, we provide a high-level introduction to the logic behind Squirrel, and briefly describe some of
the interesting technical challenges encountered during its construction.},
author = {David Baelde and
St{\'{e}}phanie Delaune and
Charlie Jacomme and
Adrien Koutsos and
Joseph Lallemand},
title = {The Squirrel Prover and its Logic},
journal = {{ACM} {SIGLOG} News},
volume = {11},
number = {2},
pages = {62--83},
year = {2024},
}