Résumé
Régler un achat, accéder à ses comptes et même voter, toutes ces actions peuvent désormais s'effectuer « en ligne ». Comment s'assurer alors qu'aucun intrus ne vienne perturber ces opérations sensibles ? La sécurité de ce type de transactions est garantie par des programmes informatiques appelés « protocoles de sécurité ». Ces protocoles reposent sur des techniques de cryptographie : chiffrement, signature électronique, hachage, etc. Cependant, la cryptographie ne suffit pas.
Il peut parfois suffire d'intervertir deux messages pour accéder à un service de manière illégitime. Il est donc nécessaire d'analyser la structure logique des protocole, combinée à la cryptographie utilisée.
L'analyse formelle des protocoles de sécurité fait appel à de nombreuses techniques de vérification : résolution, unification, théorie équationelle, systèmes de contraintes. L'objectif de ce séminaire est de dessiner un panorama des techniques utilisées et de décrire comment plusieurs protocoles ont pu être corrigés grâce à ces techniques d'analyse.
