Vincent Cheval

Recherche

Début septembre 2010, j'ai démarré une thèse avec Hubert Comon-Lundh et Stéphanie Delaune sur les preuves automatiques d'indistinguabilité

Abstract : Les protocoles de sécurité sont de petits programmes distribués visant à assurer la sécurité des communications à travers des réseaux non sécurisé (comme l'internet). Prouver que de tels protocoles satisfont une propriété de sécurité est un problème important que ce soit du point de vue économique (transfert bancaire sécurisé), militaire (communication) ou encore social (protection de la vie privée).
L'objectif de la thèse est de développer et de comparer des démonstrateurs automatiques, spécialisés dans des preuves d'indistinguabilité. Ce type de preuve est nécessaire pour vérifier certaines propriétés des protocoles cryptographiques, typiquement des propriétés d'anonymat ou de secret fort. Il n'existe actuellement qu'un seul logiciel qui permet de prouver des propriétés d'équivalence, en présence d'un attaquant actif: ProVerif, dévelopé au LIENS. On se propose de développer un autre outil, basé sur des techniques très différentes, et de comparer avec ProVerif.

• Mes publications
• Mes exposés
• Outils développés :
  • Adecs : Outil déterminant l'équivalence de système de contraintes.
  • Datep : Outil déterminant l'équivalence de trace de protocoles.

Cette thèse s'inscrit dans le cadre de l'axe SECSI du laboratoire : page web de l'axe.

Enseignement

En parallèle avec la thèse, j'effectue un monitorat à l'ENS de Cachan.

• TP d'informatique dans le cadre du L3-IST (2010)
• Projet programmation Java L3 (Dpt-Info) (2010): Site web
• TP programmation (prépa agreg option info) (2011 & 2010): Site web
• TP Programmation L3 (Dpt-Info) (2011) :
  • Signatures minimales des TP
  • TP 1
  • TP 2
  • TP 3
  • TP 4
  • TP 5
  • TP 6

Participation collective

• Participation au groupe Outils Informatiques interne du LSV, développement d'une base de données et d'interface web associée pour les ressources humaines du laboratoire. Responsable : Nicolas Markey
• Participation au groupe Communication interne du LSV
• Participation à l'organisation du séminaire interne du laboratoire en 2010