Stéphanie Delaune. Verification of security protocols: from confidentiality to privacy. Ph.D. Thesis, École Normale Supérieure de Cachan, France, 2011.
Security is a very old concern, which until quite recently was mostly of interest for military purposes. The deployment of electronic commerce changes this drastically. The security of exchanges is ensured by cryptographic protocols which are notoriously error prone. The formal verification of cryptographic protocols is a difficult problem that can be seen as a particular model-checking problem in an hostile environment. Many results and tools have been developed to automatically verify cryptographic protocols.
Recently, new type of applications have emerged, in order to face new technological and societal challenges, e.g. electronic voting protocols, secure routing protocols for mobile ad hoc networks, ... These applications involve some features that are not taken into account by the existing verification tools, e.g. complex cryptographic primitives, privacy-type security properties, ... This prevents us from modelling these protocols in an accurate way. Moreover, protocols are often analysed in isolation and this is well-known to be not sufficient. In this thesis, we use formal methods to study these aspects concerning the verification of cryptographic protocols.
@phdthesis{delaune-HDR11,
abstract = {Security is a very old concern, which until quite
recently was mostly of interest for military
purposes. The deployment of electronic commerce
changes this drastically. The security of exchanges
is ensured by cryptographic protocols which are
notoriously error prone. The formal verification of
cryptographic protocols is a difficult problem that
can be seen as a particular model-checking problem in
an hostile environment. Many results and tools have
been developed to automatically verify cryptographic
protocols.\par Recently, new type of applications
have emerged, in order to face new technological and
societal challenges, e.g. electronic voting
protocols, secure routing protocols for mobile ad hoc
networks,~... These applications involve some
features that are not taken into account by the
existing verification tools, e.g. complex
cryptographic primitives, privacy-type security
properties,~... This prevents us from modelling these
protocols in an accurate way. Moreover, protocols are
often analysed in isolation and this is well-known to
be not sufficient. In this thesis, we use formal
methods to study these aspects concerning the
verification of cryptographic protocols.},
author = {Delaune, St{\'e}phanie},
month = mar,
school = {{\'E}cole Normale Sup{\'e}rieure de Cachan, France},
type = {M{\'e}moire d'habilitation},
title = {Verification of security protocols: from
confidentiality to privacy},
year = {2011},
nmonth = {3},
lsv-category = {thes},
wwwpublic = {public and ccsb},
}