はじめに

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のプロセスを並列に繰り返し動作させることを表します。

コードの全体像

以下にコードを貼っておきます。

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()) )

コードの実行

以下のようにして、コードを実行します。

$ 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

ProVerifによるWPA3プロトコルの検証 | 晴耕雨読