自動検証ツール ProVerifを導入する

インストールするのに結構時間がかかってしまったのでメモ

ProVerif とは

こちらの記事に書いてありますが，セキュリティプロトコルを形式検証するツールとなっております．

インストールについてはドキュメントの"Instalation"を確認するとすぐにできると思います．

ダウンロードはここからどうぞ

あとはファイルを解凍して，インストールでok

本編

こちらは少し苦労したので，メモを兼ねてます．
ここでドキュメントの通りに終了すれば問題ないですが，私は

ocamlyacc command not found
ocamllex command not found

のようなエラーが出力されました．

どうやらProVerifに利用するソフトウェア群を自動インストールするためのパッケージマネージャーがインストールされていないようです．

私は"ocamllex"をインストールするだけで解決できてしまったので，
以下に方法を示します(実はここに書いてあったり..)．

$ tar -xzf ocaml-4.03.0.tar.gz

解凍後のフォルダへ移動しスクリプトを実行

$ cd ocaml-4.03.0
$ ./configure --prefix <プリフィクス> 
...
$ make world.opt
...
$ make install
...

解凍

$ tar -xzf proverif1.96.tar.gz

Build

$ cd proverif1.96
$ ./build

実行

サンプルファイルとして，hello.pvを作成します．

free c : ch annel .
free Cocks : b i t s t r i n g [private ] .
free RSA: b i t s t r i n g [ private ] .

process
out ( c ,RSA ) ;
0

proverifで実行

$ proverif hello.pv

以上!
あとはお好みでPATH通しましょう!

ocamllexはhomebrewからでもインストールできるようです．参考はこちら