ProVerif is compatible with the Linux, Mac, and Windows operating systems; it can be downloadedfrom:
The remainder of this section covers installation on Linux,Mac, and Windows platforms.
ProVerif has been developed using Objective Caml (OCaml) and OPAM is the package manager ofOCaml. Installing via OPAM is the simplest, especially if you already have OPAM installed.
If you do not already have OPAM installed, download it from
and install it.
brew install opam
If you already have OPAM installed, run
Opam has not been initialised, please run `opam init’
to make sure that you get the latest version of ProVerif.
opam depext conf-graphviz
The first line installs graphviz, if you do not already have it. You may also install it using thepackage manager of your Linux, OSX, or cygwin distribution,especially if opam fails to install it.It is needed only for the graphical display of attacks.
The second line installs
GTK+2 including development libraries, if you do not already have it. You mayalso install it using the packagemanager of your distribution. It is needed for the interactive simulatorproverifinteract. 【 [见问题处理] (#problem) 】
Thethird line installs ProVerif itself and its OCaml dependencies. ProVerif executables are in~/.opam/〈switch〉/bin, which is in thePATH, examples are in~/.opam/〈switch〉/doc/proverif, andvarious helper files are in~/.opam/〈switch〉/share/proverif. The directory〈switch〉is the opamswitch in which you installed ProVerif, by defaultsystem.
GTK version 2+
brew install pkg-config