Difference between revisions of "CryptoVerif Installation"

From prosecco
m (Prerequisites: emacs)
Line 1: Line 1:
Instructions for installing [http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif].
+
Instructions for installing [http://cryptoverif.inria.fr/ CryptoVerif].
 
 
== Prerequisites ==
 
 
 
(CH: It would be great if these prerequisites would be only for building from sources, while the binary packages would include their dependencies)
 
 
 
* [http://caml.inria.fr OCaml version 3.00] or higher.
 
 
 
(CH: This is a prerequisite only when building from source, right? Is there any way to do this without building things from sources (e.g. on Windows)?)
 
 
 
(CH: TODO: separate instructions for OCaml, shared between the three tools)
 
 
 
* [http://forge.ocamlcore.org/projects/cryptokit/ The cryptokit OCaml cryptographic library, version 1.9] (CH: right?)(CH: Is this required or optional?)
 
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
 
so that the cryptokit library is included.
 
 
 
(CH: Can we make this easier? Can we automate it with a script? Also, people using opam can just do `opam install cryptokit`)
 
 
 
* (CH: Cygwin for Windows)
 
 
 
(CH: If any of the other tools needs Cygwin to run on Windows, we could link to the Cygwin installation instructions, and mention explicitly which packages our tools we depend on: make, etc)
 
 
 
* Emacs (CH: it seems it's already a dependency for the EasyCrypt part: https://www.easycrypt.info/trac/browser/README?rev=1.0)
 
  
 
= Installing the binary package (Windows) =
 
= Installing the binary package (Windows) =
  
 
On Windows, the recommended way is to use the precompiled binaries, available as a separate distribution.
 
On Windows, the recommended way is to use the precompiled binaries, available as a separate distribution.
[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/cryptoverifbin1.19.tar.gz]
+
[http://cryptoverif.inria.fr/cryptoverifbin.html]
  
(CH: Any chance for a zip archive of this? Windows people don't usually use tar gz?)
+
= Building from Source (Linux, Mac, Windows with Cygwin) =
  
(CH: How about including a cryptokit binary in this release, so that people can use this out of the box?)
+
Prerequisite : [http://caml.inria.fr OCaml version 3.00] or higher.
 
 
(CH: It would be too hard to provide binaries for other platforms?)
 
 
 
= Building from Source (Linux, Mac, Windows with Cygwin) =
 
  
 
Download CryptoVerif sources:
 
Download CryptoVerif sources:
  
   wget http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/cryptoverif1.19.tar.gz
+
   wget http://cryptoverif.inria.fr/cryptoverif1.19.tar.gz
  
 
Uncompress the archive using tar:
 
Uncompress the archive using tar:
Line 66: Line 28:
 
   cd cryptoverif1.19
 
   cd cryptoverif1.19
 
   ./build
 
   ./build
 +
 +
= Optional =
 +
 +
* You will need a text editor to type examples. Any text editor is ok. If you happen to use emacs, there is an emacs mode for CryptoVerif that will give you syntax coloring. To install it:
 +
 +
1. Copy the file cryptoverif1.19/emacs/cryptoverif.el of the CryptoVerif distribution to a directory where Emacs will find it (that is, in your emacs load-path)
 +
 +
2. Add the following lines to your .emacs file:
 +
 +
        (setq auto-mode-alist
 +
              (cons '("\\.cv[l]?$" . cryptoverif-mode)
 +
              (cons '("\\.ocv[l]?$" . cryptoverifo-mode) auto-mode-alist)))
 +
        (autoload 'cryptoverif-mode "cryptoverif" "Major mode for editing CryptoVerif code." t)
 +
        (autoload 'cryptoverifo-mode "cryptoverif" "Major mode for editing CryptoVerif code." t)
 +
 +
* You will need a shell to run CryptoVerif. Under Windows, you may use the Windows command line, although there are better shells, such as the cygwin terminal if you use cygwin. Under Unix, the terminal is fine.
 +
 +
* If you want to run protocol implementations generated by CryptoVerif (which will not be required during the school), you need to install [http://forge.ocamlcore.org/projects/cryptokit/ The cryptokit OCaml cryptographic library, version 1.9]
 +
This library is available at
 +
  http://forge.ocamlcore.org/projects/cryptokit/
 +
For opam users, you can install it just by running "opam install 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
 +
so that the cryptokit library is included.
  
 
= Frequently asked questions =
 
= Frequently asked questions =
Line 71: Line 64:
 
= License =
 
= License =
  
The CryptoVerif cryptographic protocol verifier, version 1.19 is copyright ENS, CNRS, INRIA, by Bruno Blanchet and David Cadé, 2005-2014. It is released under the terms of [http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/cryptoverif.html the CeCILL-B license]. (The CeCILL-B license is a BSD-style license. See the file LICENSE for more information.)
+
The CryptoVerif cryptographic protocol verifier, version 1.19 is copyright ENS, CNRS, INRIA, by Bruno Blanchet and David Cadé, 2005-2014. It is released under the terms of [http://cryptoverif.inria.fr/cryptoverif.html the CeCILL-B license]. (The CeCILL-B license is a BSD-style license. See the file LICENSE for more information.)

Revision as of 13:47, 4 November 2014

Instructions for installing CryptoVerif.

Installing the binary package (Windows)

On Windows, the recommended way is to use the precompiled binaries, available as a separate distribution. [1]

Building from Source (Linux, Mac, Windows with Cygwin)

Prerequisite : OCaml version 3.00 or higher.

Download CryptoVerif sources:

 wget http://cryptoverif.inria.fr/cryptoverif1.19.tar.gz

Uncompress the archive using tar:

 gunzip cryptoverif1.19.tar.gz
 tar -xf cryptoverif1.19.tar

or if you have GNU tar:

 tar -xzf cryptoverif1.19.tar.gz

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

 cd cryptoverif1.19
 ./build

Optional

  • You will need a text editor to type examples. Any text editor is ok. If you happen to use emacs, there is an emacs mode for CryptoVerif that will give you syntax coloring. To install it:

1. Copy the file cryptoverif1.19/emacs/cryptoverif.el of the CryptoVerif distribution to a directory where Emacs will find it (that is, in your emacs load-path)

2. Add the following lines to your .emacs file:

       (setq auto-mode-alist
             (cons '("\\.cv[l]?$" . cryptoverif-mode) 
             (cons '("\\.ocv[l]?$" . cryptoverifo-mode) auto-mode-alist)))
       (autoload 'cryptoverif-mode "cryptoverif" "Major mode for editing CryptoVerif code." t)
       (autoload 'cryptoverifo-mode "cryptoverif" "Major mode for editing CryptoVerif code." t)
  • You will need a shell to run CryptoVerif. Under Windows, you may use the Windows command line, although there are better shells, such as the cygwin terminal if you use cygwin. Under Unix, the terminal is fine.

This library is available at

 http://forge.ocamlcore.org/projects/cryptokit/

For opam users, you can install it just by running "opam install 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 so that the cryptokit library is included.

Frequently asked questions

License

The CryptoVerif cryptographic protocol verifier, version 1.19 is copyright ENS, CNRS, INRIA, by Bruno Blanchet and David Cadé, 2005-2014. It is released under the terms of the CeCILL-B license. (The CeCILL-B license is a BSD-style license. See the file LICENSE for more information.)