Extension attack simulatable Random Oracle (ERO)[74]

EROは，SHA1などが採用しているMerkle-Damgård construction[71, 41] から漏洩する情 報をモデル化したものである．EROの定義は次のとおりである．

定義22 (Extension attack simulatable Random Oracle[74])EROは，定義18のROとEOから なる． IV はハッシュ関数の初期ベクトルである．EOは，空リストで初期化されたEO-List を持っており，RO-Listを見ることができるとする．シミュレーションクエリ(m,z)がEOに 問い合わされると，下記のように結果を返す．

1. もし(m,z,zE)∈EO-Listが存在すれば，zEを返す．

2. もし z = IV ならば， EO は m をRO に問い合わせ， zE を受け取り， (m,z,zE) を EO-Listに記録し，z_E を返す．

3. もし(M,z) ∈RO-Listがただ一組のみ存在していれば， EOはM||mをROに問い合わ せ，zE を受け取り，(m,z,zE)をEO-Listに記録し，zE を返す．

4. それ以外の場合は，EOはz_E ∈Dを一様ランダムに選択し，(m,z,z_E)をEO-Listに加 えてz_E を返す．

CryptoVerifは，ある配列内に条件を満たすインデックスが「ただ一つのみ」存在するか否か

を判定する手段を提供していない．そのため，我々は，EOの判定条件を緩和したEROモデ ルであるRelaxedERO(rERO)モデルを定義する．

定義23 (Relaxed Extension attack simulatable Random Oracle) rERO は，定義 18 の RO と rEOからなる．IV はハッシュ関数の初期ベクトルとなる．rEOは，初期状態は空のリスト rEO-Listを持っており，RO-Listを見ることができるとする．シミュレーションクエリ(m,z) がrEOに問い合わされると，下記のように結果を返す．

1. もし(m,z,zE)∈rEO-Listが存在すれば，zEを返す．

2. もしz= IV が存在すれば，rEOはmをROに問い合わせ，zEを受け取り，zE を返す．

3. もしn個の(M_i,z)∈RO-List(i=1, . . . ,n)が存在したら，rEOはi∈ {1, . . . ,n}^を一様ラ ンダムに選択し，Mi||mをROに問い合わせ，zEを受け取り，zE を返す．

4. それ以外の場合は，rEOをzE ∈ D一様ランダムに選択し，(m,z,zE)をrEO-Listに加 え，z_E を返す．

EROモデルとrEROモデルは，ROの出力が衝突を起こさない限り，完全に同じふるまいを する．ROの定義域は十分に大きいため，衝突を起こす確率は無視できるほど小さい．そのた め，多項式時間アルゴリズムでは，EROモデルとrEROモデルを識別することが出来ない．

6.2.4.1 CryptoVerifのための定式化(rERO)

CryptoVerifの記述法を使うと，rEROモデルは，いくつかの定式化が考えられる．まず，

wT ROを利用した素直な定式化である案1を与える．残念ながら，第6.3.2.1節で説明する理 由により，CryptoVerifは，案1の記述を用いると，FDH署名の安全性を証明することができ なかった．そこで，直接的で単純にrEROを定式化した案2を与える．案2の記述を用いる

と，CryptoVerifは，FDH署名の安全性を証明することができた．

■案 1.(wT RO を使った rERO) 図 6.2 は，rERO の定式化案 1 である．ただし，hash : bitstring→ D，invhash: D→ bitstring∪ ⊥^とする．ROはランダムオラクルで，rEO1は情 報を漏えいするオラクルである．hashとinvhashは，wT Oモデルと同様に定義される．案1 では，rEO1は，wT Oでも用いたhashとinvhashを利用して定式化される．

equiv!qR(M :bitstring)N →hash(M), [all]

!qE(z: D)→invhash(z) [all]

<= (0)=>

!qR(M:bitstring)→findu≤qRsuchthat

(defined(M[u],r[u])∧M= M[u])thenr[u]else newr: D;r,

!q_E (z:D)→findu≤q_Rsuchthat

(defined(M[u],r[u])∧z=r[u])thenM[u]else⊥.

letRO:=!q_Rdo in(c1,M :bitstring);out(c2,hash(M)). letrEO1 :=!qEdo in(c3,M :bitstring,z:D);

findv≤ qE suchthat(defined(M[v],z[v],zE[v])

∧M = M[v]∧z=z[v])then out(c4,z_E[v]) else ifz=IV then out(c4,hash(M))

else ifinvhash(z), ⊥then out(c4,hash(invhash(z)||z)) else newzE :D;out(c4,zE).

図6.2 CryptoVerifのためのrEROの定式化：案１

図6.2 の書き換え規則の適用後，ROとrEO₁ は下記の処理に変換される．ROは，通信路 c1からMを受け取ると，

