Doctorant en Vérification de protocoles avec opérateurs AC à l'aide de PROVERIF. (H/F)

Sujet de thèse :
La vérification formelle repose sur des techniques de raisonnement mathématique pour établir des propriétés de systèmes distribués complexes. Dans les cadres de vérification symbolique, les comportements du système et les manipulations de données sont représentés sous forme de termes algébriques et analysés à l’aide de procédures de déduction automatisées. Une difficulté centrale dans ce contexte réside dans le traitement des structures algébriques satisfaisant des propriétés équationnelles non triviales, en particulier l’associativité et la commutativité. La prise en charge de telles théories augmente considérablement la complexité des procédures de raisonnement automatisé et soulève des questions fondamentales concernant la correction, la complétude et la terminaison.
ProVerif est un outil de raisonnement automatisé largement utilisé, basé sur une traduction des problèmes de vérification en clauses de Horn [5], ainsi que sur une procédure de résolution dont la correction est prouvée [1, 2]. Bien que la correction soit garantie, la terminaison n’est pas assurée en général, bien qu’elle soit souvent observée en pratique.
Plusieurs extensions ont été étudiées afin d’intégrer les théories associatives-commutatives (AC) dans ce cadre, y compris les théories liées au XOR, aux groupes abéliens et à l’exponentiation de Diffie-Hellman, principalement par le biais de techniques de prétraitement [4]. Cependant, ces approches présentent des limites importantes et n’ont pas été intégrées dans l’outil principal. Récemment, nous avons étendu ProVerif pour prendre en charge le XOR dans l’analyse des propriétés d’accessibilité [3]. En nous appuyant sur ce travail, l’objectif de ce projet de thèse est de développer de nouvelles techniques de résolution capables de gérer des classes plus riches de théories équationnelles associatives-commutatives dans le même cadre de raisonnement automatisé.

Objectifs du projet de thèse
Le premier objectif du projet de thèse sera d’acquérir une compréhension approfondie du moteur de résolution de ProVerif et de ses fondements théoriques.
L’objectif scientifique principal consistera ensuite à étendre cette procédure de résolution pour prendre en charge des théories équationnelles associatives-commutatives supplémentaires, telles que les groupes abéliens (AG), l’exponentiation de Diffie-Hellman ou les appariements bilinéaires. L’accent sera d’abord mis sur les propriétés d’accessibilité.
Plus précisément, le projet de thèse comportera les tâches suivantes :

Concevoir une nouvelle procédure de résolution en adaptant le cadre existant pour prendre en charge des théories associatives-commutatives plus riches ;
Établir les propriétés de correction et, dans la mesure du possible, de complétude de la procédure proposée ;
Implémenter la nouvelle procédure dans le code source de ProVerif et évaluer son comportement pratique, en prêtant une attention particulière aux que
Voir plus sur le site emploi.cnrs.fr...