セキュリティプロトコルの形式検証ツール“ProVerif”
はじめに
ProVerifとは、INRIAが開発したセキュリティプロトコルを形式検証するツールである。この記事ではProVerifによるプロトコルの形式検証のやり方の基礎を解説する。なお、この記事では2015年10月時点での最新版であるProVerif 1.91について解説する。
この文章を読んで何か気がついたことがあったら、コメントなどで気軽に指摘して欲しい。
インストールと入手
次のようにインストールできる。また、現在はEmacs用のモードが提供されているので、Emacsも併せてインストールするといいかもしれない1。
OS X
$ brew tap homebrew/science/proverif
$ brew install proverif
その他のOS
下記のサイトからソースコードをダウンロードしてコンパイルする。
詳しいインストール方法については、公式のマニュアルに書かれている。
Hello World
それでは早速ProVerifによる検証を行ってみる。次のようなファイルを作成する。
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・おっさんプロトコルを検証してみる。プロトコルの流れを引用すると次のようになる。
高校生判定プロトコル
おっさん
は自分が 信頼できる カラオケ・理髪店・映画館をいくつかピックアップして、そのリストをJK
へ渡すJK
は(1)で受け取ったリストの中から 信頼できる お店を一つ選択する(もし信頼できるお店がリストにない場合は、おっさん
がお店のリストを作り直す)おっさん
とJK
は(2)で指定したお店で待合せをして、JK
はそのお店を 高校生の価格 で利用する(その際に学生証などを提示するが、おっさん
は少し離れた場所に待機してもらい、学生証が店員にしか見えないようにする)JK
はお店を高校生の価格で利用したことを示す証拠(レシートなど)をおっさん
に提示するおっさん
は(4)の証拠を確認する(レシートの日付けなど)
これをProVerifへ翻訳すると、どのようになるだろうか。
型の定義
JK・おっさんプロトコルには出てくる概念を、Proverifの型として考える。ここでの型という言葉は、一般的なプログラム言語の型と同じと考えてよい。JK・おっさんプロトコルに登場するのは次のような型である。
- お金
- 支払いで暗黙的に登場
- レシート
- 支払いの結果を証明する書類として登場
-
JK
の身分証明書 -
JK
が店員に身分を証明するために登場
これを次のようにProverifで定義する。
type Money.
type Receipt.
type Id.
通信経路とJK
の身分証明書の定義
通信経路(チャンネル)の定義
このプロトコルでは次のような通信が発生する。
-
JK
からおっさん
-
おっさん
からJK
-
JK
から店員 - 店員から
JK
この通信経路を、Proverifではchannnel
という型を持つ変数として次のように定義する2。
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() )
まず、サブプロセス3jk
は通信経路(チャンネル)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へ翻訳すると、例えば次のようになる4。
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を用いて記事にまとめたい。
参考文献
Author And Source
この問題について(セキュリティプロトコルの形式検証ツール“ProVerif”), 我々は、より多くの情報をここで見つけました https://qiita.com/yyu/items/f35f24516fd1776c19d9著者帰属:元の著者の情報は、元のURLに含まれています。著作権は原作者に属する。
Content is automatically searched and collected through network algorithms . If there is a violation . Please contact us . We will adjust (correct author information ,or delete content ) as soon as possible .