SVP

Aperçu

Mettre au point des techniques et des outils permettant d’apporter aux protocoles cryptographiques des garanties de sécurité.

Stéphanie Delaune, DR CNRS

Le projet SVP envisage de développer de nouvelles fonctionnalités dans les outils existants pour permettre l’analyse de protocoles toujours plus complexes ; de construire des ponts entre les différentes techniques de preuves existantes et les outils associés afin de tirer profit des forces de chacun d’entre eux ; et enfin de valider les techniques et outils développés dans le cadre de ce projet sur des protocoles déjà largement déployés, comme sur des applications plus récentes, en plein essor, tel le vote par Internet.

Les problématiques soulevées doivent répondre à la vérification de propriétés comme l’anonymat et la non-traçabilité, ou la prise en compte des aspects probabilistes que l’on peut trouver dans certains protocoles.

Mots clefs : vérification formelle de protocole (approche symbolique et approche calculatoire).

Les tâches

Nos recherches

Obtenir des garanties au niveau symbolique

Une meilleure intégration des primitives cryptographiques.
La vérification de propriétés d’équivalence.
Les modèles probabilistes et leur vérification.
Efficacité et utilisabilité des outils.
Élaborer les bases d’une plateforme multi-outils et multipropriétés.

Obtenir des garanties au niveau calculatoire

La poursuite des développements sur les outils permettant d’obtenir des garanties calculatoires (CRYPTOVERIF et EASYCRYPT) tout en proposant de nouvelles approches prometteuses (approche CSSA et outil Squirrel, collaboration avec de nouveaux outils, résistance contre les attaques quantiques).

Obtenir des garanties au niveau de l’implémentation

La preuve symbolique et calculatoire d’implémentations de protocoles, la compilation certifiée, la lutte contre les attaques par canaux auxiliaires.

Applications

Les études de constructions cryptographiques, des protocoles déployés à grande échelle via des contributions sur les standards ainsi que le développement de cas d’usage autour du vote électronique.