EVA

Project between LSV (ENS Cachan), VERIMAG (Grenoble) and Trusted Logic SA (Versailles) on the Explanation and verification of cryptographic protocols. The goal of this project is the highly automatized formal verification of cryptographic protocols and the production of proof explanations, i.e. attacks scenario or certification documents (e.g. in the framework of Common Criteria).

The main realizations of the project are :

• the development of prototypes of tools for the automatic verification of protocols based on model checking procedures and methods for the automatic computation of relevant finite abstractions of infinite models ;
• the conception of a base of protocols, as case studies, in a syntax defined for the purpose of the project ;
• the development of proof explanation tools.