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

はじめに

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

インストールと入手

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

OS X

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

その他のOS

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

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

詳しいインストール方法については、公式のマニュアルに書かれている。

Hello World

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

hello_world.pv

free c:channel.

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

process
  out(c, RSA);
  0

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

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

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

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

ここではProVerifの練習として、JK・おっさんプロトコルを検証してみる。プロトコルの流れを引用すると次のようになる。

高校生判定プロトコル

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

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

型の定義

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

お金

支払いで暗黙的に登場

レシート

支払いの結果を証明する書類として登場

JKの身分証明書

JKが店員に身分を証明するために登場

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

type Money.
type Receipt.
type Id.

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

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

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

• JKからおっさん
• おっさんからJK
• JKから店員
• 店員からJK

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

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

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

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

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

free ngId:Id.

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

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

fun makeReceipt(Id, Money): Receipt.

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

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

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

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

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

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

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

process
  ( jk() | middleAge() )

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

イベントとクエリー

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

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

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

event getMoneyFromMa(Money).
event sendMoneyToJk(Money).

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

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で次のように書ける。

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

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

検査

全てを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() )

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

• 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を受け取った）

実行結果

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

$ 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
• Webspi

1. Emacsでなくとも、テキストエディタであればなんでも問題はない。 ↩

2. ここでmaとはMiddle Ageのことで、おっさんを指す。 ↩

3. ここでは最終的なプロセスの一部という意味で「サブプロセス」という言葉を用いている。 ↩

4. shopClerkについている!は、ここでは複数の店員がいるということを表現していると考えればよい。 ↩