OMHSO プロトコルの定式化

るときにのみ共有鍵を更新することで，同期のずれが広がることを防いでいる．さらに，ハッ シュ関数を利用した2種類のチャレンジ-レスポンスプロトコルを構成して，同期が1つだけ ずれたとしても正しく認証できるよう工夫が施されている．これらの工夫を組み合わせること で，通信のエラーや攻撃によりプロトコルが途中終了したとしても，高々１つしか同期にずれ は生じず，以降のセッションでも正常にプロトコルを実行できる．OMHSOプロトコルの基本 的な安全性要件は，OSKプロトコルの構造を利用して達成している．そして，サーバー側が 最新と直前の2つの共有鍵を持つことで，タグ側の計算効率を維持したままで，非同期耐性を 達成している．

そこで，鍵更新処理を省略した単純化OMHSOプロトコルを形式化し，CryptoVerifによる 検証結果を得た．

4.5.1.1 攻撃モデルの定式化

モデルの詳細は，次のとおりである．単純化したプロトコルは，OMHSOプロトコルと同 様に3種のランダムオラクルを用いる．単純化プロトコルは鍵の更新を行わないため，共有

鍵がRevealしたらいかなる安全性も満たさない．そのため，OMHSOプロトコルへの攻撃者

とは異なり，単純化プロトコルの攻撃者のRevealクエリは使用禁止とする．Revealクエリの 代わりに，攻撃者には，攻撃対象となるセッションの次のセッションのセッション鍵SK2は あらかじめ与えるようモデル化する．上記のようにモデル化することで，単純化プロトコルは

CryptoVerifによる検証を適用でき，さらに，その検証結果を利用して人手により所望の安全

性を示すことができた．

単純化プロトコルは，ランダムオラクルOH0,OH1,OH2，サーバーオラクルServer，タグオ ラクルTag，チャレンジオラクルChallengeの6種のオラクルからなる．ServerとTagは，そ れぞれ，攻撃モデル中で正しいサーバーと正しいタグの役割をするオラクルである．Challenge は安全性要件ごとに異なるが，その他のオラクルは全ての安全性要件で同じものを用いる．

以上のプロセスを用いて，攻撃ゲームを式(4.1)のように定式化する．

(input();

ID←^R IDs;seed←^R key;SK0←H2(seed,ID);

SK1← H₂(SK0,ID);SK2←H₂(SK1,ID);

return(ID,SK2);

(S erver|T ag|Challenge|OH₁|OH₂|OH₃)).

(4.1)

これは，攻撃対象のIDと攻撃対象の共有鍵を更新した鍵SK2を与えられたとき，Server， Tag，Challenge，OH₁,OH₂,OH₃ に任意の順序で問い合わせを行い，Challengeから与えられ る問題に対して，答えようとするゲームを意味している．ここで，input()は，通信要求のみ が入力され，データは入力されないことを意味し，以降の()も同様の意味とする．

以降では，CryptoVerifで検証を行うために定式化した各オラクルを与える．

4.5.1.2 ランダムオラクルの定式化

ランダムオラクルの形式化は，Blanchetら[24]が与えた形式化に簡単な拡張を施したもの を用いる．OMHSOプロトコルでは，次の3種のランダムオラクルH₀,H₁,H₂ を用いる^*2．た

*2 本来，H0,H1,H2 は，H0 : bitstring → h0,H1 : bitstring → h1,H2 : bitstring → key と定義される．こ れは，本章で用いる H₀,H₁,H₂ の定義とは異なっているが，要素の組を一意なビット列に変換する関数

だし，keyはセッション鍵の集合，IDsはIDの集合,そして，nonceはtビットのビット列の 集合とする.

H0 :key×IDs×nonce×nonce→ h0, H1 :key×IDs×nonce×nonce→ h1

H₂ :key×IDs→key.

OH0,OH1,OH2は，それぞれ，H0,H1,H2 に対応するランダムオラクルのプロセスとする．こ のとき，OH0 は，下記のように定式化できる．

foreach i_h ≤ n_hdoOH₀(k:key,ID:IDs,A:nonce,B:nonce) := return(H0(k,ID,A,B)) [all]

≈0 foreach i_h ≤n_h doOH₀(k:key,ID: IDs,A:nonce,B:nonce) := findu≤nh suchthat (defined(k[u],ID[u],A[u],B[u],r[u])∧k=^? k[u]

∧ID =^? ID[u]∧A=^? A[u]∧B=^? B[u])then return(r[u]) elser←^R h₀;return(r)

(4.2)

OH1,OH2も，同様に定式化する．

foreach i_h ≤ n_hdoOH₁(k:key,ID:IDs,A:nonce,B:nonce) := return(H1(k,ID,A,B)) [all]

