Edited at

Proverifを導入(MacとWindows編)

More than 1 year has passed since last update.


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

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


ProVerif とは

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


Windowsへのインストール

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

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

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


Mac OS へのインストール

本編

ドキュメント

こちらは少し苦労したので,メモを兼ねてます.

ここでドキュメントの通りに終了すれば問題ないですが,私は

ocamlyacc command not found

ocamllex command not found

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

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

私は"ocamllex"をインストールするだけで解決できてしまったので,

以下に方法を示します(実はここに書いてあったり..).


ocamllex導入編


  1. まずは本家からバイナリファイルをダウンロード


  2. 解凍&実行


$ 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からでもインストールできるようです.参考はこちら


Ubuntu 編

ここ