Date: Tuesday, February 4th 2025 – 13h00
Place: A008
Title: The Squirrel Prover
The Squirrel Prover is a proof assistant dedicated to cryptographic protocols. It relies on a higher-order logic following the computationally complete symbolic attacker approach. It thus provides guarantees in the computational model. In this talk, we will introduce the main ingredients underlying its logic and proof system, trying to outline why it does yield computational guarantees and how it allows to reason over protocols. We will then cover the current development status of Squirrel, showcasing its current features and expressivity.
