プロトコルの形式的安全検証ツール ProVerif を用いて、簡単なプロトコルの検証

# はじめに
Proverifとは、プロトコルを形式的に検証するツールです。プロトコルをモデル化したコードで記述して、Proverifツールで実行すると脆弱性の有無を判断してくれます。

今回はProverif2.04を用いて、簡単なプロトコルについて秘匿性、オフライン攻撃耐性、の有無を検証していきます。

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

# インストールと環境構築
インストールと環境構築の方法は以下をご覧ください。

https://qiita.com/eusk/items/e019a81dbee7b5623555

# 検証するプロトコル
以下の簡単なプロトコルで検証を行います。

![protocol1.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/3445264/64fccb3f-7c7e-1117-4092-5021ca815edf.png)



AとBからなる二者モデルであり、Aはパスワード(password)と平文(msg)、Bは(password)を保持しています。
Aが平文をパスワードを用いて暗号化して、Bに送信。
送られた暗号文をBがパスワードを用いて復号するというプロトコルです。

いわゆる、共通鍵暗号方式です。

# プロトコルのコード記述
Proverifで検証可能にするため、プロトコルをコードで記述します。
出てくるキーワードや、変数などを順に説明していきます。

## 主なキーワード
今回のコーディングの際に用いるワードを簡単にまとめます。

* ``type``：型の宣言。デフォルトではbitstringやchannelなどがある。鍵とメッセージなどを区別できるようにkey型などを作っておくと便利。
* ``free``：グローバル変数の宣言。[private]を加えると、当事者のみアクセス可能。
* ``event``：イベントの発生。プロセス内でのイベントの発生を表す。
* ``fun``：関数の宣言。入力と出力の型で宣言する。
* ``let``：変数への値の代入や、プロセスの動作を記述する。
* ``in``：チャンネルからデータを受信する。
* ``out``：チャンネルにデータを送信する。
* ``query attacker(v)``：秘匿性の検証。攻撃者が変数vに到達可能か。
* ``weaksecret v``：オフライン攻撃の検証。秘密値vのエントロピーが低い(人が覚えられる程度の文字列)とき、攻撃者が変数vに到達可能か。
* ``process``：mainプロセスの定義。
* ``!プロセス``：プロセスが繰り返し実行される。
* ``プロセスA|プロセスB``：プロセスAとプロセスBを並列に動作させる。

## 型の定義
プロトコルに必要な型をまず定義・宣言していきます。

~~~
free c: channel.             (*通信に使うチャネルを用意*)
free msg:bitstring[private]. (*平文msgを用意*)

type key.                    (*key型の宣言*)
free password: key[private]. (*key型のpassworを用意*)
~~~

まずは、通信に使うチャネルを用意します。今回は通信が1方向で1回なため、１つのチャネル。
そして、bitstring型の平文と、key型のpasswordを用意します。この２つは当事者間でのみアクセスできる **[private]** で宣言します。

## イベントの宣言
発生するイベントを宣言していきます。

~~~
event beginA(bitstring).
event endB(bitstring).
~~~
* ``biginA(bitstring).`` Aでの暗号化、送信イベントの発生を表します。
* ``endB(bitstring).`` Bで復号終了のイベントの発生を表します。

## 検証する脆弱性を記述
以下のようにして、検証する脆弱性を記述します。
~~~
query attacker(msg).
query attacker(password).
weaksecret password.
~~~
* ``query attacker(msg)``攻撃者が平文msgに到達可能か
* ``query attacker(password)``攻撃者が鍵keyに到達可能か
上記の2つが問題なかった場合、秘匿性があるということになります。

* ``weaksecret password.``passwordのエントロピーが低いとき、攻撃者がpasswordに到達可能か。
上記の``weaksecret password.``に問題がなければ、オフライン攻撃に耐性があるといえます。

## 共通鍵暗号のコード化
まず、共通鍵暗号方式とはについて、めちゃくちゃ簡単に説明します。
共通鍵暗号方式では、平文を共通の鍵を用いて暗号化します。そして、復号する際も共通の鍵を用いて復号する暗号方式です。

