Protocol verifier, copyright INRIA-LIENS-MPII, by Bruno Blanchet
and Xavier Allamigeon, 2000-2011.
INRIA: 	Institut National de Recherche en Informatique et Automatique,
	Domaine de Voluceau, Rocquencourt, 78153 Le Chesnay Cedex, France
LIENS: 	Laboratoire d'Informatique de l'Ecole Normale Supérieure, 
	45 rue d'Ulm, 75005 Paris, France
MPII:	Max-Planck-Institut für Informatik, 
	Stuhlsatzenhausweg, 66123 Saarbrücken, Germany

This software can be used to prove secrecy and authenticity properties
of cryptographic protocols.

INSTALL

There are two possibilities for installing ProVerif: 
either the source distribution or the binary distribution for Windows.

******* Source distribution (and documentation)

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

Uncompress the source and documentation archives using tar:

	gunzip proverif1.86pl3.tar.gz
	tar -xf proverif1.86pl3.tar
	gunzip proverifdoc1.86pl3.tar.gz
	tar -xf proverifdoc1.86pl3.tar

or if you have GNU tar:

	tar -xzf proverif1.86pl3.tar.gz
	tar -xzf proverifdoc1.86pl3.tar.gz

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

	cd proverif1.86pl3
	./build

* under Windows NT, 2000, or XP

Uncompress the archives proverif1.86pl3.tar.gz and proverifdoc1.86pl3.tar.gz
using Winzip, in the directory of your choice. This will create a
subdirectory named proverif1.86pl3. Open a DOS window, cd into the
proverif1.86pl3 directory and run the build .BAT file:

	build

The system can run under Windows, but it is not very Windows-friendly:
you have to use the command line to run the programs. Improving the interface
is on the to-do list...

******* Binary distribution for Windows (and documentation)

* under Cygwin

Uncompress the binary and documentation archives using GNU tar:

	tar -xzf proverifbsd1.86pl3.tar.gz
	tar -xzf proverifdoc1.86pl3.tar.gz

This will create a directory named proverif1.86pl3 in the current directory.

* under Windows NT, 2000, or XP

Uncompress the archives proverifbsd1.86pl3.tar.gz and 
proverifdoc1.86pl3.tar.gz using Winzip, in the directory
of your choice. This will create a subdirectory named proverif1.86pl3. 


USAGE

This software contains one executable program, proverif.  It takes as
input a description of a cryptographic protocol, and checks whether it
can leak some secrets, or satisfies authenticity properties. The
description of the protocol can have two different formats. By
default, it is a description by rules of the form
	c:M1 & ... & c:Mn -> c:M
meaning if the attacker has M1, ..., Mn then it also has M. This
description corresponds to the format used internally by the program.
	By adding the command line option "-in pi", you can work with
protocols described in a language that is a restricted version of the
applied pi calculus (Abadi and Fournet, POPL'01). The description is
first translated into the above rules, and then the core of the
verifier is called.
	Examples of protocol descriptions can be found in the examples
subdirectory. Files in directory examples/horn are inputs for
proverif; files in directory examples/pi are inputs for proverif -in pi. 
For example:
	./proverif examples/horn/secr/needham
	./proverif -in pi examples/pi/secr-auth/piskeme

	The user manual can be found in the docs subdirectory. Research papers
can be downloaded on
	http://www.di.ens.fr/~blanchet/publications.html
They are not included in the distribution because of copyright differences.
(You cannot redistribute these papers.)
	The script "test" runs several tests (Unix only):

	./test secr	runs secrecy tests of the CSFW'01 paper
	./test bidsecr	similar to the previous one, but runs bidirectional
			protocols
	./test both 	runs secrecy and authenticity tests
	./test noninterf runs non-interference tests (strong secrecy)
	./test weak	runs tests on protocols using weak secrets
	./test choice	runs observational equivalence tests
	./test obsequi  runs observational equivalence tests (LICS'05 paper)
	./test attack   runs attack reconstruction test (CSFW'05 paper)
	./test jfk      runs tests on the protocol JFK (ESOP'04/TISSEC paper)
	./test mailprot runs tests on a certified email protocol (SAS'03/TCS paper)
	./test ffgg     runs tests on the f^n g^n protocol by Millen

The output of these scripts is written in the directory tests. The
filename of the output contains the argument of "test" and the
date/time of the run.

COPYRIGHT

The source package is distributed under the GNU general public license.
The binary package for Windows is distributed under BSD license.

BUG REPORTS

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

MAILING LIST

A mailing list is available for discussions on ProVerif. New releases
are announced on this mailing list.

* If you wish to subscribe, send an email to sympa@lists.ens.fr with subject
"subscribe proverif" (without quotes) and an empty body.

* To post a message on the list, send it to proverif@ens.fr. 
To avoid spam, only people that have subscribed to the list can post.

ACKNOWLEDGMENTS

I would like to thank all users of ProVerif who contributed to the
development of the software by their helpful remarks.
From July 2008 to Octobre 2010, the development of ProVerif was partly 
supported by DGA.