はじめに

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.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.
--------------------------------------------------------------

最後に

グラフ描画や、エディタなど様々な拡張機能があるようです。
次回の記事では、簡単なプロトコルを例にプログラムの記述の仕方を
投稿する予定です。
ご意見、ご指摘等あれば、コメントしていただけると幸いです。

参考文献

Proverif User Manual