暗号系の安全性検証ツール“EasyCrypt”の導入法
はじめに
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をインストールして動かしてみることができる。さらに興味がある方は文献を読むとよいかもしれない。
文献
Author And Source
この問題について(暗号系の安全性検証ツール“EasyCrypt”の導入法), 我々は、より多くの情報をここで見つけました https://qiita.com/yyu/items/2634c5e053f4b419945e著者帰属:元の著者の情報は、元のURLに含まれています。著作権は原作者に属する。
Content is automatically searched and collected through network algorithms . If there is a violation . Please contact us . We will adjust (correct author information ,or delete content ) as soon as possible .