Doctorat en Science Informatique - In Foundations Of Ccsa Logics H/F CNRS

Détail du poste

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 oeuvre 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é computationnelle. Cette question est triviale sans noms frais, mais devient intéressante une fois qu'ils peuvent être pris en compte.

Au-delà de ces deux premiers objectifs, le doctorant abordera des questions plus larges. Il serait souhaitable d'obtenir des résultats de complétude dans le cadre du premier ordre (ou même du second ordre). Nous nous attendons également à ce que la restriction technique aux bandes finies dans la sémantique de nos logiques cause des difficultés récurrentes ; il serait naturel d'explorer comment elle pourrait être levée. Enfin, le travail ne devrait pas rester uniquement attaché à ses motivations originales dans les logiques CCSA : les questions abordées ici ne sont même pas spécifiques à la cryptographie, mais traitent de questions larges sur les probabilités et la logique, qui ont été abordées dans des travaux classiques et récents [8,9].

[0] Antoine. "Propositional Logics of Overwhelming Truth". CSL 2025.
[1] Bana, Comon. "A computationally complete symbolic attacker for equivalence properties." CCS 2014.
[2] Baelde, Koutsos, Lallemand. "A higher-order indistinguishability logic for cryptographic reasoning." LICS 2023.
[3] Baelde et al. "An interactive prover for protocol verification in the computational model." S&P 2021.
[4] Baelde et al. "Foundations for Cryptographic Reductions in CCSA Logics." CCS 2024.
[5] Pitts. "Nominal logic, a first order theory of names and binding." Information and Computation 2003.
[6] Miller, Tiu. "A proof theory for generic judgments." ACM TOCL 2005.
[7] Goubault-Larrecq. "A semantics for nabla." MSCS 2019.
[8] Geiger, Paz, Pearl. "Axioms and algorithms for inferences involving probabilistic independence." Information and Computation 1991.
[9] Li et al. "A Nominal Approach to Probabilistic Separation Logic." LICS 2024.

Contexte de travail
Cette thèse s'inscrit dans le cadre du PEPR cybersécurité et plus précisément du projet SVP : https://pepr-cyber-svp.cnrs.fr/

A propos du laboratoire :
L'IRISA est aujourd'hui l'un des plus grands laboratoires de recherche français (plus de 850 personnes) dans le domaine de l'informatique et des technologies de l'information. Structuré en sept départements scientifiques, l'IRISA est un centre de recherche d'excellence dont les priorités scientifiques sont la bio-informatique, la sécurité des systèmes, les nouvelles architectures logicielles, la réalité virtuelle, l'analyse des big data et l'intelligence artificielle. Tourné vers l'avenir de l'informatique et nécessairement tourné vers l'international, l'IRISA est au coeur même de la transition numérique de la société et de l'innovation au service de la cybersécurité, de la santé, de l'environnement et de l'écologie, des transports, de la robotique, de l'énergie, de la culture et de l'intelligence artificielle.
Présentation de l'IRISA en tant que laboratoire d'affectation : https://www.irisa.fr/umr-6074
Présentation du CNRS en tant qu'employeur : https://www.cnrs.fr/fr/le-cnrs
présentation de l'équipe d'accueil : https://www-spicy.irisa.fr/

Le poste se situe dans un secteur relevant de la protection du potentiel scientifique et technique (PPST), et nécessite donc, conformément à la réglementation, que votre arrivée soit autorisée par l'autorité compétente du MESR.
Contraintes et risques
Le/la doctorant(e) pourra effectuer plusieurs séjours de recherche courts. Des déplacements chez les partenaires du projet pour des réunions d'avancement sont également prévus.