Stéphanie Delaune. Vérification des protocoles cryptographiques et propriétés algébriques. Ph.D. Thesis, Laboratoire Spécification et Vérification, ENS Cachan, France, 2006.
Cryptographic protocols are small concurrent programs designed to guarantee the security of exchanges between participants using non-secure medium. Establishing the correctness of these protocols is crucial given the increasing number of applications, such as electronic commerce, that exchange information on the Internet. Unfortunately, the existence of cryptographic primitives such as encryption is not sufficient to ensure security. 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. To verify such protocols, a line of research consists in considering encryption as a black box and assuming that an adversary can't learn anything from an encrypted message except if he has the key. This is called the perfect cryptography assumption. Many results have been obtained under this assumption, but such an assumption is too strong in general. Some attacks exploit in a clever way the interaction between protocol rules and properties of cryptographic operators.
In this thesis, we relax the perfect cryptography assumption by taking into account some algebraic properties of cryptographic primitives. We give decision procedures for the security problem in presence of several algebraic operators.
@phdthesis{THESE-delaune06,
abstract = {Cryptographic protocols are small concurrent programs
designed to guarantee the security of exchanges
between participants using non-secure medium.
Establishing the correctness of these protocols is
crucial given the increasing number of applications,
such as electronic commerce, that exchange
information on the Internet. Unfortunately, the
existence of cryptographic primitives such as
encryption is not sufficient to ensure security. The
security of exchanges is ensured by cryptographic
protocols which are notoriously error-prone.\par The
formal verification of cryptographic protocols is a
difficult problem that can be seen as a particular
model-checking problem in an hostile environment. To
verify such protocols, a line of research consists in
considering encryption as a black box and assuming
that an adversary can't learn anything from an
encrypted message except if he has the key. This is
called the \emph{perfect cryptography} assumption.
Many results have been obtained under this
assumption, but such an assumption is too strong in
general. Some attacks exploit in a clever way the
interaction between protocol rules and properties of
cryptographic operators. \par In this thesis, we
relax the perfect cryptography assumption by taking
into account some algebraic properties of
cryptographic primitives. We give decision procedures
for the security problem in presence of several
algebraic operators.},
author = {Delaune, St{\'e}phanie},
month = jun,
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
title = {V{\'e}rification des protocoles cryptographiques et
propri{\'e}t{\'e}s alg{\'e}briques},
year = {2006},
nmonth = {6},
lsv-category = {thes},
wwwpublic = {public and ccsb},
}