一方向性の定式化

計算量的仮定である一方向性の定式化について記す．

■計算量的モデルにおける定式化 まず，計算量的モデルにおける定式化を記す．

集合D上の置換族P^は，次の3つのアルゴリズムで定義される．

• ^{鍵生成アルゴリズム}kgen: seedrを入力として，公開鍵と秘密鍵のペア(pk,sk)を生成 するアルゴリズム．このアルゴリズムは，公開鍵生成アルゴリズムpkgenと秘密鍵生 成アルゴリズムskgenの2つのサブアルゴリズムに分けることができる．公開鍵pkに よって，D上の置換 fpkが定まる．

• evaluationアルゴリズム f :公開鍵pkと値 x∈ Dを入力として，y= fpk(x)を出力する アルゴリズム．

• inversionアルゴリズムinv f :要素yと落とし戸情報skを入力されると，yに対応する fpkの逆写像xを出力するアルゴリズム．

これらのアルゴリズムは，効率的に実行できることが必要である．“一方向性”では，ある効率 的なアルゴリズムが“存在しない”ことが求められるため，定式化はやや複雑になる．

定義4 (一方向性)高々時間tで動作するいかなる確率的多項式時間Turing機械A^{を以ってし} ても，

Pr









r←^R seed,

(pk,sk)←kgen(r), x←^R D,y← f_pk(x) x^′ ← A(pk,y) : x= x^′









 ≤ϵ (3.5)

が成立するとき，置換族P={fpk}^は(t, ϵ)-一方向性安全であるという．また，A^の時間t以内 での最大の成功確率をSucc^OW_P (t)と書く．

■Blanchetの枠組みにおける定式化 Blanchetの枠組みにおいて一方向性を取り扱うための

定式化を行う．最初に，次のように変数の型と記号を定義する．

定義5 (型と記号)

• seed:large,fixed-length型

L:foreachi_k ≤n_kdor ←^R seed; (O_pk:= return(pkgen(r))

|foreachif ≤nf dox←^R D; (Oy() :=return(f(pkgen(r),x))

|foreachi₁ ≤ n₁doO_eq(x^′ :D) :=return(x^′ =^? x)

|Ox() :=return(x))).

≈p^OW

R:foreachi_k≤ n_kdor←^R seed; (Opk :=return(pkgen(r))

|foreachif ≤nf dox←^R D; (Oy() :=return(f(pkgen(r),x))

|foreachi1 ≤n1doOeq(x^′ :D) :=

if defined(k)then return(x^′ =^? x)else return(false)

|Ox() :=k← mark;return(x))).

図3.2 Definition of Onewayness for CryptoVerif.

• pkey:公開鍵空間の型

• skey:秘密鍵空間の型

• D:置換の定義域

• skgen: seed→ skey

• pkgen: seed→ pkey

• f:pkey×D→ D

• invf:skey×D→ D

skgen は 秘 密 鍵 を 生 成 し ，pkgen は 公 開 鍵 を 生 成 す る ア ル ゴ リ ズ ム で あ る ．pk ← pkgen(r),sk← skgen(r)のとき，各pkについて，x7→f(pk,x)は置換族P^に属する D上の置 換であり，その逆置換は x7→invf(sk,x)である．

これらの記号を用いて，観測等価性を満たす定式化を行ったものを図3.2に示す．図3.2の 定式化では，ただ1つの公開鍵に対してだけではなく，n_k個の公開鍵を考慮している．

左辺Lの構成は次の通りである．まず，オラクルOpk[ik]は，公開鍵pkgen(r[ik])を出力す る．次に，x[ik,if]がランダムに選ばれた後，3つのオラクルOy[ik,if],Oeq[ik,if,i1],Ox[ik,if] が利用できるようになる．O_y[i_k,i_f]は，問い合わせに対して f(pkgen(r[i_k]),x[i_k,i_f])の像を 出力する．Oeq[ik,if,i1]は，x[ik,if]を受け取ったらtrueを返し，それ以外の入力に対しては falseを返す．Ox[ik,if]は，問い合わせに対して x[ik,if]を返す．

一方，右辺 R は，次のような構成になっている．O_x[i_k,i_f] において k[i_k,i_f] を導入し，

O_x[i_k,i_f]への問い合わせの有無を記録するよう変更した．そして，O_eq[i_k,i_f,i₁]をk[i_k,i_f]が

未定義の場合，常にfalseを返すように変更している．

置換族P= {fpk}^は(t, ϵ)-一方向性安全であるとき，図3.2に示したプロセス L,Rが確かに 観測等価性を満たすことを示し，その際の p^OW を評価するために，以下の補題を示す．

