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

# はじめに
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)...** をクリック。 

![環境変数.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/3445264/9a553f67-a508-22ef-9c91-108eba62b2ba.png)

ユーザー環境変数 or システム環境変数のPATH(Path,pathなど)をクリックし、さらに編集をクリック。PATHの変数がない場合は新規をクリック。
![pathの通し方.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/3445264/caa470cc-71ef-e343-45d0-0e740daeee9b.png)


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


![pathの通し方2.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/3445264/ae56786a-177e-16de-e00d-d4613426dd6f.png)

適当なフォルダでコマンドプロンプトを開いて以下のように入力。
~~~shell-session
$ 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
```
そのフォルダ内でコマンドプロンプトを開き、以下を入力。

~~~shell-session
$ proverif hello.pv
~~~

以下のような出力が得られればOK。

~~~shell-session
Process 0 (that is, the initial process):
{1}out(c, RSA)


--------------------------------------------------------------
Verification summary:

No query in the input file.
--------------------------------------------------------------
~~~

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

# 参考文献
* [Proverif User Manual](https://bblanche.gitlabpages.inria.fr/proverif/manual.pdf "ProverifUserManual")