The RNTL EVA Project: Explication et Vérification Automatique de protocoles cryptographiques

General statement

The EVA project is a common research effort between LSV/CNRS UMR 8643 & ENS Cachan, Verimag and Trusted Logic S.A. It is funded by a 3-year French national programme, the "Réseau National des Technologies Logicielles", in short the RNTL, sponsored by the French ministries of industry and of research and technology. The EVA project started in Fall 2000.

EVA means "Explication et Vérification Automatique de protocoles cryptographiques": automated explanation and verification of cryptographic protocols. Therefore the stress is both on automation of security proofs (not specifically on automation of attack discovery, which would be the other side of the coin), and explanation of security proofs: it is not enough to claim a protocol is secure, we want to be able to produce formal proofs of it that can be checked independently, and if possible to explain in natural language why and under which assumptions a given protocol is secure.

This Web page is only intended to give information on the various contributions of the LSV to the project. The general page for the EVA project is here. The "fiche résumé" that introduces the goals and perspectives of the EVA project is here.

Current implementations and documentation

© Copyright Jean Goubault-Larrecq, le 19 mars 2001; dernière modification: 27 novembre 2002.