The next D2 seminar, entitled “The Squirrel Prover”, by Charlie Jacomme, will be held on February 4 at 1:00 pm in room A008.
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.