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.

Introduction

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.

eva2eva outputs the operational model in an LAEVA-like readable syntax. This tool can then be used to show how this compiles internally.
eva2h1 tool instead converts the input protocol to a set of Horn clauses, in Prolog notation, or in TPTP format, a standard format used primarily for testing automated theorem provers, now become a de facto standard for writing first-order formulas. This can then be fed to an automated theorem prover like SPASS, Vampire, Waldmeister, or h1, for example: if the automated theorem prover stops without finding a contradiction, then the protocol is secure.
eva2cpl translates LAEVA specifications to a Lisplike syntax called CPL, which is the input format of the tools like Hermes and Securify from the EVA project.
eva2tex translates LAEVA specifications to LaTeX.

Documentation

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

a description of the principles and the architecture of evatrans,
installation instructions and reference of the commands,
the grammar of the LAEVA input syntax,
the semantics for the operational models produced by the compiler.

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

Download

the evatrans library.
- evatrans.cma (compressed tar)
- sources (compressed tar)
the eva2h1 source code:
- alone (compressed tar)
- or with the code of the evatrans library (compressed tar)
the eva2cpl source code:
- alone (compressed tar)
- or with the code of the evatrans library (compressed tar)

Installation

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

README for the evatrans library and eva2eva.
README for the eva2h1.
README for the eva2cpl.

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:

sources documentation for the evatrans library.
sources documentation for eva2cpl.
sources documentation for eva2h1.

Links

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.