≈0 foreach i_h ≤n_h doOH₁(k:key,ID: IDs,A:nonce,B:nonce) := findu≤n_h suchthat (defined(k[u],ID[u],A[u],B[u],r[u])∧k=^? k[u]

∧ID =^? ID[u]∧A=^? A[u]∧B=^? B[u])then return(r[u]) elser←^R h1;return(r)

(4.3)

foreach ih ≤ nhdoOH2(k:key,ID:IDs) := return(H2(k,ID)) [all]

≈0 foreach ih ≤nh doOH2(k:key,ID: IDs) :=

findu≤n_h suchthat (defined(k[u],ID[u],r[u])∧k=^? k[u]

∧ID =^? ID[u])then return(r[u]) elser←^R key;return(r)

(4.4)

2bs1 :key×IDs×nonce×nonce→bitstring，2bs2 :key×IDs→bitstringを定義し利用することで，本来のラ ンダムオラクルを用いて本章で与える攻撃モデルを記述できる．このようにモデルしたとしても，CryptoVerif で証明が可能であることを確認しているが，本章では，記述の理解しやすさため，直接的なランダムオラクル の記述を採用する．

4.5.1.3 補助関数test_n,test_h0,test_h1の定式化

OMHSOプロトコルのサーバーオラクルやチャレンジオラクルを愚直に定式化したとして

も，CryptoVerifでは正しく検証できない．そこで，次のような関数test1,test2,test3を用いる

ことで，CryptoVerifが検証できる定式化を与える．

まず，testn,testh₀,testh1 を定式化する．

test_n :bool×nonce×nonce→nonce, test_h0 :bool×h₀×h₀ →h₀,

test_h1 :bool×h₁×h₁ →h₁.

testn(b,A,B)は，あらゆるA,B∈nonceに対して，bがtrueならばAを出力し，bが f alseな らばBを出力する関数とする．b:boolが与えられたとき，A,B←^R nonceをランダムに選択し て，test(b,A,B)を出力するプロセスの出力値の分布は，b:boolが与えられたとき，C ←^R nonce をランダムに選択して，Cを出力するプロセスの出力値の分布と完全に一致する．つまり，こ の2つのプロセスは観測等価となる．式(4.5)は，この性質を定式化したものである．

foreach it ≤nt dotestn(b:bool) :=A,B←^R nonce;

return(testn(b,A,B))[all]

≈0 foreach it ≤ nt dotestn(b:bool) :=C ←^R nonce;return(C)

(4.5)

test2とtest3も同様に定義することで，下記のように観測等価となる．

foreach i_t ≤n_t dotest_h0(b:bool) := A,B←^R h₀; return(testn(b,A,B))[all]

≈0 foreach i_t ≤ n_t dotest_h0(b:bool) :=C ←^R h₀;return(C)

(4.6)

foreach i_t ≤n_t dotest_h1(b:bool) := A,B←^R h₁; return(testn(b,A,B))[all]

≈0 foreach i_t ≤ n_t dotest_h1(b:bool) :=C ←^R h₁;return(C)

(4.7)

4.5.1.4 サーバーオラクルの定式化

Serverオラクルを定式化する．まず，愚直に定式化したサーバーオラクルを与える．

foreach ip ≤ npdoS erver:=input(); Xs

←R nonce; return(Xs);

input(αs :nonce, βs :h0);ifβs

=? H0(SK1,ID,Xs, αs)then return(H₁(SK1,ID,X_s, αs))

else ifβs

=? H0(SK0,ID,Xs, αs)then return(H1(SK0,ID,Xs, αs))

elseZrnd

←R h1; return(Zrnd).

(4.8)

式(4.8)で与えたサーバーオラクルを用いて検証を行うと，CryptoVerifでは，単純化OMHSO

プロトコルが安全であることを検証できなかった．そこで，test_h1 を用いて，条件分岐を削減 した定式化を行う必要がある．

foreach ip ≤ npdoS erver:=input(); Xs

←R nonce; return(Xs);

input(αs :nonce, βs :h0);ifβs

=? H0(SK0,ID,Xs, αs)then return(H₁(SK0,ID,X_s, αs))

elseZrnd

←R h1;Zs ← H1(SK1,ID,Xs, αs);

bs :bool← (βs

=? H0(SK1,ID,Xs, αs));

return(test3(bs,Zs,Zrnd)).

(4.9)

式(4.9)を用いることで，CryptoVerifで検証することが出来た．

4.5.1.5 タグオラクルの定式化 Tagオラクルを定式化する．

foreach i_p ≤ n_pdoT ag:=input(X_t :nonce); αt

←R nonce;

βt ← H0(SK1,ID,Xt, αt);return(αt, βt);

input(Zt :h1);ifZt

