Automatisation de preuves de protocoles cryptographiques pour l’outil Squirrel / Mechanizing cryptographic protocols proofs in the Squirrel tool

[English below]

La vérification formelle de protocoles cryptographiques dans le modèle calculatoire offre de fortes garanties de sécurité, mais demeure difficile à automatiser. La logique CCSA (Computationally Complete Symbolic Attacker), implémentée dans l'assistant de preuve Squirrel, permet un raisonnement calculatoire sûr au sein d'une logique d'ordre supérieur polymorphe dont la sémantique est définie par la notion de vérité écrasante.

Dans cette thèse, nous introduisons une tactique fondée sur les solveurs SMT afin d'automatiser le raisonnement dans Squirrel. Nous proposons tout d'abord la première définition formelle de la logique locale polymorphe de Squirrel. Nous présentons ensuite trois traductions vers la logique de \why : deux traductions portant sur des fragments restreints de la logique locale de Squirrel, ainsi qu'une traduction de la logique locale complète. Nous démontrons la correction de ces traductions, permettant ainsi l'utilisation de solveurs SMT génériques. Enfin, nous implémentons la traduction complète sous la forme d'une tactique SMT pour Squirrel et montrons son efficacité au travers de tests systématiques et de plusieurs études de cas.

Formal verification of cryptographic protocols in the computational model provides strong security guarantees but remains challenging to automate. The Computationally Complete Symbolic Attacker (CCSA) logic, implemented in the Squirrel proof assistant, provides computationally sound reasoning in a polymorphic higher-order logic whose validity is defined as overwhelming truth.

In this thesis, we introduce an SMT-based tactic to automate Squirrel's logic. We first provide the first formal definition of Squirrel's polymorphic local logic.
We then present three translations into the \why logic: two from a restricted fragment of Squirrel's local logic, and one translation from the full local logic. 
We prove the soundness of these translations, thereby enabling the use of off-the-shelf SMT solvers. Finally, we implement the full translation as an SMT tactic for Squirrel, and demonstrate its effectiveness through systematic benchmarks and various case studies.