SCD-Universite de Rennes 1 Modelling and verification of protocols in the computational model with Squirrel Modélisation et vérification de protocoles dans le modèle calculatoire avec Squirrel Squirrelprotocolesmodèle calculatoirevérification Squirrelprotocolcomputational modelverification Protocoles de réseaux d'ordinateurs Cryptographie L'assistant de preuve Squirrel est dédié à la vérification de protocoles cryptographiques. Le modèle utilisé par ce prouveur est appelé modèle calculatoire. Il assure un haut niveau de garanties de sécurité, mais souffre d'un manque d'automatisation. Cette thèse propose d'utiliser des méthodes symboliques et de les adapter pour le modèle calculatoire de Squirrel. Tout d'abord, les protocoles dans Squirrel sont déclarés par des processus écrits dans une variante du pi-calcul appliqué. La sémantique de ces processus n'a pas été définie dans l'article initial présentant Squirrel. L'outil utilise à la place une représentation nommée systèmes d'actions, pour laquelle une sémantique bien définie existe. La première contribution de cette thèse est de définir cette sémantique et de fournir une traduction correcte du pi-calcul vers la représentation interne des protocoles de l'outil. Ensuite, pour automatiser les preuves écrites avec Squirrel, nous concevons un système de types pour les preuves de secret dans le modèle calculatoire. Nous prouvons la correction de ce système de types et l'implémentons dans l'outil, en supportant le chiffrement symétrique et asymétrique. The Squirrel prover is a proof assistant specifically designed for verifying cryptographic protocols. The model used by this prover is named computational model. It ensures a high level of security guarantees, but suffers from a lack of automation. This thesis proposes the use of symbolic methods and their adaptation to the computational setting of Squirrel.   Firstly, protocols in Squirrel are declared with processes written in a variant of applied pi-calculus. The computational semantics of these processes is not defined in the article introducing Squirrel. Instead, the theory underlying Squirrel is based on a different representation, known as systems of actions, for which a well-defined semantics exists. The first contribution of this thesis is to define this semantics and to provide a sound translation from the applied pi-calculus to the tool's internal representation. Secondly, to automate proofs written with Squirrel, we design a type system for proofs of secrecy in the computational model. We prove the soundness of this type system and implement it in the tool, supporting symmetric and asymmetric encryption. Electronic Thesis or DissertationText en application/pdf1 : 1490 Kohttps://ged.univ-rennes1.fr/nuxeo/site/esupversions/fcfa82a5-0a29-4dea-aff8-80e91456a543 Hérouard Clément 1995-02-17 FR 293893195 c.herouard42@gmail.com 2025URENS071 http://www.theses.fr/2025URENS071 2025-11-27 Informatique Université de Rennesthesis.degree.grantor_1 26693823X Doctorat non ouiDelauneStéphanieintervenant_1JensenThomasintervenant_2059884959DelauneStéphanieintervenant_1KünnemannRobertintervenant_5179044117LallemandJosephintervenant_6241794455BlanchetBrunointervenant_3178034738MaffeiMatteointervenant_4224737643 MATISSEecoleDoctorale_1 267602553 IRISA partenaireRecherche_1 026386909 ddc:004 DelauneStéphanieJensenThomasBlanchetBrunoMaffeiMatteoKünnemannRobertLallemandJosephUniversité de RennesMATISSE IRISA ASCII PDF 1526168