H/F Doctorat en Science informatique - in Foundations of CCSA Logics

Sujet de thèse :


Titre: Fondements des logiques CCSA

Les logiques CCSA sont utilisées pour raisonner sur les messages et protocoles cryptographiques. Elles ont émergé des travaux pionniers de Bana et Comon [1] basés sur la logique du premier ordre, qui a progressivement évolué vers une logique CCSA du second ordre [2], mise en œuvre dans l'assistant de preuve Squirrel [3]. Dans ces logiques, des constantes spéciales appelées noms sont utilisées pour modéliser des familles d'échantillonnages aléatoires, utilisées par exemple pour modéliser des clés cryptographiques ou des nonces. Les hypothèses cryptographiques (c'est-à-dire, la sécurité de jeux particuliers impliquant des primitives cryptographiques) sont alors exprimées sous forme de schémas d'axiomes - formellement, ces axiomes peuvent être générés à partir des jeux cryptographiques par bi-déduction.

L'objectif global de cette thèse sera d'élargir le champ d'application des logiques CCSA, en considérant de nouvelles variantes dans cet espace conceptuel, et de mieux comprendre leur théorie des preuves. Une partie du travail consistera donc à concevoir de nouvelles logiques avec une sémantique appropriée. Une autre partie consistera à étudier les propriétés clés de ces logiques, telles que la compacité, la décidabilité... et à concevoir des systèmes de preuves pour lesquels des résultats de complétude peuvent être obtenus. Certains de ces résultats peuvent avoir un impact pratique dans l'assistant de preuve Squirrel, qui pourrait devenir plus expressif ou bénéficier de nouvelles capacités de raisonnement automatisé.

Un premier objectif sera d'équiper les logiques CCSA de quantification sur des noms frais. La logique enrichie devrait permettre d'écrire des choses telles que « pour tout x, frais n, n - x » qui devraient être valides, car un nom n qui est frais par rapport à x a une probabilité négligeable d'entrer en collision avec ce nom. Ce quantificateur serait utile pour exprimer des axiomes cryptographiques mais aussi dans des lemmes intermédiaires où les utilisateurs de Squirrel introduisent typiquement des noms frais : au lieu des noms frais codés en dur actuels, un traitement logique approprié apportera plus de flexibilité, par exemple choisir le nom frais en fonction du contexte, ou le renommer, tant que la fraîcheur est assurée. Ce projet, dont les premières étapes sont actuellement en cours d'investigation dans le cadre du stage de M2 de Thibaut Antoine, s'inspirera à la fois de la logique nominale [5] et de la quantification générique [5] et de sa sémantique catégorielle [7]. Une fois terminé, la logique devrait être conservatrice par rapport à la logique CCSA du second ordre existante, et venir avec un calcul séquentiel naturel.

En s'appuyant sur les résultats de l'objectif précédent, un deuxième but sera d'étendre les résultats de complétude obtenus pour les logiques modales CCSA de [0] à un cadre incluant l'indistinguabilité co
Voir plus sur le site emploi.cnrs.fr...