セキュリティプロトコルの形式検証ツール“ProVerif”

# はじめに

**ProVerif**とは、INRIAが開発したセキュリティプロトコルを形式検証するツールである。この記事ではProVerifによるプロトコルの形式検証のやり方の基礎を解説する。なお、この記事では2015年10月時点での最新版であるProVerif 1.91について解説する。
この文章を読んで何か気がついたことがあったら、コメントなどで気軽に指摘して欲しい。

# インストールと入手

次のようにインストールできる。また、現在はEmacs用のモードが提供されているので、Emacsも併せてインストールするといいかもしれない[^emacs]。

[^emacs]: Emacsでなくとも、テキストエディタであればなんでも問題はない。

## OS X

```console
$ brew tap homebrew/science/proverif
$ brew install proverif
```

## その他のOS

下記のサイトからソースコードをダウンロードしてコンパイルする。

- http://prosecco.gforge.inria.fr/personal/bblanche/proverif/

詳しいインストール方法については、公式の[マニュアル](http://prosecco.gforge.inria.fr/personal/bblanche/proverif/manual.pdf)に書かれている。

# Hello World

それでは早速ProVerifによる検証を行ってみる。次のようなファイルを作成する。

```proverif:hello_world.pv
free c:channel.

free Cocks:bitstring [private].
free RSA:bitstring [private].

process
  out(c, RSA);
  0
```

これを次のように実行する。

```console
$ proverif -color hello_world.pv
Process:
{1}out(c, RSA)
```

このような出力が得られたらインストールの成功である。

# JK・おっさんプロトコルの検証

ここではProVerifの練習として、[JK・おっさんプロトコル](http://qiita.com/yyu/private/b4a9db1a2b2cd3dfb193)を検証してみる。プロトコルの流れを引用すると次のようになる。

> # 高校生判定プロトコル
>
> 1. `おっさん`は自分が **信頼できる** カラオケ・理髪店・映画館をいくつかピックアップして、そのリストを`JK`へ渡す
> 2. `JK`は（1）で受け取ったリストの中から **信頼できる** お店を一つ選択する（もし信頼できるお店がリストにない場合は、`おっさん`がお店のリストを作り直す）
> 3. `おっさん`と`JK`は（2）で指定したお店で待合せをして、`JK`はそのお店を **高校生の価格** で利用する（その際に学生証などを提示するが、`おっさん`は少し離れた場所に待機してもらい、学生証が店員にしか見えないようにする）
> 4. `JK`はお店を高校生の価格で利用したことを示す証拠（レシートなど）を`おっさん`に提示する
> 5. `おっさん`は（4）の証拠を確認する（レシートの日付けなど）

これをProVerifへ翻訳すると、どのようになるだろうか。

## 型の定義

JK・おっさんプロトコルには出てくる概念を、Proverifの**型**として考える。ここでの型という言葉は、一般的なプログラム言語の型と同じと考えてよい。JK・おっさんプロトコルに登場するのは次のような型である。

<dl>
  <dt>お金</dt>
  <dd>支払いで暗黙的に登場</dd>
  <dt>レシート</dt>
  <dd>支払いの結果を証明する書類として登場</dd>
  <dt><code>JK</code>の身分証明書<dt>
  <dd><code>JK</code>が店員に身分を証明するために登場</dd>
</dl>

これを次のようにProverifで定義する。

```proverif
type Money.
type Receipt.
type Id.
```

## 通信経路と`JK`の身分証明書の定義

### 通信経路（チャンネル）の定義

このプロトコルでは次のような通信が発生する。

- `JK`から`おっさん`
- `おっさん`から`JK`
- `JK`から店員
- 店員から`JK`

この通信経路を、Proverifでは`channnel`という型を持つ変数として次のように定義する[^ma]。

[^ma]: ここで`ma`とは**M**iddle **A**geのことで、`おっさん`を指す。

```
free jkToMa:channel [private].
free maToJk:channel [private].
free jkToClerk:channel [private].
free clerkToJk:channel [private].
```

ここで`private`とは、この通信経路を傍受・改竄などする攻撃者がいないことを表している。今回のプロトコルでは`JK`と`おっさん`の間、また`JK`と店員の間の通信経路は安全であると仮定しているので、このようにする。

### `JK`の偽造された身分証明書

今回は単純のため「偽造された身分証明書」というものを一枚だけ定義して、それ以外のものは全て「`JK`の身分証明書」であるという定義とすることにした。`JK`の身分証明書は次のように定義する。

```proverif
free ngId:Id.
```

## レシートの定義とレシートの生成関数の定義

レシートは、`JK`が本当に`JK`の身分証明書を持っているかどうかに応じて店員が発行する書類であるまた、レシートを発行するにあたっては当然何か売買があるはずなので、お金も必要である。お金と身分証明証でレシートを発行する関数を次のように定義する。

```proverif
fun makeReceipt(Id, Money): Receipt.
```

さて、`おっさん`はレシートを生成するために使われたお金の情報をレシートから取得できる必要がある。ただし、レシートから身分証明書の情報を入手できてはならない。それは「書き換え」として次のように定義できる。

```proverif
reduc forall id:Id, m:Money; showReceipt(makeReceipt(id, m)) = m.
```

これは、全ての身分証明書`id`と全てのお金`m`について、`makeReceipt`で生成したレシートを`showReceipt`に適用した結果はお金`m`と等しくなることを意味する。

## `JK`と`おっさん`を表わすサブプロセス

ProVerifではいくつかの**プロセス**が並列に計算を進めていき、その過程でプロセスは他のプロセスへメッセージを送信したり、メッセージを受信したりする。ここでは`JK`と`おっさん`をそれぞれプロセス`jk`と`middleAge`というプロセスとし、これらが並列実行させる。
例えば、まず「`JK`が`おっさん`からお金を貰う」という様子をモデル化すると、次のようになる。

```proverif
let jk() =
  in(maToJk, money:Money).

let middleAge() =
  new money:Money;
  out(maToJk, money).

process
  ( jk() | middleAge() )
```

まず、サブプロセス[^subprocess]`jk`は通信経路（チャンネル）`maToJk`に対する型`Money`の入力を待機する。そして、サブプロセス`middleAge`は型`Money`の変数`money`を生成し、通信経路`maToJk`に`money`を送信する。最後の`process`の部分は、二つのサブプロセスを並列実行させるという意味である。

[^subprocess]: ここでは最終的なプロセスの一部という意味で「サブプロセス」という言葉を用いている。

## イベントとクエリー

ProVerifには**イベント**というものがあり、これにより例えば「イベント$e$が発生したならば、その前にイベント$e'$が発生している」といった**クエリー**（仕様）を書くことができる。
例えば次のようなイベントを定義することにする。

- `おっさん`がお金を送った
- `JK`がお金を受け取った

これらを表すイベントを次のように書く。

```proverif
event getMoneyFromMa(Money).
event sendMoneyToJk(Money).
```

これらを用いて、先ほどの例に次のようなイベントを加える。

```proverif
let jk() =
  in(maToJk, money:Money);
  event getMoneyFromMa(money);

let middleAge() =
  new money:Money;
  event sendMoneyToJk(money);
  out(maToJk, money).

process
  ( jk() | middleAge() )
```

そして、これらのイベントの間にある関係を考えると、明らかに次のことが成り立つはずである。

- `JK`がお金を受け取るイベントが発生したならば、その前に`おっさん`がお金を送った

これはProVerifで次のように書ける。

```proverif
query m:Money; event(getMoneyFromMa(m)) ==> event(sendMoneyToJk(m)).
```

あとはひたすら、残りの通信をProVerifへ翻訳すればよい。

## 検査

全てをProVerifへ翻訳すると、例えば次のようになる[^ex_mark]。

```proverif:jk.pv
type Money.
type Receipt.
type Id.

free jkToMa:channel [private].
free maToJk:channel [private].
free jkToClerk:channel [private].
free clerkToJk:channel [private].

free ngId:Id.

fun makeReceipt(Id, Money): Receipt [private].

reduc forall id:Id, m:Money; showReceipt(makeReceipt(id, m)) = m.

event getMoneyFromMa(Money).
event sendMoneyToClerk(Money).
event failReceipt(Receipt).
event getReceiptFromClerk(Id, Receipt).
event sendMoneyToJk(Money).
event giveMoneyFromJk(Id, Money).
event getReceiptFromJk(Receipt).
event sendReceiptToJk(Id, Receipt).

let jk(jkId:Id) =
  in(maToJk, money:Money);
  event getMoneyFromMa(money);
  out(jkToClerk, (jkId, money));
  event sendMoneyToClerk(money);
  in(clerkToJk, r:Receipt);
  event getReceiptFromClerk(jkId, r);
  out(jkToMa, r).

let middleAge() =
  new money:Money;
  event sendMoneyToJk(money);
  out(maToJk, money);
  in(jkToMa, r:Receipt);
  event getReceiptFromJk(r);
  if showReceipt(r) <> money then 
    event failReceipt(r).

let shopClerk() =
  in(jkToClerk, (id:Id, money:Money));
  event giveMoneyFromJk(id, money);
  if id = ngId then
    let r = makeReceipt(id, money) in
    event sendReceiptToJk(id, r);
    out(clerkToJk, r)
  else
    new ngReceipt:Receipt;
    out(clerkToJk, ngReceipt).

query r:Receipt; event(failReceipt(r)).
query m:Money; event(getMoneyFromMa(m)) ==> event(sendMoneyToJk(m)).
query id:Id, r:Receipt; event(getReceiptFromClerk(id, r)) ==> event(sendReceiptToJk(id, r)).
query id:Id, r:Receipt; event(getReceiptFromJk(r)) ==> event(getReceiptFromClerk(id, r)).

process
  new jkId:Id;
  ( jk(jkId) | middleAge() | !shopClerk() )
```

[^ex_mark]: `shopClerk`についている`!`は、ここでは複数の店員がいるということを表現していると考えればよい。

検証している性質は次の通りである。

- `failReceipt`（レシートが不正である）が発生するかどうか
- `getMoneyFromMa(m)`（お金`m`を`JK`が受け取った）ならば、その前に`sendMoneyToJk(m)`（お金`m`を`JK`へ送った）
- `getReceiptFromClerk(id, r)`（店員から身分証明書`id`に対するレシート`r`を受け取った）ならば、その前に`sendReceiptToJk(id, r)`（`JK`へ身分証明書`id`に対応するレシート`r`を送った）
- `getReceiptFromJk(r)`（レシート`r`を`JK`から受け取った）ならば、その前に`getReceiptFromClerk(id, r)`（店員からレシート`r`を受け取った）

## 実行結果

上記のコードを次のように実行する。

```console
$ proverif -color jk.pv
```

すると、次のような出力が得られる。

```
Process:
{1}new jkId: Id;
(
    {2}in(maToJk, money: Money);
    {3}event getMoneyFromMa(money);
    {4}out(jkToClerk, (jkId,money));
    {5}event sendMoneyToClerk(money);
    {6}in(clerkToJk, r: Receipt);
    {7}event getReceiptFromClerk(jkId,r);
    {8}out(jkToMa, r)
) | (
    {9}new money_28: Money;
    {10}event sendMoneyToJk(money_28);
    {11}out(maToJk, money_28);
    {12}in(jkToMa, r_29: Receipt);
    {13}event getReceiptFromJk(r_29);
    {14}if (showReceipt(r_29) <> money_28) then
    {15}event failReceipt(r_29)
) | (
    {16}!
    {17}in(jkToClerk, (id_30: Id,money_31: Money));
    {18}event giveMoneyFromJk(id_30,money_31);
    {19}if (id_30 = ngId) then
    {20}let r_32: Receipt = makeReceipt(id_30,money_31) in
        {21}event sendReceiptToJk(id_30,r_32);
        {22}out(clerkToJk, r_32)
    else
        {23}new ngReceipt: Receipt;
        {24}out(clerkToJk, ngReceipt)
)

-- Query event(getReceiptFromJk(r_34)) ==> event(getReceiptFromClerk(id_33,r_34))
Completing...
Starting query event(getReceiptFromJk(r_34)) ==> event(getReceiptFromClerk(id_33,r_34))
RESULT event(getReceiptFromJk(r_34)) ==> event(getReceiptFromClerk(id_33,r_34)) is true.
-- Query event(getReceiptFromClerk(id_250,r_251)) ==> event(sendReceiptToJk(id_250,r_251))
Completing...
Starting query event(getReceiptFromClerk(id_250,r_251)) ==> event(sendReceiptToJk(id_250,r_251))
RESULT event(getReceiptFromClerk(id_250,r_251)) ==> event(sendReceiptToJk(id_250,r_251)) is true.
-- Query event(getMoneyFromMa(m_461)) ==> event(sendMoneyToJk(m_461))
Completing...
Starting query event(getMoneyFromMa(m_461)) ==> event(sendMoneyToJk(m_461))
goal reachable: begin(sendMoneyToJk(money_28[])) -> end(getMoneyFromMa(money_28[]))
RESULT event(getMoneyFromMa(m_461)) ==> event(sendMoneyToJk(m_461)) is true.
-- Query not event(failReceipt(r_659))
Completing...
Starting query not event(failReceipt(r_659))
RESULT not event(failReceipt(r_659)) is true.
```

注目するべきは次の部分である。

> ```
> RESULT event(getReceiptFromClerk(id_250,r_251)) ==> event(sendReceiptToJk(id_250,r_251)) is true.
> RESULT event(getReceiptFromJk(r_34)) ==> event(getReceiptFromClerk(id_33,r_34)) is true.
> RESULT event(getMoneyFromMa(m_461)) ==> event(sendMoneyToJk(m_461)) is true.
> RESULT not event(failReceipt(r_659)) is true.
> ```

まず、最初の三つはこれらの性質が成り立つことが明かになったということを示している。そして最後の一行は、この性質が成り立たないことが明らかになったことを示している。`failReceipt`が発生するケースがあるというのは、このプロトコルにとってまずいことなので、これが成り立たないのは正しい性質である。

# まとめ

この記事ではProVerifの全機能を解説することはできなかったが、最初のさわりをおさえることはできたのではないかと思う。今後はより実用的なプロトコルの検証にProVerifを用いて記事にまとめたい。

# 参考文献

- [ProVerif User Manual](http://prosecco.gforge.inria.fr/personal/bblanche/proverif/manual.pdf)
- [Webspi](http://prosecco.gforge.inria.fr/webspi/POST/index.html)