@phdthesis{Laf06,
title = { V\'erification des protocoles cryptographiques en pr\'esence de th\'eories \'equationnelles },
author = {Lafourcade, Pascal},
month = {sep},
year = {2006},
address = {ENS Cachan},
note = {209~pages},
type = {Th\`ese de doctorat},
school = {Laboratoire Sp\'ecification et V\'erification, ENS Cachan, France},
team = {other},
abstract = {The rise of the internet of new technologies has reinforced the key role of computer science in communication technology. The recent progress in these technologies has brought a dramatic change in the ways how we communicate and consume. All these communication activities are subject to complex communication protocols that a user does not control completely. Users of communication protocols require that their communications are {"}secure{"}. The developers of these communication protocols aim to secure communications in a hostile environment by cryptographic means. Such an environment consists of a dishonest communication participant, called an {"}intruder{"} or {"}attacker{"}... We suppose that the intruder controls the network on which the messages are exchanged.\par The verification of a cryptographic protocol either ensures that no attack is possible against the execution of the protocol in presence of a certain intruder, or otherwise exhibits an attack. One important assumption in the verification of cryptographic protocols is the so-called {"}perfect cryptography assumption{"}, which states that the only way to obtain knowledge about an encrypted message is to know its decryption key. This hypothesis is not sufficient to guarantee security in reality. It is possible that certain properties used in the protocol allow the intruder to obtain some information.\par One way to weaken this perfect cryptography assumption is to take into account in the model certain algebraic properties. We develop a formal approach for verifying the so-called secrecy property of cryptographic protocols in the presence of equational theories and of homomorphism.},
}
