Amphiteatre Maison Jean Kuntzmann
18 septembre 2015 - 10h00
Vérification automatique de protocoles d'examen, de monnaie, de réputation, et de routage (Phd Defense)
par Ali Kassem de Verimag
Résumé : La sécurité est une exigence cruciale dans les applications basées sur l'information et la technologie de communication, surtout quand un réseau ouvert tel que l'Internet est utilisé. Pour assurer la sécurité dans ces applications de nombreux protocoles cryptographiques ont été développé.
Dans cette thèse, nous contribuons à la vérification des protocoles cryptographiques avec un accent sur la vérification formelle et l'automatisation. Tout d'abord, nous étudions les protocoles d'examen. Nous proposons des définitions formelles pour plusieurs propriétés d'authentification et de confidentialité dans le pi-calcul appliqué. Nous fournissons également des définitions abstraites de propriétés de vérifiabilité. Nous analysons toutes ces propriétés en utilisant automatiquement ProVerif sur plusieurs études de cas, et avons identifié plusieurs failles. En outre, nous proposons plusieurs moniteurs pour vérifier les exigences d’examen à l’exécution. Ces moniteurs sont validés par l'analyse d'un exécutions d’examens réels en utilisant l'outil MarQ.
Deuxièmement, nous proposons un cadre formel pour vérifier les propriétés de sécurité de protocoles de monnaie électronique. Nous définissons la notion de vie privée du client et les propriétés de la falsification. Encore une fois, nous illustrons notre modèle en analysant trois études de cas à l'aide ProVerif, et confirmons plusieurs attaques connues. Troisièmement, nous proposons des définitions formelles de propriétés de l'authentification, la confidentialité et le vérifiabilité de protocoles de réputation électroniques. Nous discutons les définitions proposées, avec l'aide de ProVerif, sur un protocole simple de réputation. Enfin, nous obtenons un résultat sur la réduction de la vérification de la validité d'une route dans
les protocoles de routage ad-hoc, en présence de plusieurs attaquants indépendants qui ne partagent pas leurs connaissances.
Dear all,
It is my pleasure to invite you to the defense of my PhD thesis entitled
Automated Verification of Exam, Cash, Reputation, and Routing Protocols
in front of the following committee:
Sebastien Gambs Université de Rennes 1, INRIA
Steve Kremer Inria Nancy--Grand Est, LORIA
Pascal Lafourcade Université Joseph Fourier
Yassine Lakhnech Université Joseph Fourier
Olivier Pereira Université catholique de Louvain
Luca Vigano King's College London
You are also invited to the reception following the defense.
