はじめに
Proverifとは、プロトコルを形式的に検証するツールです。プロトコルをモデル化したコードで記述して、Proverifツールで実行すると脆弱性の有無を判断してくれます。
今回はProverif2.04を用いて、簡単なプロトコルについて秘匿性、オフライン攻撃耐性、の有無を検証していきます。
プロトコルの検証に関して、初心者です。備忘録を兼ねておりますので、間違い等ございましたらご指摘ください。
インストールと環境構築
インストールと環境構築の方法は以下をご覧ください。
検証するプロトコル
以下の簡単なプロトコルで検証を行います。
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のプロセスを並列に繰り返し動作させることを表します。
コードの全体像
以下にコードを貼っておきます。
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()) )
コードの実行
以下のようにして、コードを実行します。
$ 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の簡単なプロトコルの検証でしたが、結構苦戦しましたので皆様のご参考になれば幸いです。
今後はより実用的なプロトコルや、他の脆弱性につていの検証なども記事にまとめていければなーと思います。
ご意見、ご指摘等あれば、コメントしていただけると幸いです。