Official LSV Web Site

The EVA translator v.2

evatrans is a toolkit for parsing, type-checking and compiling cryptographic protocols specified in an high level abstract language. It has been written for the project EVA.


The core of evatrans is the library evatrans.cma, an ocaml library for parsing, type-checking, and compiling cryptographic protocols in the LAEVA language (the input language of EVA) to internal data structures describing an operational model that tools for automatic cryptographic protocol verification like Hermes, or Securify or h1 can work on.
The high-level LAEVA notation focuses on the form of the messages exchanged during the protocol whereas the operational model describes the operations performed by the participants. Hence, roughly, the EVA compiler transforms a sequence of messages into a set of processes (or programs), one for each role of the protocol (user, server, signing authority, etc.) The implementability of protocols as well as the correctness of typing of messages is also checked during compilation.
Several wrappers have been implemented in order to print the result of the compilation in various syntaxes. The are written in OCaml on the top of evatrans, and can be compiled separately.


The documentation and reference manual for evatrans are available as the EVA technical report number 9.
This TR contains:

It can also be downloaded from the webpage of the EVA project.



The compilation instructions for the above package can be found in the following README:

Sources documentation

The sources of the various tools of evatrans have been documented using ocamldoc. They are distributed along with the sources of the project, and are also available online:


The EVA project
EVA (Explanation and Automated Verification of cryptographic protocols) is a project of the french national network Reseau National des Technologies du Logiciel (RNTL).
Its purpose is to create automated cryptographic protocol verification tools, and to extract explanations why they are secure (in case they are) from verification, as readable and independently checkable proofs.
EVA translator v.1
The first version of the EVA translator compiles cryptographic protocols in an earlier version of the LAEVA language into CPL. It has developed in C, ocaml and HimML by Jean Goubault-Larrecq and it is available here.

About LSV