はじめに

EasyCryptは暗号プロトコルや暗号技術の安全性を検証するためのツールである。この文書ではEasyCryptをmacOSへインストールするための方法について述べる。

インストール

OPAMのインストール

まずOCamlのパッケージマネージャーであるOPAMを次のようにインストールする。

$ brew install opam

opamをインストールしたあとは指示に従って、opam initやeval `opam config env` を入力する。
そして、OPAMからEasyCrypt用のOCaml環境を次のコマンドで用意する¹。

$ 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に次を追加する。

init.el

(load-file "<OPAM_PREFIX>/share/proofgeneral/generic/proof-site.el")

ただし、<OPAM_PREFIX>には次のコマンドで表示された場所を入力する。

$ opam config var prefix

これでEmacsが正常に起動すればインストールは終了である。

証明の検証

これでEmacsから証明を検証できるようになったので、さっそく簡単な証明を用いてテストしてみる。

test.ec

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の中から何かをダウンロードして実行してみるのもよいだろう²。

まとめ

このようにしてEasyCryptをインストールして動かしてみることができる。さらに興味がある方は文献を読むとよいかもしれない。

文献

最新のOCamlは4.04であるが、EasyCryptのREADMEには4.02系が書かれているので、念のため4.02系の最新を選んだ。 ↩
EasyCryptのExampleの中にはFMapを用いているものがあるが、これをSmtMapに書き換えないと正しく検証できない。 ↩