Chercheur post-doctoral (H/F) ANR HOPR - Cryptographie et ordre supérieur

Missions :
Le ou la candidate mènera des travaux de recherche en informatique théorique au sein de l'équipe SPICY de l'IRISA (Rennes). Ce projet concerne des développements théoriques, et éventuellement pratiques, autour de l'assistant de preuve Squirrel pour les protocoles cryptographiques. Il s'agira d'étendre la logique sous-jacente pour faciliter l'utilisation d'ordre supérieur.

Activités :
La logique CCSA (Computationally Complete Symbolic Attacker) permet de raisonner
sur les protocoles cryptographiques et les messages qu'ils contiennent.
Son origine se trouve dans les travaux de Bana et Comon [1], qui étaient fondés sur
la logique du premier ordre. Elle a ensuite évolué progressivement pour devenir une logique CCSA d'ordre supérieur [2], et a été implémentée dans l'assistant de preuve Squirrel [3]. Une
introduction générale à la logique CCSA et à Squirrel est disponible en [4].

Dans les preuves de sécurité cryptographiques, les attaquants considérés disposent d'une puissance de calcul limitée, car il n'est généralement pas possible de garantir la sécurité contre un attaquant tout puissant. Cette restriction apparaît donc naturellement
de plusieurs façons dans notre logique -- voici deux d'entre elles. D'une part, la logique CCSA s'accompagne d'une méthode pour encoder sous forme de schéma d'axiomes des hypothèses cryptographiques, c'est-à-dire des paires de jeux cryptographiques que l'on suppose indistinguables. Ces axiomes demandent en particulier -- de plusieurs façons que l'on ne détaillera pas ici -- que certains sous-termes soient calculables par un adversaire dans le jeu qu'ils expriment. Puisque les adversaires sont des machines de Turing probabilistes polynomiales (PPTIME), utiliser ces axiomes demande donc de vérifier que des termes sont calculables en PPTIME. D'autre part, la logique contient un prédicat exprimant l'indistinguabilité calculatoire, et le raisonnement sur ce prédicat fait souvent intervenir des réductions dans lesquelles le distingueur doit calculer lui même certaines parties d'un terme, qui doivent donc être calculables en PPTME.


Squirrel utilise actuellement des critères très simples pour s'assurer qu'un terme est calculable en PPTIME. Ceux-ci suffisent en pratique, principalement parce que les preuves de protocoles que nous faisons aujourd'hui reposent sur des définitions récursives simples et écrites en dur, qui décrivent les observables lors d'une interaction entre l'adversaire et le protocole. Cependant, la logique elle-même permet des définitions récursives plus complexes, contenant notamment des termes d'ordre supérieur. Celles-ci commencent seulement à être utilisées, dans des preuves plus compliquées et expérimentales. Prouver des garanties de complexité pour de tels termes requerra des techniques plus puissantes. Par ailleurs, le prédicat d'indistinguabilité ne peut pour l'instant s'appliquer qu'à des termes d'ordre au plus 1. L'étendre à des terme
Voir plus sur le site emploi.cnrs.fr...