The Squirrel Prover and its Logic

David Baelde (1, 2) , Stéphanie Delaune (1, 2) , Charlie Jacomme (3, 4) , Adrien Koutsos (5) , Joseph Lallemand (1, 2)

1 IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires
2 SPICY - Security & PrIvaCY
3 LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
4 PESTO - Proof techniques for security protocols
5 PROSECCO - Programming securely with cryptography

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.

Domaines: Informatique [cs]

David Baelde, Stéphanie Delaune, Charlie Jacomme, Adrien Koutsos, Joseph Lallemand. The Squirrel Prover and its Logic. ACM SIGLOG News, 2024, 11 (2), ⟨10.1145/3665453.3665461⟩. ⟨hal-04579038⟩