自動検証ツール ProVerifを導入する
インストールするのに結構時間がかかってしまったのでメモ
ProVerif とは
こちらの記事に書いてありますが，セキュリティプロトコルを形式検証するツールとなっております．
Windowsへのインストール
インストールについてはドキュメントの"Instalation"を確認するとすぐにできると思います．
ダウンロードはここからどうぞ
あとはファイルを解凍して，インストールでok
Mac OS へのインストール
本編
こちらは少し苦労したので，メモを兼ねてます．
ここでドキュメントの通りに終了すれば問題ないですが，私は
ocamlyacc command not found
ocamllex command not found
のようなエラーが出力されました．
どうやらProVerifに利用するソフトウェア群を自動インストールするためのパッケージマネージャーがインストールされていないようです．
私は"ocamllex"をインストールするだけで解決できてしまったので，
以下に方法を示します(実はここに書いてあったり..)．
ocamllex導入編
-
まずは本家からバイナリファイルをダウンロード
-
解凍&実行
$ tar -xzf ocaml-4.03.0.tar.gz
解凍後のフォルダへ移動しスクリプトを実行
$ cd ocaml-4.03.0
$ ./configure --prefix <プリフィクス>
...
$ make world.opt
...
$ make install
...
ProVerif Build編
解凍
$ 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からでもインストールできるようです．参考はこちら