| Version imprimable |
| 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) | ||
Hérouard, Clément - (2025-11-27) / Université de Rennes Modelling and verification of protocols in the computational model with Squirrel Langue : Anglais Directeur de thèse: Delaune, Stéphanie Laboratoire : IRISA Ecole Doctorale : MATISSE Thématique : Informatique | ||
Mots-clés : Squirrel, protocoles, modèle calculatoire, vérification, Protocoles de réseaux d'ordinateurs, Cryptographie Résumé : 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. Résumé (anglais) : 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. Identifiant : rennes1-ori-wf-1-21929 | ||
| Exporter au format XML |