定義5によって定まる置換族P^が(t,Succ^OW_P )-一方向性安全のとき，以下の補題が成立する．

補題5 時間t以内で動作するいかなるContextCに対しても，

Pr





C







LR: Ogen() := r0

←R seed;x0

←R D;

return(pkgen(r₀),f(pkgen(r₀),x₀));

Oeq(x^′ : D) :=ifx^′ =^? x0then eventinvert.





 eventinvert





≤ Succ^OW_P (3.6)

が成立する．

証明：オラクルO_genはpkgen(r₀)として置換族P^より置換f(pkgen(r₀),)を一つ定め，pkgen(r₀) と，D上の値x0 を置換した値f(pkgen(r0),x0)を出力する．オラクルOeq はD上の値x^′ を受 けとり，x^′ = x0 ならばeventinvertを起こす．

もし，置換族P^が(t,Succ^OW_P )-一方向性安全ならば，定義4より x^′ = x₀ なるx^′ を見つけら れる確率は高々Succ^OW_P (t)である．

次に，一方向性に対する能動的攻撃ゲームのプロセスLR^′ を考える．LR^′ は，LRと同様に 一方向性に対する攻撃成功の条件を満たしたとき，eventinvertが起こるゲームで，O_xに問い 合わせていないyに対応する xをOeq^′ に入力したとき攻撃成功となる．

LR^′ :Ogr() :=r ←^R seed;pk← pkgen(r);return;

(Opk := return(pk)

|foreachif ≤ nf doOgx() := x←^R D;y←f(pk,x);return;

(O_y() := return(y)

|foreachi₁ ≤ n₁doO_eq′(x^′ :D) := if defined(k)then return(x^′ =^? x) else if(x^′ =^? x)then eventinvert else return(false)

|Ox() :=k← mark;return(x))).

(3.7)

LR^′ に対して次の補題が成り立つ．

補題6 プロセスLR^′ においてi_f =aで初めてeventinvertが起こる場合，次のようなContext

C_a によるプロセスC_a[LR]は，LR^′ を完全にシミュレートする． 

fora∈[1,nf]

Ca = newOracleOgen;newOracleOeq; ( Ogr() :=(pk,y)←Ogen();return;

(Opk :=return(pk)

|foreachif ≤nf doOgx() :=

ifi_f =athen return; (O_y :=return(y)

|foreachi₁ ≤n₁doO_eq′(x^′ :Gp) :=O_eq(x^′)else return(false)) else x←^R D;return; (Oy :=return(f(pk,x))

|foreachi1 ≤n1doOeq^′(x^′ :Gp) :=return(x^′ =^? x)

|Ox() := return(x)))). 

(3.8)

証明：C_a[LR]とLR^′ のオラクル呼び出し時の動作を比較する．

• O_gr が呼ばれたとき

– LR^′:ランダムにr∈ seedを選び，empty messageを返す．

– Ca[LR]: Ogen を呼び出す．Ogen はランダムに r ∈ seed,x0

←R D を選び，pk ← pkgen(r),^として，(pk,f(pk,x₀))を返す．C_a[LR]は，empty messageを返す．

共にempty messageを返すので，識別できない．

• Opkが呼ばれたとき

– LR^′:pk← pkgen(r)を返す．

– C_i[LR]:O_gen より受け取ったpkを返す．

どちらの出力も共に，Ogr の呼び出し時に seedからランダムに選ばれた要素より計算 されるため識別できない．

• O_gx[i_f]が呼ばれたとき

– LR^′: x[if]∈D]をランダムに選び，empty messageを返す．

– Ca[LR]: if , a のとき， x[if] ∈ D をランダムに選び，empty message を返す．

i_{f a}= aのとき，empty messageを返す．

共にempty messageを返すので，識別できない．

• Oy[if]が呼ばれたとき

– LR^′:f(pk,x[i_f])を返す．

– Ca[LR]: if , aのとき，f(pk,x[if])を返す．if = a のとき，Ogen より受け取った f(pk,x0)を返す．

どちらの出力も共に，seedからランダムに選ばれた要素と Dからランダムに選ばれた 要素から計算されるため，識別できない．

• Oeq^′[if,i1]が呼ばれたとき

– LR^′:if , aのとき，x^′ =^? x[if])を返す．if =a∧x^′ = x[if]のとき，eventinvertを 実行する．i_f = a∧x^′ , x[i_f]のとき，falseを返す．

– Ca[LR]: if , a のとき， x^′ =^? x[if])を返す．if = a のとき，Oeq[if,i1](x^′) を返 す．Oeqは x^′ = x0 のとき，eventinvertを実行し，x^′ , x0)のとき通常終了する．

