Cryptographic protocol verifier, copyright ENS, CNRS, INRIA, by Bruno Blanchet
and David Cadé, 2005-2016
ENS: 	Ecole Normale Supérieure, 
	45 rue d'Ulm, 75005 Paris, France
CNRS:	Centre Nationale de la Recherche Scientifique
INRIA:  Institut National de Recherche en Informatique et Automatique
	Domaine de Voluceau - Rocquencourt - B.P. 105 - 78153 Le Chesnay

This package contains source files, documentation, and examples of a
cryptographic protocol verifier. The material contained in this
package is under the CeCILL-B license. (The CeCILL-B license is 
a BSD-style license. See the file LICENSE for more information.)

This software can be used to prove secrecy and authentication
properties of cryptographic protocols, in the computational model. (If
you want a verifier for the Dolev-Yao model, please download
ProVerif.)

INSTALL

To run this software, you need Objective Caml version 3.00 or
higher. Objective Caml can be downloaded from
	http://caml.inria.fr

* under Unix or cygwin

Uncompress the archive using tar:

	gunzip cryptoverif1.23.tar.gz
	tar -xf cryptoverif1.23.tar

or if you have GNU tar:

	tar -xzf cryptoverif1.23.tar.gz

This will create a directory named cryptoverif1.23 in the current directory.
Go into this directory, and build the programs:

	cd cryptoverif1.23
	./build

* under Windows NT, 2000, or XP (without cygwin)

The recommended way is to use the precompiled binaries for Windows,
available as a separate distribution.

In order to run implementations of protocols generated by 
CryptoVerif, you need to have the Caml cryptographic library
"cryptokit" installed. This library is available at
  http://forge.ocamlcore.org/projects/cryptokit/
You need to either 
- arrange so that the installed cryptokit library is in
subdirectory "implementation/cryptokit" of the CryptoVerif
distribution (possibly via a symbolic link)
- or install the cryptokit library in the "cryptokit" subdirectory
of the Caml standard library
- or modify the variable CRYPTOKIT in the scripts
implementation/npsk/build.sh
implementation/wlsk/build_wlsk.sh
implementation/ssh/build.sh
so that the cryptokit library is included.

USAGE

This software contains one executable program, cryptoverif.  It takes as
input a description of a cryptographic protocol, and checks whether it
can leak some secrets. The subdirectory examples contains examples
of cryptographic protocols. To run CryptoVerif on example X, execute
	./cryptoverif examples/X
e.g.	./cryptoverif examples/otway-rees3Stream

Note: CryptoVerif must be run in the directory that contains the files
"default.cvl" and "default.ocvl" (which is the cryptoverif1.23
directory). CryptoVerif accesses these files which contain definitions
of cryptographic primitives.

COPYRIGHT

This software is distributed under CeCILL-B license. The CeCILL-B
license is a BSD-style license. See the file LICENSE for more
information.

BUG REPORTS

Bugs and comments should be reported by e-mail to
	Bruno.Blanchet@inria.fr

ACKNOWLEDGMENTS

I warmly thank David Pointcheval for his advice and explanations
of the computational proofs of protocols. This project would not have
been possible without him.

This project was partly supported by ARA SSIA Formacrypt and is partly
supported by the ANR project ProSe (decision ANR-2010-VERS-004-01).