Difference between revisions of "CryptoVerif Installation"
m (→Building from Source (Linux, Mac, Windows with Cygwin)) |
|||
| (4 intermediate revisions by one other user not shown) | |||
| Line 9: | Line 9: | ||
= Building from Source (Linux, Mac, Windows with Cygwin) = | = Building from Source (Linux, Mac, Windows with Cygwin) = | ||
| − | Prerequisite : [http://caml.inria.fr OCaml] version 3.00 or higher. If you don't have | + | Prerequisite : [http://caml.inria.fr OCaml] version 3.00 or higher. If you don't have OCaml installed already we recommend installing a "modern" version such as 4.01 or 4.02. |
Download CryptoVerif sources: | Download CryptoVerif sources: | ||
| Line 34: | Line 34: | ||
=== Text editor: Emacs mode for CryptoVerif === | === Text editor: Emacs mode for CryptoVerif === | ||
| − | You will need a text editor to type examples. Any text editor is ok. If you happen to use | + | 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: |
| − | # Copy the file cryptoverif1.19/emacs/cryptoverif.el of the CryptoVerif distribution to a directory where Emacs will find it (that is, in your | + | # 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) |
# Add the following lines to your .emacs file: | # Add the following lines to your .emacs file: | ||
| Line 44: | Line 44: | ||
(autoload 'cryptoverif-mode "cryptoverif" "Major mode for editing CryptoVerif code." t) | (autoload 'cryptoverif-mode "cryptoverif" "Major mode for editing CryptoVerif code." t) | ||
(autoload 'cryptoverifo-mode "cryptoverif" "Major mode for editing CryptoVerif code." t) | (autoload 'cryptoverifo-mode "cryptoverif" "Major mode for editing CryptoVerif code." t) | ||
| + | |||
| + | '''Note''': On Windows and Mac the [https://www.easycrypt.info/trac/wiki/SchoolParis14Install EasyCrypt binary packages] come with Emacs; if you don't have Emacs already installed you can just use that. | ||
=== Shell === | === Shell === | ||
| Line 69: | Line 71: | ||
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.) | 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.) | ||
| + | |||
| + | = Teaching material = | ||
| + | |||
| + | [http://prosecco.gforge.inria.fr/personal/bblanche/talks/CV-School14-Wednesday.pdf General introductory talk] | ||
| + | |||
| + | [http://prosecco.gforge.inria.fr/personal/bblanche/talks/CV-School14-Course.pdf Course] | ||
| + | |||
| + | [http://prosecco.gforge.inria.fr/personal/bblanche/talks/CV-School14-Tutorial.pdf Tutorial] | ||
| + | |||
| + | [http://prosecco.gforge.inria.fr/personal/bblanche/talks/CV-School14-enc-then-MAC.cv enc-then-MAC.cv] | ||
| + | |||
| + | [http://prosecco.gforge.inria.fr/personal/bblanche/talks/CV-School14-FDH.cv FDH.cv] | ||
Latest revision as of 10:05, 25 November 2014
Instructions for installing CryptoVerif.
Contents
Installing the binary package (Windows)
On Windows, the recommended way is to use the precompiled binaries here. After accepting the license twice, you will download a file named cryptoverifbin1.19.zip. Uncompress this file in the directory of your choice. This will create a subdirectory named cryptoverif1.19.
Building from Source (Linux, Mac, Windows with Cygwin)
Prerequisite : OCaml version 3.00 or higher. If you don't have OCaml installed already we recommend installing a "modern" version such as 4.01 or 4.02.
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
Text editor: Emacs mode for CryptoVerif
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:
- 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)
- 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)
Note: On Windows and Mac the EasyCrypt binary packages come with Emacs; if you don't have Emacs already installed you can just use that.
Shell
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.
Cryptokit
If you want to run protocol implementations generated by CryptoVerif (which will not be required during the school), you need to install the OCaml cryptographic library Cryptokit, 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". Others should follow the installation instructions provided with the library. Additionally, 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.
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.)
