第 3 章 CryptoVerif
3.2 CryptoVerif
3.2.1 概要
Blanchetらのフレームワークでは，計算量的手法と形式的手法のギャップを埋めるために，
直接的手法がとられている．観測等価性の概念をGameにおけるIndistinguishabilityと一致す るように変更した．これによって，プロセスを高々時間tで動作し，その入出力はbitstringと することができた．さらに，プロセス計算に確率的な意味を持たせることで，攻撃者の2つの View 間の距離というかたちで，Distinguishabilityや観測等価性を定義できるようになった．
この距離は，純粋に記号論的に変換を行うために役立つ．変換は書き換えルールとして表現さ れ，書き換えルールによって，距離が等しいか計算量的仮定の下でほとんど等しいゲームが生 成される．
Blanchetらは，上記のような工夫を施して，Game列による検証を自動化する方法を提案し
た[24, 21]．提案された方法は，証明したいプロトコル，その攻撃モデル，計算量的な仮定，
演算規則などの証明に必要な条件を，プロセス計算に従って書き換えルールとして記述したも のを与えることで，そのルールに従ってプロトコルの変形を行い証明を行う方法である．さら に，Blanchetは提案手法を実装したプログラムCryptoVerif*2と共に，FDH署名[18]やPFDH 署名 [38]などの自動証明を行うためのサンプルデータも公開している．これらの方式は，一 方向性落とし戸付き置換を安全性の根拠としており，サンプルデータには一方向性落とし戸付
き置換をCryptoVerifで取り扱うための記述がある．一度でも記述を作成すれば，その記述と
同じ条件を必要とする他の方式の証明にも流用できる．
典型的な形式手法では，攻撃者に許す操作を記号的操作に制約して評価を行っていた．その ため，制約された攻撃者に対する安全性しか評価できず，直接的に計算量的安全性を評価でき なかった．一方，CryptoVerifでは，証明中で可能なゲームの変形を記号的操作に制約するの みで，攻撃者を制約しない．つまり，計算量的な攻撃者に対して観測等価性を評価した書き換 えルールを利用することにより，証明の手順は制約されるが，攻撃者を制約しない証明を与え ている．そのため，CryptoVerifは，典型的な形式手法とは異なり，直接計算量的安全性を評価 できる．
*2Bruno Blanchetのサイトで無償で公開されている．http://www.di.ens.fr/blanchet/
3.2.2 プロセス計算
本節では，計算量的な安全性証明を行うGameをモデル化するためのプロセス計算について 検討する．このプロセス計算を用いることで，ランダムオラクルや暗号プリミティブの複数の 性質の定式化が可能になった．さらに，帰着のコストについて従来は漸近的な評価を行ってい たが，このプロセス計算ではどれくらいの損失があるか正確な評価ができる．
プロセス計算の最低限必要な文法を次に記す．詳細は文献[21, 22]を参照のこと．
• bitstring:全てのbitstringを要素とする集合．
• ⊥:特別な記号．
• bitstring⊥ =bitstring∪ {⊥}．
• T型:bitstring⊥の部分集合．
• f ixed-length:型がある長さのbitstringの集合であるとき，f ixed-lengthであるという．
• large : T型から一様ランダムに要素を選ぶ際，衝突が生じる確率が十分小さいとき，T
はlargeであるという．ただし，低い確率で衝突が生じることがある．
• bool={true,false}． ただし，true=1,false =0．
• f :関数記号．型宣言 f :T1×T2× · · · ×Tm → T を伴う．このとき，時間tf で計算可能 な f(x1, . . . ,xm)をあらわす．ただし，tf は入力x1, . . . ,xmで制限されている．
• M =? N :等価テスト．同じ型の2つの値をとり，boolを返す．
• M∧N :等価テスト．同じ型の2つのboolをとり，boolを返す．
• a←bはaにbを代入する．
• a←R Dは空間Dから 要素をランダムに選びaに代入する．
3.2.3 観測等価性
本節では，観測等価性の定義とそこから導かれる補題を紹介する．
形式手法では，Gameが完璧なプリミティブを使ったプロセスに置き換わる．観測等価性と は，識別不可能性とよく似た概念で，敵による二つのプロセス間の識別可能性をあらわして いる．
• Ostart() : experimentが始まる際に呼ばれるオラクル．ゲーム開始の合図を意味する．()
は，通信のリクエストのみで，データとしては何も与えられないことを意味する．
• Pr[C[Q]] a:Ostart()が呼ばれてからのプロセスQの答えがaとなる確率．
• Pr[C[Q]] E:Ostart()が呼ばれてからのプロセスQがイベント列Eをこの順序で実行 する確率．
次の定義では，ContextCはプロセスQとQ′ を見分けようとするアルゴリズムをあらわして いる．プロセス Qを呼び出すContextをC[Q]を書く．この構成は，プロセスQはContextC に含まれるその他のプロセスとパラレルに入力されることをあらわしている．このとき，
ContextC はプロセスQのオラクルを外部から隠すことができる．(例えば，C′[C[Q]]を考え
ると，C′ はQのオラクルにアクセスできない．)
定義2 (観測等価性). QとQ′はwell-formedness invariantsを満たすprocesseとする．Context C が event を含んでおらず，C と Q の間に共通の invariant が存在せず，C[Q] が well-formedness invariantsを満たすとき，かつその時に限り，C はQをacceptableであるという．
QとQ′が
∀C∀a: (|Pr[C[Q] a]−Pr[C[Q′] a]| ≤ p(t)
∧∑
E|Pr[C[Q] E]−Pr[C[Q′] E]| ≤ p(t)) (3.1)
を満たすとき，QとQ′ は 確率 pまで観測等価性 といい，Q ≈p Q′ と書く．ただし，C はQ とQ′をacceptableで実行時間が高々tのContext，aはbitstringである．
定義3
∀C :
∑
E,e∈E
Pr[C[Q] E]≤ p(t)
(3.2)
を満たすとき，かつそのときに限り，Qはeventeを高々確率 pで実行するという．ただし，
CはQをacceptableで実行時間が高々tのContextである．
定義2，3より，補題2が導かれる．
補題2 1. ≈p は反射的かつ対称的である．
2. Q≈p Q′ かつQ′ ≈p′ Q′′ならばQ≈p+p′ Q′′．
3. Qが高々確率pでeventeを実行し，Q≈p′ Q′ならば，Q′は高々確率 p+ p′ でevente を実行する．
4. Q ≈p Q′， C は Q と Q′ を acceptableでその実行時間は高々 tc の Context ならば，
p′(t)= p(t+tC)なるC[Q]≈p′ C[Q′]が成り立つ．
5. Qが高々確率 pでeventeを実行し，C はQをacceptableでその実行時間は高々tcの Contextならば，C[Q]は高々p′(t)= p(t+tC)なる確率 p′ でeventeを実行する．
Q{P′/P}は，プロセス Qで起こるサブプロセス Pを全てP′ で置き換えをあらわす．つま り，Q{P′/P}とQ{P′′/P}でサブプロセスPの置き換えを行った以外の部分は完全に同じプロ セスである．よって，eventeを含むプロセスQを考えると，次の補題2が成り立つ．
補題3 Qが高々確率 pでeventeを実行するならば，
Q{P′/evente.P} ≈p Q{P′′/evente.P} (3.3) が成立する．
これは，ShoupのDifference Lemma[86]を プロセスを用いて記述しなおしたものである．
n×Qは，Qのn個の独立なコピーを表す．eventeを実行する Qのコピーをランダムに選 び，その他の Qのコピーをシミュレートすることで補題3が証明できる．
補題4 Qが高々確率 pでeventeを実行し，Qは時間tQで実行されるならば，n×Qは高々
p′(t)=n× p(t+(n−1)tQ) (3.4)
なる確率 p′ でeventeを実行する．
3.2.4 CryptoVerif の動作例
G0 をInitial Game，Gm をFinal Gameとすると，CryptoVerifの目的は，G0 ≈p Gm を作る ことである．CryptoVerifには，G0 と観測等価性を満たす書き換えルールのみが与えられ，Gm
はCryptoVerifが生成する．
CryptoVerifは，書き換えルールをもとにしてInitial Gameを書き換えていく．そして，攻撃
成功のイベントが起こらないGameに到達することができるかどうか判定する．到達できた とき，その暗号プロトコルは与えられた書き換えルールの下で安全であると判定し停止するま た，書き換えルールは観測等価性を満たす式として与えられているため，書き換えルールの適 用によって生じるGame間の差を評価することができ，最終的にInitial GameとFinal Game の間の差を出力することができる．与えられた書き換えルールから，攻撃成功イベントの起こ らないゲームまで到達できなかったときは，与えられた書き換えルールでは安全性を保証でき ないと判定し停止する．このとき，適切な書き換えルールを与えれば，証明できる可能性は残 されている．
end end end end
end end end
end
end win win
end end end end
end end
end end end
winwin
win win
win win
end end end end
end end
end winwin
winwin
1. 書き換えルールによる書き換え． 2. 無駄な判定の削除による書き換え．
Win Win への枝が存在しない Game
end end end end
end end
end win win
win win end
end end end
end end
win win
Initial Game
1
1
1 2
2
図3.1 動作例