Automated Verification of Exam, Cash, Reputation, and Routing Protocols

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.

Security is a crucial requirement in the applications based on information and communication technology, especially when an open network such as the Internet is used. To ensure security in such applications security protocols have been used.

In this thesis we contribute to security protocol verification with an emphasis on formal verification and automation. Firstly, we study exam protocols. We propose formal definitions for several authentication and privacy properties  in the Applied Pi-Calculus. We also provide an abstract definitions of verifiability properties. We analyze all these properties automatically using ProVerif on multiple case studies, and identify several flaws. Moreover, we propose several monitors to check exam requirements at runtime. These monitors are validated by analyzing a real exam implementation using MarQJava based tool. Secondly, we propose a formal framework to verify the security properties of non-transferable electronic cash protocols. We define client privacy and forgery related properties. Again, we illustrate our model by analyzing three case studies using ProVerif, and confirm several known attacks. Thirdly, we propose formal definitions of authentication, privacy, and verifiability properties of electronic reputation protocols. We discuss the proposed definitions, with the help of ProVerif, on a simple reputation protocol. Finally, we obtain a reduction result to verify route validity of ad-hoc routing protocols in presence of multiple independent attackers.