Pascal Lafourcade

Home page

Habilitation à Diriger des Recherches

HDR manuscript, slides and Video

Computer Aided Security for:

Cryptographic Primitives,
Voting protocols,
and Wireless Sensor Networks


Abtract : 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:

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.

How to come

The defense will be Tuesday November 6, 2012 at 10.00 am at

Maison Jean Kuntzmann (MJK) - 110 av. de la Chimie
Domaine Universitaire de Saint-Martin-d’Hères
BP 53 - 38041 Grenoble cedex 9
How to come at MJK in english or in french