Limited Entropy Dot Com Not so random thoughts on security featured by Eloi Sanfèlix

ProVerif bajo Mac OS X ( ProVerif under Mac OS X )

Note: You can find an english version of these instructions in the extended version of this entry, by clicking on 'Lee el resto de esta entrada'.

Escribo esta rápida nota sobre cómo instalar ProVerif en Mac OS X entre otras cosas porque he visto que alguien andaba buscando instrucciones. ProVerif es una utilidad para verificar protocolos criptográficos basada en el uso de spi-calculus y cláusulas de Horn, en la que se especifica un modelo del protocolo criptográfico y las metas del mismo ( s es secreto, o se ha autenticado A con B, ...).

Para instalarlo en Mac OS X lo primero que necesitamos es Ocaml. Vamos a download y bajamos el código fuente. Una vez hecho la instalación se resume en lo siguiente (tras haber descomprimido el tar.gz del código fuente):

$ cd ocaml-3.10.2
$ ./configure
$ ls
$ make world
$ make opt
$ sudo make install


El siguiente paso es situarse en la carpeta de ProVerif y ejecutar el archivo build:

$ cd ../proverif1.14pl4
$ ls
$ ./build

Si no obtienes ningún error, ya tienes compilado ProVerif. Puedes comprobar que funciona utilizando la utilidad analyzer con alguno de los ejemplos en examples:

$ ./analyzer examples/auth/needham
[... output omitted]
RESULT goal reachable: end:x_6,y_7


Y para aprender sobre ProVerif puedes mirar las transparencias de la asignatura Verification Of Security Protocols.

[ENGLISH VERSION]

I'm writing this quick note about how to install ProVerif on Mac OS X because I saw someone looking for it in the stats. ProVerif is a cryptographic protocol' verification tool based on the spi-calculus and Horn clauses, where one specifies a model of the protocol and its goals ( such as secrecy of s, authentication of A against B, ...).

In order to install it on OS X, we first need Ocaml. Let's go to download and download its source code. After that, the installation reduces to these commands (after uncompressing the tarball with the source):

$ cd ocaml-3.10.2
$ ./configure
$ ls
$ make world
$ make opt
$ sudo make install

Next step is going into ProVerif's directory and execute the build tool:

$ cd ../proverif1.14pl4
$ ls
$ ./build


If no errors are returned, you have compiled ProVerif successfully. You can check it is working by means of the analyzer tool with any of the examples under examples:

$ ./analyzer examples/auth/needham
[... output omitted]
RESULT goal reachable: end:x_6,y_7

And for learning about ProVerif you can take a look at the slides of the Verification Of Security Protocols subject.