C_a[LR]は，O_eqが通常終了したとき，falseを返す．

どちらの出力も共に，seedからランダムに選ばれた要素と Dからランダムに選ばれた 要素から計算されるため，識別できない．

• O_z[i_f]が呼ばれたとき – LR^′: x[if]を返す．

– Ca[LR]: x[if]を返す．

仮定より，(i_{f a},i_{f b})= (i, j)ではdefined(k)=0でなければならないため，O_z[i_{f a},i_{f b}]は 呼び出されない．(i_{f a},i_{f b}),(i, j)では，どちらの出力も共に，seedからランダムに選ば れた要素と[1,|Gp|]からランダムに選ばれた要素から計算されるため，識別できない．

以上より，if =aまで各オラクルの動作において完全に識別できないことが示せた．

LR^′ において，eventinvertの起こる確率は，次のようになる．

補題7 置換族P^が(t,Succ^OW_P )-一方向性を満たすならば，

∑

E,^invert∈E

Pr[C[LR^′] E]≤ nf ×Succ^OW_P (t+tC_a)． (3.9)

証明：補題5，補題6より，

∑

E,^invert∈E

Pr[C[LR^′] E]= ∑

a∈[1,nf]

∑

E,^invert∈E

Pr[C[Ca[LR]] E]

≤ ∑

a∈[1,n_f]

Succ^OW_P (t+t_Ca)

= nf ×Succ^OW_P (t+tC_a)．

(3.10)

また，L,R,LR^′ の間には次の補題が成り立つ．

補題8 n_k 個の LR^′ のコピーにおいて，event invertをreturn(true)かreturn(false)で置き換 えると，

(nk×LR^′){return(true)/eventinvert} ≈0 L (3.11) (nk×LR^′){return(false)/eventinvert} ≈0 R (3.12)  が成立する．

証明：LR^′ のeventinvertをreturn(true)で置き換えると，そのOeq^′ は，

if defined(k)then return(x^′ =^? x) else if(x^′ =^? x)then return(true) else return(false)

(3.13)

⇐⇒

if defined(k)then return(x^′ =^? x) else return(x^′ =^? x)

(3.14)

⇐⇒

return(x^′ =^? x) (3.15)

となる．また，pk,yに値を代入せずに，その値を直接プロセスで使っても振る舞いは変わらな いので，

(n_k×LR^′){return(true)/eventinvert} ≈0 L (3.16) が成り立つ．同様にLR^′ のeventinvertをreturn(false)で置き換えると，そのO_eq′ は，

if defined(k)then return(x^′ =^? x) else if(x^′ =^? x)then return(false) else return(false)

(3.17)

⇐⇒

if defined(k)then return(x^′ =^? x)

else return(false) (3.18)

となり，pk,yに値を代入せずに，値を直接プロセスで使っても振る舞いは変わらないので，

(n_k×LR^′){return(false)/eventinvert} ≈0 R (3.19) が成り立つ．

以上の補題より，図3.2に対して次の定理を示すことができる．

定理1 図3.2の式について，置換族P^が(t,Succ^OW_P )-一方向性安全ならば，

p^OW =nk×nf ×Succ^OW_P (t+(nknf −1)tf +(nk−1)tpkgen) (3.20) となる．ただし，tf はfの計算時間，tpkgen はpkgenの実行にかかる時間である． 

証明：L≈p^OW Rなる p^OW を評価する．

LR^′ がeventinvertを実行する確率をp^′ とすると，補題2より

(n_k×LR^′){return(true)/eventinvert} ≈p^′ (n_k×LR^′){return(false)/eventinvert} (3.21) となる．よって，補題8より，

L≈p^′ R (3.22)

となる．

また，補題3,補題7より，nk×LR^′ がeventinvertを実行する確率 p^′ は高々 

p^′ =n_k×n_f ×Succ^OW_G (t+t_Ca +(n_k−1)t_LR′) (3.23) である．ただし，

tLR^′ = tpkgen+nftf. (3.24)

よって，

t^′ =tCa +(nk−1)tLR^′ =(nknf −1)tf +(nk−1)tGgen (3.25) とおくと，

p^OW(t)= p^′(t)= n_k×n_f ×Succ^OW_P (t+(n_kn_f −1)t_f +(n_k−1)t_pkgen) (3.26) となる．

各オラクルはただ1つのreturn命令で構成されなければならないという制限によって，暗 号プリミティブを定義する多くの等価性をモデル化でき，一般的なプロセスの文法を使ってプ ロセスの書き換えを単純化することが可能となる．

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