Vérification formelle de familles avancées de protocoles de sécurité : vote électronique et API

For a long time now, formal methods have been successfully used to analyze security protocols. Several tools have even been developed to tackle automatically different proof techniques and, therefore, to ease the verification of such protocols. However, when it comes to electronic voting and APIs, current tools tend to reach their limits because they can’t handle some cryptographic primitives (e.g. homomorphic encryption), or the security properties (e.g. ballot secrecy), involved in those protocols.In this thesis, we first work on two cases studies of existing and deployed systems: a Norwegian e-voting protocol and a CNRS boardroom voting protocol. These two protocols are analyzed using the applied pi-calculus model and we discuss in details about their security properties, in different corruption scenarios. Even though this part provides several reusable results, it also shows the complexity to prove them by hand and, therefore, underlying a real need for automation in those proofs.The third part of this thesis focuses on a possible lead in direction of this needed automation: type- systems. Indeed, we build upon a recent work describing a new type-system designed to deal with equivalence properties, in order to apply this on the verification of equivalence-based properties in elec- tronic voting like ballot-secrecy. We present an application of this method through the example of Helios, a well-known, web-based, and open-audit, e-voting system.Another family of advanced security protocols are APIs: secure interfaces devoted to allow access to some information stored into a secured trusted hardware without leaking it outside. Such protocols are not immune to attacks; in fact, recent work seems to show the opposite. In the second part of this thesis, we provide a new design for APIs, including a revocation functionality, which is not always considered. In addition, we include a fully formal analysis of this API allowing that a malicious combination of API’s commands does not leak any key, even when the adversary may brute-force some of them.Les méthodes formelles ont depuis longtemps fait leurs preuves dans l’études des protocoles de sécurité. Il existe même plusieurs outils qui permettent d’automatiser la vérification de ces protocoles. Toutefois, ceux-ci se montrent encore parfois dans l’incapacité d’analyser certains protocoles, que ce soit à cause de certaines primitives cryptographiques employées ou des propriétés que l’on cherche à démontrer.Dans la première partie de cette thèse, on étudie deux systèmes existants: un protocole de vote par internet Norvégien et un protocole pour les votes en réunion du CNRS. A l’aide du pi-calcul appliqué, nous analysons des garanties de sécurité qu’ils proposent et ce, au travers de différents scénarios de corruption. Mais malgré les résultats réutilisables obtenus, ces preuves démontrent également la difficulté de les effectuer à la main.C’est pourquoi la troisième partie de cette thèse est consacrée à une nouvelle piste dans l’automatisation de telles preuves: les systèmes de types. En effet, inspirés par le développement récent d’un système de types permettant de traiter des propriétés d’équivalence, nous l’avons utilisé afin de démontrer des propriétés comme l’anonymat dans le vote électronique. Nous avons appliqué cette méthode à un exemple: Helios, un système de vote par internet bien connu.Il existe une autre famille de protocoles de sécurité : les APIs. Ces interfaces permettent l’utilisation d’informations stockées dans des dispositifs sécurisés sans qu’il soit normalement possible de les en extraire. Des travaux récents montrent que de telles interfaces sont également vulnérables. La deuxième partie de cette thèse présente un nouveau design d’API, incluant une fonctionnalité de révocation, rarement présente dans les solutions existantes. Nous démontrons, par une analyse entièrement formelle, qu’aucune combinaison de commandes ne permet de faire fuir des clefs sensées rester secrètes, même si l’adversaire parvient à en brute-forcer certaines