1
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

More than 1 year has passed since last update.

プロトコルの形式的安全検証ツールProVerif -インストール-(windows11)

Last updated at Posted at 2023-05-22

はじめに

Proverifとは、プロトコルを形式的に検証するツールです。プロトコルをモデル化したコードで記述して、Proverifツールで実行すると脆弱性の有無を判断してくれます。
主に、秘匿性や、前方秘匿性、オフライン攻撃、到達可能性など、種々の脆弱性を形式的に検証することができます。

プロトコルの検証に関して、初心者です。備忘録を兼ねておりますので、間違い等ございましたらご指摘ください。

インストール(windows11)

下記のサイトからダウンロードすることができます。
https://bblanche.gitlabpages.inria.fr/proverif/

サイトに飛んだら、DownloadsProVerif 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)... をクリック。

環境変数.png

ユーザー環境変数 or システム環境変数のPATH(Path,pathなど)をクリックし、さらに編集をクリック。PATHの変数がない場合は新規をクリック。
pathの通し方.png

編集をクリックしたら新規をクリック、
入力欄が出てきたら
C:proverif\proverif2.04
と入力し、OKをクリック。

pathの通し方2.png

適当なフォルダでコマンドプロンプトを開いて以下のように入力。

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

最後に

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

参考文献

1
0
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
1
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?