コードでは、暗号化、復号をこのよう定義します。
* ``enc(m,k)``：平文 m を鍵 k を用いて暗号化
* ``dec(c,k)``：暗号 m を鍵 k を用いて復号
* ``dec(enc(m,k),k) = m``：暗号化と復号で元に戻る

ProVeriのコードで記述すると以下のようになります。

~~~
fun enc(bitstring, key): bitstring.
reduc forall m: bitstring, k: key;
  dec(enc(m,k),k) = m.
~~~
* ``enc(bitstring,key)``では、bitstring型とkey型を入力として、bitstring型を出力します。
* ``dec(enc(m,k),k) = m ``では、上記で暗号化されたbitstring型の enc(bitstring,key)とkey型のkを用いて復号し、bitstring型のm出力します。

つまり、enc()で暗号化したものを同じ鍵(key)を用いてdec()で復号すれば、同一の平文が得られます。

## プロセスの記述

### Aのプロセス
まずは、Aのプロセスを記述していきます。
~~~
let A() =
  event beginA(msg);
  out(c, enc(msg,password));
  0.
~~~

``event beginA(msg)``ではイベントの発生を表します。
``out``はチャネルcを通じて msg を password で暗号化した``enc(msg,password)``をBへ送信します。

### Bのプロセス
~~~
let B() =
  in(c, x: bitstring);
  let recvmsg = dec(x,password) in
  event endB(recvmsg);
  0.
~~~
``in``でcチャネルを通じて得た値を、xに代入します。
次に``dec(x,password)``で復号した値を``recvmsg``に代入します。
``event endB(recvmsg)``でプロセス終わりのイベントの発生を表して、プロセスの記述は終わりとなります。

## メイン関数内のプロセスの記述
~~~
process
  ( (!A()) | (!B()) )
~~~
AのプロセスとBのプロセスを並列に繰り返し動作させることを表します。

# コードの全体像
以下にコードを貼っておきます。

~~~protocol.pv
free c: channel.
free msg:bitstring[private].

type key.
free password: key[private].

event beginA(bitstring).
event endB(bitstring).

query attacker(msg).
query attacker(password).
weaksecret password.

fun enc(bitstring, key): bitstring.
reduc forall m: bitstring, k: key;
  dec(enc(m,k),k) = m.

let A() =
  event beginA(msg);
  out(c, enc(msg,password));
  0.

let B() =
  in(c, x: bitstring);
  let recvmsg = dec(x,password) in
  event endB(recvmsg);
  0.

process
  ( (!A()) | (!B()) )
~~~

# コードの実行
以下のようにして、コードを実行します。
~~~shell-session
$ proverif protocol.pv
~~~

実行結果で重要な部分は Verification summary:以下の部分です。
~~~
--------------------------------------------------------------
Verification summary:

Query not attacker(msg[]) is true.

Query not attacker(password[]) is true.

Weak secret password is false.
--------------------------------------------------------------
~~~

* ``Query not attacker(msg[]) is true.`` trueなため、攻撃者はmsgには到達できなかったことが分かります。
* ``Query not attacker(password[]) is true.``trueなため、攻撃者はpasswordには到達できなかったことが分かります。

つまり、攻撃者はmsgとpasswordに到達不可能であり、このプロトコルは秘匿性があるといえます。

* ``Weak secret password is false.``こちらは、falseなためオフライン攻撃の耐性はないということになります。

検証の結果は以下の通りです。
* 秘匿性：〇
* オフライン攻撃：×

# まとめ
今回は簡単なプロトコルについて、秘匿性の有無と、オフライン攻撃に対しての耐性を検証しました。

Proverifの簡単なプロトコルの検証でしたが、結構苦戦しましたので皆様のご参考になれば幸いです。
今後はより実用的なプロトコルや、他の脆弱性につていの検証なども記事にまとめていければなーと思います。

ご意見、ご指摘等あれば、コメントしていただけると幸いです。

# 参考資料
[プロトコルの形式的安全検証ツール ProVerif](https://speakerdeck.com/tex2e/proverif)

[ProVerifによるWPA3プロトコルの検証 | 晴耕雨読](https://tex2e.github.io/blog/crypto/proverif-wpa2-and-wpa3)