Cryptographic protocol verifier, copyright ENS, CNRS, INRIA, by Bruno Blanchet
and David Cadé, 2005-YEAR
ENS: 	Ecole Normale Supérieure, 
	45 rue d'Ulm, 75005 Paris, France
CNRS:	Centre National 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 OCaml version 4.03 or higher.
OCaml can be downloaded from
	https://ocaml.org

* under Unix or cygwin

Uncompress the archive using tar:

	gunzip cryptoverifVERSION.tar.gz
	tar -xf cryptoverifVERSION.tar

or if you have GNU tar:

	tar -xzf cryptoverifVERSION.tar.gz

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

	cd cryptoverifVERSION
	./build

* under Windows (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 OCaml cryptographic library
"cryptokit" installed. This library is available at
  https://github.com/xavierleroy/cryptokit
The easiest way to install "cryptokit" is via opam
(See https://opam.ocaml.org/ Under Windows, see 
https://fdopen.github.io/opam-repository-mingw/
Installing OCaml for Windows as instructed on this page
will also install Cygwin, thus providing Unix utilities
useful to run some test scripts of the CryptoVerif distribution,
such as bash, grep, cat, ...)
After installing opam, just run
  opam install cryptokit
to install cryptokit.

* In order to analyze .pcv files, you need to m4 preprocessor.
It is preinstalled in most Unix distributions.
Under Windows, the easiest way is to install Cygwin, as
already suggested above, and install m4 via the Cygwin
installer if it is not already present.

USAGE

This software contains the executable program cryptoverif.  It takes as
input a description of a cryptographic protocol, and checks whether it
satisfies secrecy, authentication, or indistinguishability properties.
The subdirectory examples contains examples of cryptographic protocols.
To run CryptoVerif on example X, execute
	./cryptoverif examples/X
e.g.	./cryptoverif examples/basic/OtwayRees.pcv

A few helper programs are described in Section 10 of the manual,
in directory docs.

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.

I also thank Benjamin Beurdouche and Benjamin Lipp for their help
(updates of examples, bug reports and fixes).

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