Computer Aided Security for : Cryptographic Primitives, Voting protocols, and Wireless Sensor Networ

Résumé :

La sécurité est une des préoccupations principales de l’informatique moderne. De plus en plus de personnes utilisent un ordinateur pour des opérations sensibles comme pour des transferts bancaires, des achats sur internet, le payement des impôts ou même pour voter. La plupart de ces utilisateurs ne savent pas comment la sécurité est assurée, par conséquence ils font totalement confiance à leurs applications. Souvent ces applications utilisent des protocoles cryptographiques qui sont sujet à erreur, comme le montre la célèbre faille de sécurité découverte sur le protocole de Needham-Schroeder dix-sept ans après sa publication. Ces erreurs proviennent de plusieurs aspects : — Les preuves de primitives cryptographiques peuvent contenir des erreurs. — Les propriétés de sécurité ne sont pas bien spécifiées, par conséquence, il n’est pas facile d’en faire la preuve. — Les hypothèses faites sur le modèle de l’intrus sont trop restrictives. Dans cette habilitation, nous présentons des méthodes formelles pour vérifier la sécurité selon ces trois aspects. Tout d’abord, nous construisons des logiques de Hoare afin de prouver la sécurité de primitives cryptographiques comme les chiffrements à clef publique, les modes de chiffrement asymétriques et les codes d’authentification de message (Message authentication codes, MACs). Nous étudions aussi les protocoles de votes électroniques et les réseaux de capteus sans fil (Wireless Sensor Networks, WSNs). Dans ces deux domaines, nous analysons les propriétés de sécurité afin de les modéliser formellement. Ensuite nous développons des techniques appropriées afin de les vérifier. Mots Clefs: Vérification formelle, modèle symbolique, modèle calculatoire, sécurité concrète, chiffrement à clef publique, mode de chiffrement, MAC, chiffrement homomorphique, respect de la vie privée, vote électronique, réseaux de capteurs sans fil, découverte de voisinage, intrus indépendants, algorithmes de routage, résilience.

Abstract :

Security is one of the main issues of modern computer science. Nowadays more and more people use a computer to perform sensitive operations like bank transfer, Internet shopping, tax payment or even to vote. Most of these users do not have any clue how the security is achieved, therefore they totally trust their applications. These applications often use cryptographic protocols which are notoriously error prone even for experts. For instance a flaw was found in the Needham-Schroeder protocol seventeen years after its publication. These errors come from several aspects: - Proofs of security of cryptographic primitives can contain some flaws. - Security properties are not well specified, making it difficult to formally prove them. - Assumptions on the intruder\'s model might be too restrictive. In this habilitation thesis we propose formal methods for verifying security of these three layers. First, we build Hoare logics for proving the security of cryptographic schemes like public encryption, encryption modes, Message Authentication Codes (MACs). We also study electronic voting protocols and wireless sensor networks (WSNs). In each one of these areas we first analyze the required security properties in order to propose a formal model. Then we develop adequate techniques for their verification. Keywords: Formal verification, computational model, symbolic model, concrete security, public encryption scheme, encryption modes, MAC, homomorphic encryption, privacy, electronic voting protocol, wireless sensor networks, neigbourhood discovery, independent intruders, routing algorithms, resilience.