はじめに
Proverifとは、プロトコルを形式的に検証するツールです。プロトコルをモデル化したコードで記述して、Proverifツールで実行すると脆弱性の有無を判断してくれます。
主に、秘匿性や、前方秘匿性、オフライン攻撃、到達可能性など、種々の脆弱性を形式的に検証することができます。
プロトコルの検証に関して、初心者です。備忘録を兼ねておりますので、間違い等ございましたらご指摘ください。
インストール(windows11)
下記のサイトからダウンロードすることができます。
https://bblanche.gitlabpages.inria.fr/proverif/
サイトに飛んだら、Downloads の ProVerif version 2.04,for Windows
をダウンロード。(2023/05/22現在、version 2.04)
proverifbin2.04.tar.gz をダウンロード出来たら、7.zipなどで解凍。
proverif2.04 のファイルができればOK。
Cドライブ直下にproverifというフォルダを作成。
その中にproverif2.04をコピペ。
パスを通す
windowsの検索ボックスにシステム環境変数と入力し、システム環境変数の編集 をクリック。
システムのプロパティから 環境変数(N)... をクリック。
ユーザー環境変数 or システム環境変数のPATH(Path,pathなど)をクリックし、さらに編集をクリック。PATHの変数がない場合は新規をクリック。
編集をクリックしたら新規をクリック、
入力欄が出てきたら
C:proverif\proverif2.04
と入力し、OKをクリック。
適当なフォルダでコマンドプロンプトを開いて以下のように入力。
$ proverif -help
以下のようにオプションが表示されればOK。
Proverif 2.04. Cryptographic protocol verifier, by Bruno Blanchet, Vincent Cheval, and Marc Sylvestre
-test display a bit more information for debugging
-in <format> choose the input format (horn, horntype, spass, pi, pitype)
-out <format> choose the output format (solve, spass)
-o <filename> choose the output file name (for spass output)
-lib <filename> choose the library file (for pitype front-end only)
-set <param> <value> equivalent to adding set <param> = <value> to the input file
-TulaFale <version> indicate the version of TulaFale when ProVerif is used inside TulaFale
-graph create the trace graph from the dot file in the directory specified
-commandLineGraph Define the command for the creation of the graph trace from the dot file
-gc display gc statistics
-color use ANSI color codes
-html HTML display
-help Display this list of options
--help Display this list of options
サンプルプログラムを動かす
今回は環境構築ができたかどうかの確認のため User manual 内にあるhello.pvを動かします。
メモ帳を開いて以下のプログラムを入力、拡張子をpvで保存。
(* hello.pv: Hello World Script *)
free c:channel.
free Cocks:bitstring [private].
free RSA:bitstring [private].
process
out(c,RSA);
0
そのフォルダ内でコマンドプロンプトを開き、以下を入力。
$ proverif hello.pv
以下のような出力が得られればOK。
Process 0 (that is, the initial process):
{1}out(c, RSA)
--------------------------------------------------------------
Verification summary:
No query in the input file.
--------------------------------------------------------------
最後に
グラフ描画や、エディタなど様々な拡張機能があるようです。
次回の記事では、簡単なプロトコルを例にプログラムの記述の仕方を
投稿する予定です。
ご意見、ご指摘等あれば、コメントしていただけると幸いです。