=? H1(SK1,ID,Xt, αt)thenyield.

(4.10)

4.5.1.6 チャレンジオラクルの定式化

Challengeオラクルは，安全性要件ごとに異なるため，以降で，各安全性要件に対応した

Challengeプロセスを定義する．

■タグ識別不可能性の定式化 タグ識別不可能性の攻撃ゲームのためのChallengeオラクルを 定式化する．まず，サーバーオラクルの場合と同様に愚直に定式化したものを式 (4.11)に与

える．

Challenge:= input(X^∗ :nonce); b^∗ ← {^R true, f alse}; ifb^∗= truethen

α^∗ ←^R nonce; β^∗ ← H0(SK1,ID,X^∗, α^∗);

return(α^∗, β^∗) else

αrnd

←R nonce; βrnd

←R h0; return(αrnd, βrnd).

(4.11)

Challengeオラクルは，一様ランダムに選択したbがtrueの場合，正しいTagオラクルと同じ

出力を返すが，bがfalseの場合，ランダムな値を返す．もし，正しいタグの出力とランダム な出力を識別できる攻撃者が存在すると，bがtrueであるかfalseであるかを識別できる．つ まり，bが秘匿性を満たすとき，いかなる攻撃者もタグの出力とランダムな出力を識別するこ とができない．このとき，タグ識別不可能性を満たすという．

残念ながら，式(4.11) の定式化を用いても，CryptoVerifでは安全性が証明できなかった．

これは，式(4.11)のbが関わる条件分岐のために，CryptoVerifが行う Simplify処理により，

冗長な事象を単純化できなかったことが原因である．そこで，tsetn,testh1を使って，条件分岐 を削減した定式化を与える．

Challenge:= input(X^∗ :nonce); b^∗ ← {^R true, f alse}; α^∗ ←^R nonce;β^∗ ←H0(SK1,ID,X^∗, α^∗);

αrnd

←R nonce; βrnd

←R h0;

return(testn(b^∗, α^∗, αrnd),testh₀(b^∗, β^∗, βrnd));

(4.12)

式(4.12)は，式(4.11)と同様の処理を表現している．式(4.12)を用いることで，CryptoVerif でタグ識別不可能性を証明することが出来た．

■タグ成りすまし不可能性の定式化 タグ成りすまし不可能性の攻撃ゲームのための Chal-lengeプロセスを式(4.13)で定式化する．

Challenge:= input(); X^∗ ←^R nonce;return(X^∗);

input(α^∗:nonce, β^∗ :nonce);

ifβ^∗ =^? H0(SK1,ID,X^∗, α^∗)then

findu≤ npsuchthat(defined(Xt[u])∧X^∗ =^? Xt[u])thenyield elseevent bad

else ifβ^∗ =^? H0(SK0,ID,X^∗, α^∗)then

findu≤ npsuchthat(defined(Xt[u])∧X^∗ =^? Xt[u])then yield elseevent bad.

(4.13)

イベント “event bad” が生じるのは，Challengeプロセスが受け取った α^∗, β^{∗ が受理されて，}

Challengeプロセスが出力した X^∗ がTagプロセスに問い合わされていないときのみである．

つまり，“event bad”が生じることは，共有鍵SK0,SK1を与えられていない攻撃者が，サー

バーに受理される通信を行ったことを意味している．言い換えると，“event bad”が生じると き，攻撃者はタグの成りすましに成功している．いかなる攻撃者に対しても，“event bad”が生 じる確率が無視できるとき，タグ成りすまし不可能性を満たすという．

■サーバー成りすまし不可能性の定式化 サーバー成りすまし不可能性の攻撃ゲームのための Challengeプロセスを式(4.14)で定式化する．

Challenge:= input(X^∗ :nonce);

α^∗ ←^R nonce; β^∗ ← H0(SK1,ID,X^∗, α^∗);

return(α^∗, β^∗);

input(Z^∗ :h1);ifZ^∗ =^? H1(SK1,ID,X^∗, α^∗)then

findu≤np suchthat(defined(αs[u], βs[u])∧α^∗ =^? αs[u]∧β^∗ =^? βs[u])thenyield elseevent bad

(4.14)

イベント “event bad” が生じるのは，Challenge プロセスが受け取った Z^∗ が受理されて，

Challengeプロセスが出力したα^∗, β^∗がServerプロセスに問い合わされていないときのみであ る．つまり，“event bad”が生じることは，共有鍵SK1を与えられていない攻撃者が，タグに 受理される通信を行ったことを意味している．言い換えると，“event bad”が生じるとき，攻撃 者はサーバーの成りすましに成功している．いかなる攻撃者に対しても，“event bad”が生じ る確率が無視できるとき，サーバー成りすまし不可能性を満たすという．

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