第 6 章 ハッシュ関数からの情報漏洩を考慮した安全性の形式検証
6.3 情報漏えいを伴うランダムオラクルモデルにおける自動証明
（b）さもなくば，rEO2 は，u=1からqRまで，RO2で定義された(M[u],r[u])を探索 し， もし，z=r[u]なるuが存在すれば，rEO2 はMEにM[u]||mを割り当てる．
（c）さもなくば，rEO2 は，v=1からqEまで，rEO2で定義された(ME[v],zE[v])を探 索し，もし，ME[v],⊥ ∧z=zE[v]なるvが存在すれば，rEO2 はMEにME[v]||m を割り当てる．
（d）さもなくば，rEO2は，MEに⊥を割り当てる．
3. 次に，rEO2は，出力値を以下のように決定する．
（a）rEO2 は，u = 1からqRまで，RO2 で定義された(M[u],r[u]) を探索し， もし，
m= M[u]∧z=IV なるuが存在すれば，rEO2 はr[u]を出力する．
（b）rEO2は，v= 1からqE まで，rEO2 で定義された(ME[v],zE[v])を探索し，もし，
m= ME[v]∧z= IV なるvが存在すれば，rEO2はzE[v]を出力する．
（c）rEO2 は，u = 1からqRまで，RO2 で定義された(M[u],r[u]) を探索し， もし，
ME = M[u]なるuが存在すれば，rEO2はr[u]を出力する．
（d）rEO2は，v= 1からqE まで，rEO2 で定義された(ME[v],zE[v])を探索し，もし，
ME = ME[v]なるvが存在すれば，rEO2 はzE[v]を出力する．
（e）さもなくば，rEO2は，zE をDから一様ランダムに選択し，それを出力する．
注意1 ROの出力が衝突を起こす確率を評価することで，rEROとEROは観測等価であるこ とを証明できる．また，T ROとwT ROも，ROの出力が衝突を起こす確率を評価することで，
観測等価であることを証明できる．つまり，我々は，CryptoVerifで記述できる，新しい定義を 与えたといえる．
6.3 情報漏えいを伴うランダムオラクルモデルにおける自動
6.3.1 FDH 署名と安全性要件
■記法 ここでは，方式を記述するための記号を定義する．λはセキュリティパラメータ，
PK は公開鍵の空間，S K は秘密鍵の空間とし，f : PK × Dom → Domは落とし戸付き置 換，f−1 :S K ×Dom→ Domは f の逆置換とする．H : {0,1}∗ → Domはハッシュ関数とし，
a ←R AはAよりランダムに値を選択しaに代入する処理とし，a =? bはaとbが等しいとき trueを，異なるとき f alseを戻す関数とする．
■方式 FDH署名は，鍵生成アルゴリズムK，署名生成アルゴリズムS，署名検証アルゴリ ズムV の3つからなる．
K(1λ) S(sk,M) V(pk,M, σ) (pk,sk)←R KG(1λ). h← H(M); h← H(M);
σ← f−1(sk,h). h=? f(pk, σ).
図6.4 FDH署名方式
鍵生成アルゴリズムは，セキュリティパラメタ1λを受け取り，公開鍵 pkと秘密鍵skを生 成する．署名アルゴリズムは，秘密鍵 skと文書Mを入力とし，Mのハッシュ値h= H(M)を 計算し，hの逆置換 f−1(sk,h)を計算して署名σとし出力する．検証アルゴリズムは，公開鍵 pkと文書 Mと署名 σを入力とし，M のハッシュ値h= H(M)を計算し，σの置換 f(pk, σ) とhが等しいか否か判定し結果を出力する．
■計算量的仮定 FDH署名の安全性の根拠となっている計算量的仮定の定義を記す．
定義24 pkを用いると f(pk,∗)が多項式時間で計算でき，skを用いると f−1(sk,∗)が多項式時 間で計算でき，時間t以内ではいかなる多項式時間アルゴリズムをもってしても sk を用いず に逆置換を計算できる確率が高々ϵ であるとき，f は(t, ϵ)-落とし戸付き一方向性置換という．
一方向性置換として，Blanchetらにより定式化されたもの[24]を用いる．
■安全性要件 現在，デジタル署名方式は，EUF-ACMA安全性 を満たせば安全とされてい る．以下に，一般的なEUF-ACMA安全性の定義を示す．
定義25 (EUF-ACMA安全性 )多項式時間tで動作するあらゆるオラクルクエリTuring機械 に対して以下の条件が成立するとき，デジタル署名方式は(t,qH,qS, ϵ)-EuF-ACMA安全であ るという．
公開鍵を入力された後，任意の順番で，高々qH 回のランダムオラクルへの問い合わせと，
高々qS 回の署名オラクルへの問い合わせを行い，署名オラクルへ問い合わせたことの無い文 書m∗ に対して検査に合格するような署名σ∗を出力する確率が高々ϵ である．
ランダムオラクルからの情報漏洩が生じるモデルでは，ランダムオラクルと署名オラクルに 加え，情報を漏洩するオラクルにqL 回まで問い合わせを行い，情報を手に入れることが出来 る．また，鍵生成オラクルは，署名鍵と検証鍵を生成し検証鍵を攻撃者に与えるオラクルで，
テストオラクルは攻撃者の出力した署名が偽造署名の条件を満たすかを判定して返すオラクル である．
KeyGen Oracle
Random Oracle
OracleSign
OracleTest
Attacker
event bad/ yield
(m*,σ*) pk
F
qRtimes
qStimes
OracleLeak qLtimes
図6.5 情報漏洩を考慮したEUF-CMAモデル
図6.5は，以下のモデルを定式化したものである．seed は鍵のシード，pkgenは公開鍵を 生成する関数，skgen は秘密鍵を生成する関数とする．ランダムオラクルRandomOracle は Blanchetらが与えた定義[24]を用い，漏えいオラクルLeakOracleは，前述のように，wT RO かEROで定義する．高々qS 回まで， 署名オラクルS ignOracleはm: bitstringを受け取り，
f−1(sk,hash(m))を返す．高々1回まで， テストオラクルT estOracleは(m∗ :bitstring, σ∗)を
受け取り，存在的偽造に成功したか否かを判定する．
(in(start,());
newr: seed;
let pk= pkgen(r)in let sk= skgen(r)in out(c0,pk);
(S ignOracle|T estOracle|RandomOracle|LeakOracle))
6.3.2 CryptoVerif による FDH 署名の検証結果
まず，既存の結果を紹介した後，実験結果を記す．
■既存の結果 人手による証明では，LROで安全であることが示されている [74]．さらに，
FDH署名の安全性は，LROよりも漏洩する情報の少ないT RO，EROでも同様に安全性が成 立することが示されている．
また，CryptoVerifによる検証は，ROモデルの下でのみ行われており，EF-CMA安全性が
証明できることが知られている．証明は，次の3つ変形規則を適用することで行われ，単純化 処理など11回のゲームの変形が行われる．
1. hash関数の出力を一様ランダムにする変換．
2. 置換への入力のランダム性と単射性を利用し，ランダムオラクルの出力と署名オラクル の出力を交換する変形．
3. 理想的な一方向性を満たす関数への変形．
6.3.2.1 今回の結果
CryptVerifによる検証結果は次のとおりである．検証に用いた計算機はInter(R) Core(TM)2
Duo CPU U9300 @ 1.20GHz, RAM 2.85GBで，CryptoVerifは バージョン1.10pl1を用いた．
■wT ROモデル CryptoVerifによる検証の結果，wT ROでは安全性を証明できた．
11回のゲームの変形で証明できた．証明にかかる時間は，約30秒である．攻撃者が偽造に 成功する確率は，高々(qS +qR+1)∗ϵ との結果を得た．
■案1のrEROモデル 案1のrEROを使った証明では，上記2.の変形を適用する処理が終 了しないため，安全性証明が出来なかった．その原因は以下のとおりである．
CryptoVerifでは，オラクルへの入力と内部で定義された値は全て配列に記録される．簡単
のため，ROで定義された値の集合をRO-List，ROで定義された値の集合を EO-Listと呼ぶ．
まず，hash関数の出力を一様ランダムにし，invhash関数はhash関数の逆像の要素を出力す る処理に置き換える書き換え規則を適用する．適用後，ROとEOは，以下のような処理に変 換される．
!qRRO(M:bitstring) :=
if(M,r)∈RO-Listthen out(r)
else if(m,z,M′,z′)∈EO-Listthen out(z′) else newr:D;out(r)
else . . . .
!qE EO(m:bitstring,z: D) :=
if(m,z,M′,z′)∈EO-listthen out(z′) else . . .
else(M,z)∈RO-Listthen letM′ = M||min . . .
else newz′ : D;out(z′)
else if(∗,∗,M′,z)∈EO-Listthen letM′ = M′||min . . .
else newz′ : D;out(z′) else . . . .
EOは，与えられたz : Dが，EOで定義されたの値である場合も，ROで定義された値であ る場合も，条件を満たす値がRO-List,EO-Listに含まれていなければ，新たにz′ を定義して 返す．
曖昧性を避けるために，CryptoVerifは，一つ変数にはただ一つの定義のみを認める．もし，
ゲーム中に，同じ変数名の定義が複数個所に存在すると，CryptoVerifは，それらをリネーム し，曖昧性を取り除く．
今回の場合も，CryptoVerif は，上記 z′ を異なる変数名に変換しようと試みる．しかし，
CryptoVerifのリネーム方法では，z′ を異なる変数名には変換できず，リネーム処理を繰り返
すので，検証が停止しない．
■案2のrEROモデル リネームを行う必要が無いよう，EOの出力値は一様ランダムに決定 されることを利用して，定義される処理をあらかじめ1つにまとめた書き換え規則である．
この規則の下では，12回のゲームの変形で証明できた．証明にかかる時間は，約30秒であ る．攻撃者が攻撃に成功する確率は，高々(qS +qR+qE +1)∗ϵ であるとの結果を得た．