はじめに
EasyCryptは暗号プロトコルや暗号技術の安全性を検証するためのツールである。この文書ではEasyCryptをmacOSへインストールするための方法について述べる。
インストール
OPAMのインストール
まずOCamlのパッケージマネージャーであるOPAMを次のようにインストールする。
$ brew install opam
opamをインストールしたあとは指示に従って、opam initやeval `opam config env`を入力する。
そして、OPAMからEasyCrypt用のOCaml環境を次のコマンドで用意する1。
$ opam switch create easycrypt 4.05.0 easycrypt
これを実行するとOCamlが環境が整う。
EasyCryptの必要要件のインストール
次にEasyCryptが必要とするパッケージをインストールする。まずはOPAMのリポジトリに追加を行うために、次のコマンドを実行する。
$ opam repository add easycrypt git://github.com/EasyCrypt/opam.git
$ opam update
そして、EasyCryptに使われる外部ソルバーを次のコマンドでインストールする。なお、SMTソルバーであるZ3のコンパイルに相当の時間がかかることに注意して欲しい。
$ opam install ec-provers
Why3の設定ファイルの作成
Why3の設定ファイルはSMTソルバーを更新したり追加した場合に作り直す必要がある。設定を作成するためには、次のコマンドを実行すればよい。
$ why3 config --detect -C ~/.why3.conf
この設定によりEasyCryptからSMTソルバーが利用できるようになる。
EasyCryptのインストール
$ opam install easycrypt
これでEasyCryptを実際に使えるようになる。
EasyCrypt用のProof Generalのインストール
EasyCryptで証明を記述したり検証する場合、EmacsのプラグインであるProof Generalのフロントエンドが用意されているので、こちらを使うとよい。まずはProof Generalを次のようにインストールする。
$ opam install proofgeneral
そしてEmacsの設定ファイルである~/.emacsまたは~/.emacs.d/init.elに次を追加する。
(load-file "<OPAM_PREFIX>/share/proofgeneral/generic/proof-site.el")
ただし、<OPAM_PREFIX>には次のコマンドで表示された場所を入力する。
$ opam config var prefix
これでEmacsが正常に起動すればインストールは終了である。
証明の検証
これでEmacsから証明を検証できるようになったので、さっそく簡単な証明を用いてテストしてみる。
type plain.
type rand.
op zero : plain.
op(+): plain -> plain -> plain.
axiom xor0p: forall (x:plain), zero + x = x.
axiom xorC (x y:plain): x + y = y + x.
axiom xorA x y z : x + (y + z) = (x + y) + z.
lemma xorp0 x : x + zero = x by smt.
これをファイルに保存して、Emacsでエラーなく開ければインストールは成功である。EasyCryptのExamplesの中から何かをダウンロードして実行してみるのもよいだろう2。
まとめ
このようにしてEasyCryptをインストールして動かしてみることができる。さらに興味がある方は文献を読むとよいかもしれない。