1. u= 1からq_RまでROで定義された配列(M[u],r[u])を探索し，もし，M = M[u]なる uが存在したら，r[u]を通信路c2から出力する．

2. それ以外の場合，M= M[u]なるuが存在しないので，ROは，定義域Dから一様ラン ダムにrを選択することで定義し，rをc2から出力する．

rEO₁は，通信路c3から(M,z)を受け取ると，

1. v = 1 からq_E までrEO₁ で定義された配列 (M[v],z[v],z_E[v]) を探索し，もし，M = M[v]∧z=z[v]なるvが存在したら，zE[v]を通信路c4から出力する．

2. もし，z= IVならば，M をROに問い合わせ， 受け取った要素をc4から出力する．

3. もし，u = 1からq_Rまで ROで定義された配列 (M[u],r[u])を探索し，z= r[u]なる u が存在するならば，条件を満たすuの集合から一様ランダムに1つ選択し，M[u]||Mを ROに問い合わせて，受け取った要素をc4から出力する．

4. それ以外の場合は，定義域Dから一様ランダムに zE を選択することで定義し，zE を c4から出力する．

■案 2.(直接的で単純な rEROの定式化) 図 6.3 は，rEROの定式化案 2 である．ただし、

hash: bitstring→ D，reo₂ : bitstring×D→ Dである．RO₂ はランダムオラクルで，rEO₂ は情報を漏えいするオラクルである．案 2では，rEROをwT Oを使わずに直接的に定義す る．rEO2 は，RO2 に問い合わせを行うことは許されていない．その代り，rEO2 は，RO2 と rEO₂ によって定義された配列—すなわち，RO-Listと rEO-List—を参照し，その出力を決 定する．さらに，RO2 は，Blanchetらが与えたランダムオラクルの定義とは異なり，RO2 と rEO2が定義した配列を参照してその出力を決定する．

rEO₂ の愚直に記述すると次のようになる．シミュレーションクエリ(m,z)がrEO₂ に問い 合わされると，

1. rEO₂ は，v = 1からq_E まで，rEO₂ で定義された(m[v],z[v],z_E[v])を探索し，もし，

m=m[v]∧z=z[v]なるvが存在したら，rEO2はzE[v]を出力する．

2. さもなくば，もし，z=IV ならば，rEO2はME にmを割り当て， 以下を実行する．

（a）rEO₂ は，u = 1からq_Rまで，RO₂ で定義された(M[u],r[u]) を探索し， もし，

ME = M[u]なるuが存在すれば，rEO2はr[u]を出力する．

（b）さもなくば，rEO2は，v =1からqE まで，rEO2 で定義された(ME[v],zE[v])を

探索し，もし， M_E = M_E[v]なるvが存在すれば，rEO₂ はz_E[v]を出力する．

（c）さもなくば，rEO₂は，z_E をDから一様ランダムに選択し， それを出力する．

3. さもなくば，rEO2 は，u=1からqRまでRO2 で定義された(M[u],r[u])を探索し，も し，z = r[u]なるu が存在すれば，rEO2 は ME にM[u]||mを割り当て，以下を実行 する．

（a）rEO2 は，u = 1からqRまで，RO2 で定義された(M[u],r[u]) を探索し， もし，

ME = M[u]なるuが存在すれば，rEO2はr[u]を出力する．

（b）さもなくば，rEO₂は，v =1からq_E まで，rEO₂ で定義された(M_E[v],z_E[v])を 探索し，もし， ME = ME[v]なるvが存在すれば，rEO2 はzE[v]を出力する．

（c）さもなくば，rEO2は，zE をDから一様ランダムに選択し， それを出力する．

4. さもなくば，rEO₂ は，v=1からq_E までrEO₂で定義された(M_E[v],z_E[v])を探索し，

もし，z= zE[v]なるvが存在すれば，rEO2 はMEにM[u]||mを割り当て，以下を実行 する．

（a）rEO₂ は，u = 1からq_Rまで，RO₂ で定義された(M[u],r[u]) を探索し， もし，

M_E = M[u]なるuが存在すれば，rEO₂はr[u]を出力する．

（b）さもなくば，rEO2は，v =1からqE まで，rEO2 で定義された(ME[v],zE[v])を 探索し，もし， ME = ME[v]なるvが存在すれば，rEO2 はzE[v]を出力する．

（c）さもなくば，rEO₂は，z_E をDから一様ランダムに選択し， それを出力する．

5. さもなくば，rEO2は，zE をDから一様ランダムに選択し， それを出力する．

rEO2 は，RO2 かrEO2 で定義された配列の中に，(m,z)が存在しないとき，ランダムに出力 を選択する．この出力は，RO2(m),RO2(M||m),RO2(ME||m)または ランダム出力のいずれかに 対応するもので，それらは全て同じ分布で選択されるという特徴がある．我々は，この4つの 出力を1つにまとめて，単純な定式化を与える．

