Abstract FR:

Les protocoles de sécurité enregistrent souvent des données disponibles lors de leurs exécutions dans un journal pour une éventuelle analyse a posteriori, aussi appelée audit. En pratique, les procédures d'audit restent souvent informelles, et le choix du contenu des journaux est laissé au bon sens du programmeur. Cette thèse a pour but la formalisation et la vérification des propriétés attendues des journaux d'audit. D'abord, nous nous intéressons à l'utilisation des journaux par les protocoles de sécurité dits optimistes qui, contrairement aux protocoles classiques, reposent sur le contenu des journaux pour remettre certaines vérifications de sécurité à la fin de leur exécution. Nous faisons une étude formelle de deux schémas optimistes : la mise en gage de valeur et le porte-monnaie électronique. En appliquant les techniques issues des langages de processus, nous montrons que les informations enregistrées par leurs implémentations suffisent pour détecter toute tentative de tricherie de participants. Ensuite nous définissons l'auditabilité comme la capacité d'un protocole de collecter assez de preuves pour convaincre une procédure d'audit préétablie (juge). Nous proposons une méthode basée sur les types avec des raffinements logiques, pour vérifier l'auditabilité, et nous l'implémentons dans une extension d'un typeur existant. Nous montrons que la vérification de l'auditabilité se réduit à une vérification par le typage. Nous implémentons également un support logique des pré- et post-conditions génériques pour améliorer le typage modulaire des fonctions d'ordre supérieur.