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}, }