第6.3.2.1節で説明するように，この単純な定式化を用いると，同じ変数のリネーム処理を

避けることができるため，CryptoVerifはFDH署名の安全性を証明することができた．

図6.3 の書き換え規則の適用後，ROとrEO2 は下記の処理に変換される．ROは，通信路 c1からMを受け取ると，以下の手順で出力を決定する．

1. RO2 u= 1からqRまで，RO2 で定義された(M[u],r[u])を探索し， もし， M = M[u]

なるuが存在すれば，RO2 はc2からr[u]を出力する．

2. さもなくば，RO₂ はv = 1から q_E まで，rEO₂ で定義された(m[v],z[v],M_E[v],z_E[v]) を探索し，もし，M = ME[v]なるvが存在したら，RO2 はc2からzE[v]を出力する．

3. さもなくば，RO2 は，rをDから一様ランダムに選択し，それを出力する．

equiv!q_R (M :bitstring)→hash(M), [all]

!qE (m:bitstring,z:D) → seo2(m,z) [all]

<= (0)=>

!q_R(M:bitstring)→

findu≤qRsuchthat (defined(M[u],r[u])∧M = M[u])thenr[u]

else findv≤qEsuchthat(defined(ME[v],zE[v])∧M = ME[v])thenzE[v]

else newr: D;r,

!q_E (m:bitstring,z:D)→

findv≤qE suchthat defined(m[v],z[v],ME[v],zE[v])∧m= m[v]∧z= z[v]

then zE[v]

else(letM_E :bitstringbot= ( ifz= IVthenm

else findu≤qRsuchthat(defined(M[u],r[u])∧z= r[u])then M[u]||m else findv≤q_Esuchthat(defined(M_E[v],z_E[v])∧M_E[v], ⊥ ∧z=z_E[v])

thenME[v]||m else ⊥)in(

findu≤q_Rsuchthat defined(M[u],r[u])∧m= M[u]∧z= IV thenr[u]

else findv≤qEsuchthat defined(ME[v],zE[v])∧m= ME[v]∧z= IV thenzE[v]

else findu≤qRsuchthat defined(M[u],r[u])∧ME = M[u]then r[u]

else findv≤qEsuchthat defined(ME[v],zE[v])∧ME = ME[v]then zE[v]

else new z_E : D;z_E)else new z_E :D;z_E).

letRO2 =!qRdo in(c1,x:bitstring);out(c2,hash(x)).

letrEO₂ =!q_Edo in(c3,t:bitstring,s: D);out(c4,seo₂(t,s)).

図6.3 CryptoVerifのためのrEROの定式化：案２

rEO2は，高々qE回まで，入力(m,z)に対して，以下のように出力を決定する．

1. rEO2 は，v = 1 からqE まで，rEO2 で定義された(m[v],z[v],ME[v],zE[v])を探索し，

もし，m= m[v]∧z=z[v]なるvが存在すれば，rEO2はzE[v].を出力する．

2. さもなくば，rEO₂はM_E を次のように定義する．

（a）Ifz=IV then,rEO₂assignsmtoM_E.

（b）さもなくば，rEO₂ は，u=1からq_Rまで，RO₂で定義された(M[u],r[u])を探索 し， もし，z=r[u]なるuが存在すれば，rEO₂ はM_Eに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）rEO₂ は，u = 1からq_Rまで，RO₂ で定義された(M[u],r[u]) を探索し， もし，

m= M[u]∧z=IV なるuが存在すれば，rEO2 はr[u]を出力する．

（b）rEO2は，v= 1からqE まで，rEO2 で定義された(ME[v],zE[v])を探索し，もし，

m= M_E[v]∧z= IV なるvが存在すれば，rEO₂はz_E[v]を出力する．

（c）rEO2 は，u = 1からqRまで，RO2 で定義された(M[u],r[u]) を探索し， もし，

ME = M[u]なるuが存在すれば，rEO2はr[u]を出力する．

（d）rEO₂は，v= 1からq_E まで，rEO₂ で定義された(M_E[v],z_E[v])を探索し，もし，

M_E = M_E[v]なるvが存在すれば，rEO₂ はz_E[v]を出力する．

（e）さもなくば，rEO2は，zE をDから一様ランダムに選択し，それを出力する．

注意1 ROの出力が衝突を起こす確率を評価することで，rEROとEROは観測等価であるこ とを証明できる．また，T ROとwT ROも，ROの出力が衝突を起こす確率を評価することで，

観測等価であることを証明できる．つまり，我々は，CryptoVerifで記述できる，新しい定義を 与えたといえる．

6.3 情報漏えいを伴うランダムオラクルモデルにおける自動

ドキュメント内 形式検証を活用した暗号システムの安全性証明技術 花谷 嘉一 (ページ 122-127)