CanettiKrawczykモデル - 暗号理論教室

---

プロトコルの実行モデル

まず、一般にプロトコル実行のモデルを用意する。

プロトコルを実行する各パーティは（入力テープからの）実行要求や
（入力メッセージテープからの）入力メッセージを受け取ると、
あらかじめ定められたコードに従って、
出力メッセージや出力値を計算する対話的チューリング機械と考える。

UM モデル (Unauthenticated-link Model)

プロトコル実行のマルチセッションモデル。

• プロトコル実行は攻撃者が指示する。
  • 各セッションは攻撃者による実行要求によって、指定された参加者間で実行される。
• 参加者間のメッセージは攻撃者が配送する。
  • このとき、メッセージは攻撃者によって改ざんされる可能性がある。
  • また、偽メッセージが挿入されたり、送ったはずのメッセージが欠落する可能性がある。
• さらに、攻撃者はコラプト・セッション状態開示・セッション出力開示の各クエリを実行し、
  • 任意のパーティの秘密鍵・セッション状態・セッション出力を知ることができる。

[参加エンティティ]

• プロトコルπの参加者 P₁, ... , P_n
  • 各P_iの入力は x_i.
• UM攻撃者U
• 初期化関数 I

[プロトコル実行]

• 初期化:
  • 各P_iは入力x_iでプロトコルπ(P_i)を呼び出す。
  • 各P_iは I(r, k)_i を、攻撃者Uは I(r, k)₀ を得る。
  • (rはランダムテープ、kはセキュリテイパラメータ)
• 停止するまで、攻撃者Uは：
  • 実行要求または（あるP_jを送信者と指定した）入力メッセージによって、あるパーティP_iを活性化してよい：
    • 活性化されたP_iは、そのコードπに従って計算を行う。
    • 実行要求または出力メッセージをUに返す。
    • 「秘密」ラベルをもたないローカル出力もUに返す。
  • あるパーティP_iをコラプトしてよい：
    • UはP_iの（長期的な秘密情報を含む）状態を知る。
    • コラプトされたことを示す特殊なメッセージがP_iのローカル出力に追加される。
    • これ以降、パーティP_iが再び活性化されることはない。
    • とくに、これ以降、P_iのローカル出力への書き込みは発生しない。
  • あるパーティP_i内のあるセッションについてセッション状態開示クエリを発行してよい：
    • UはP_iの該当セッションの（長期的な秘密情報は含まない）セッション状態を常に知る状態となる。
    • 該当セッションが開示されたことを示す特殊なメッセージがP_iのローカル出力に追加される。
    • 以降、このセッションでは、P_iのローカル出力への書き込みは発生しない。
  • あるパーティP_i内のあるセッションについてセッション出力開示クエリを発行してよい：
    • UはP_iの該当セッションの秘密ラベルつきローカル出力を知る。
    • 該当セッションが出力クエリを受けたことを示す特殊なメッセージがP_iのローカル出力に追加される。
• Uと各パーティの出力を連結した大域出力UNAUTH_π,Uを出力する:
  • UNAUTH_π,U(k, x, r) = UM-ADV_π,U(k,x,r) | UNAUTH_π,U(k,x,r)₁ | ... | UNAUTH_π,U(k,x,r)_n
    • (x = x₁...x_n, r = r₀r₁...r_n ).

[確率変数UNAUTH_π,U]

• UNAUTH_π,U =^def { UNAUTH_π,U(k,x,r)}_k∈N,x∈B*.

AMモデル (Authenticated-link Model)

以下を除いてUMモデルと同じ：

• AM攻撃者Aが（まだコラプトされていないパーティP_jが送信者として指定された）入力メッセージによって
• パーティP_iを活性化するとき、そのメッセージは実際にP_jが生成したものでなければならない。
  • すなわち、Aによるメッセージの改ざんや偽メッセージの挿入は許されない。
• さらに、Aは各メッセージを（配送するとしたら）高々1回のみしか配送できない。
  • すなわち、Aによるメッセージの再送は許されない。
• ただし、送ったはずのメッセージの欠落はあり得る。

[確率変数AUTH_π,U]

• AUTH_π,A =^def { AUTH_π,A(k,x,r)}_k∈N,B*.
  • AUTH_π,A(k, x, r) = AM-ADV_π,A(k,x,r) | AUTH_π,A(k,x,r)₁ | ... | AUTH_π,A(k,x,r)_n.
    • (x = x₁...x_n, r = r₀r₁...r_n ).

鍵共有プロトコル

鍵共有プロトコルの実行モデル

[実行要求]

• (establish_session, P_i, P_j, s)
  • パーティP_iに対し, パーティP_jとの間でセッション鍵を共有することを要求する。
  • sはセッション識別子を表す。
  • 同一参加パーティ集合{P_i, P_j}について、セッション識別子の重複した実行要求は許されない。

[ローカル出力]

• (P_i, P_j, s, κ)

ただし、セッション鍵κは秘密ラベルを持つ。

[攻撃者Uの追加アクション]

• あるパーティP_iにセッション失効クエリを発行していよい：
  • パーティP_i内のすべての完了セッション(P_i, P_j, s)について、
    • このセッション鍵κはP_iのメモリから消去される。
    • このセッションは「失効」ラベルをもつ。
• 攻撃者Uは失効セッションに対し
  • セッション鍵クエリ（セッション出力開示クエリ）は許されない。
  • コラプトしても、そのセッション鍵は入手できない。

鍵共有プロトコルの安全性定義

２つのセッション(P_i, P_j, s)と(P_j, P_i, s')は
同じセッション識別子をもつ（s=s' である）とき
マッチングしているという。

パーティP_i内の鍵共有セッション(P_i, P_j, s)が局所暴露であるとは、
攻撃者Uがこのセッションに対し、以下のいずれかのアクションを実行したことを意味する：

• セッション状態開示クエリを発行
• セッション出力開示クエリを発行
• セッションが失効する前に、パーティP_iをコラプト。

鍵共有セッションが暴露であるとは、
該当セッションまたはそのマッチチングセッションが局所暴露であることをいう。

攻撃者Uの追加アクション：

• Uは任意の時点で１度だけ、テストセッションクエリを発行する：
  • Uは完了・未失効・未暴露のセッションを一つ選択する。
  • b ← {0,1}
    • b =^? 0 : Uにランダムストリング r を渡す。
    • b =^? 1 : Uに該当セッションのセッション鍵κを渡す。
  • 以降、Uはテストセッション（とそのマッチングセッション）を暴露することはできない。
    • ただし、テストセッションを失効させたのちは、テストセッションのピアをコラプトしてもよい。
  • 終了時にUはビットb' を出力する。

定義(SK安全)
鍵共有プロトコルπがSK安全であるとは、
どのような攻撃者Uについても、

• 完全性： πの実行において、
  • コラプトされていない2パーティがマッチングセッションを完了したら、それらのセッション鍵は一致し、
• 秘匿性： πの実行に対するテストセッションクエリにおいて、
  • Pr[ b' = b ] ≦ 1/2 + (あるネグリジブル関数).

であることをいう。

注意(フォワード秘匿性)
失効クエリを用いることができる攻撃者Uは、
それによってテストセッションを失効させ、その後、当該ピアをコラプトすることができる。
よって、鍵共有プロトコルがSK安全であるには、テストセッションのセッション鍵は、
（セッション完了後に）攻撃者Uが当該ピアの長期秘密情報を入手しても、守られなければならないことになる。

定義(フォワード秘匿性なしのSK安全)
鍵共有プロトコルπがフォワード秘匿性なしのSK安全であるとは、
πが、失効クエリを用いない任意の攻撃者UについてSK安全であることをいう。

安全な鍵共有プロトコルの構成

プロトコル 2DH

プロトコル 2DH：

• [部品] 群生成アルゴリズム GenG
• [初期化] (q, g) ← GenG(1^k) は（初期化関数Iに含まれる）公開パラメータ。
• [イニシエーター P_i の入力] 実行要求 (establish_session, P_i, P_j, s)
• [レシーバー P_j の入力] 実行要求 (establish_session, P_i, P_j, s)
• [プロトコル]　※ (P_i, s, α), (P_j, s, β).
  • P_i → P_j：x ← Z_q,　α = g^x,　(P_i, s, α)を送信。
  • P_j → P_i：y ← Z_q,　β = g^y,　(P_j, s, β)を送信するとともに、
    • γ = α^yを計算し, yを消去。(P_j, P_i, s, γ)を出力。
  • P_i : γ' = β^xを計算し, xを消去。(P_i, P_j, s, γ')を出力。

定理(2DH)
GenGに対する判定DH仮定のもとで、
鍵共有プロトコル2DHはAMモデルにおいてSK安全である。

証明

プロトコル SIG-DH

プロトコル SIG-DH：

• [部品] 群生成アルゴリズム GenG,　ディジタル署名 Σ=(Gen, Sign, Verify)
• [初期化] (q, g) ← GenG(1^k)、各パーティごとに (sk_i, vk_i) ← Gen(1^k).
• [イニシエーター P_i の入力] 実行要求 (establish_session, P_i, P_j, s)
• [レシーバー P_j の入力] 実行要求 (establish_session, P_i, P_j, s)
• [プロトコル]　※ (P_i, s, α), (P_j, s, β, σ),　(P_i, s, σ').
  • P_i → P_j : x ← Z_q,　α = g^x,　(P_i, s, α)を送信。
  • P_j → P_i : y ← Z_q, β = g^y, σ ← Sign(sk_j, (P_j,s,β,α,P_i))
    • (P_j, s, β, σ)を送信するとともに、γ = α^yを計算し, yを消去。
  • P_i → P_j :
    • Verify(vk_j, (P_j,s,β,α,P_i), σ) =^? 1 ならば、
      • γ = β^xを計算し, xを消去。σ' ← Sign(sk_i, (P_i,s,α,β,P_j))　
      • (P_i, s, σ')を送信するとともに、(P_i, P_j, s, γ)を出力。
  • P_j :
    • Verify(vk_i, (P_i,s,α,β,P_j), σ') =^? 1 ならば、(P_j, P_i, s, γ)を出力。

定理(SIG-DH)
GenGについて判定DH仮定が成り立ち、
ディジタル署名Σが適応的選択文書攻撃において存在的偽造不可ならば、
鍵共有プロトコルSIG-DHはUMモデルにおいてSK安全である。

証明

セキュアチャネル

安全な鍵共有プロトコルを部品として用いて、
セキュアチャネル（認証チャネルや秘匿チャネル）を構成する。

プロトコルエミュレーション

定義(Emulation)
プロトコルπがプロトコルπ' をエミュレートするとは、
任意のUM攻撃者Uに対し、あるAM攻撃者Aがあって、

• AUTH_π,A ≡_c UNAUTH_π',U

であることをいう。

注意
このとき、プロトコルπ'をUMモデルで攻撃するどのような攻撃者Uであっても、
それができることは、プロトコルπをAMモデルで攻撃して実現できることでしかない。
つまり、攻撃者Uにとってプロトコルπ'は、AMモデルにおけるプロトコルπと同じ。

認証チャネル

認証チャネルの安全性定義

プロトコル SMT：

• P_iは、実行要求(establish-session, P_i, P_j, s) を受け取ると、
  • (established, P_j, s)をローカル出力に記録。
• P_iは、実行要求(expire-session, P_i, P_j, s) を受け取ると、
  • (established, P_j, s)がローカル出力に記録されていたら、
    • (expired, P_j, s)をローカル出力に記録。
• P_iは、実行要求(send, P_i, P_j, s, m) を受け取ると、
  • ローカル出力に(established, P_j, s)が存在し、(expired, P_j, s)が存在しないなら、
    • メッセージ (P_i, s, m) をP_jに送信。
    • (sent, P_j, s, m)をローカル出力に記録。
• P_iは、入力メッセージ(P_j, s, m) を受け取ると、
  • ローカル出力に(established, P_j, s)が存在し、(expired, P_j, s)が存在しないなら、
    • (received, P_j, s, m) をローカル出力に記録。

プロトコル NetChan：

• [部品] 鍵共有プロトコル π,　鍵付き関数 snd, rcv
• [初期化] πの初期化関数Iを実行し、必要な情報を必要なパーティに配布。
• [プロトコル]
  • P_iは、実行要求(establish-session, P_i, P_j, s) を受け取ると、
    • パーティP_jとの間で、(P_i, P_j, s)を入力として鍵共有プロトコルπを実行し、セッション鍵κを得る。
    • (established, P_j, s)をローカル出力に記録し、(key, P_j, s, κ)を保存。
  • P_iは、実行要求(expire-session, P_i, P_j, s) を受け取ると、
    • (established, P_j, s)がローカル出力に記録されていたら、
      • (key, P_j, s, κ)を消去し、(expired, P_j, s)をローカル出力に記録。
  • P_iは、実行要求(send, P_i, P_j, s, m) を受け取ると、
    • ローカル出力に(established, P_j, s)が存在し、(expired, P_j, s)が存在しないなら、
      • (key, P_j, s, κ)を検索し、m' = snd_κ(m)を計算し、メッセージ (P_i, s, m') をP_jに送信。
      • (sent, P_j, s, m)をローカル出力に記録。
  • P_iは、入力メッセージ(P_j, s, m') を受け取ると、
    • ローカル出力に(established, P_j, s)が存在し、(expired, P_j, s)が存在しないなら、
      • (key, P_j, s, κ)を検索し、(m, ok) = rcv_κ(m')を計算する。
      • ok = 1 ならば、(received, P_j, s, m) をローカル出力に記録。

定義(認証チャネル)
プロトコルNetChan(π,snd,rcv)が認証チャネルであるとは、
それがプロトコルSMTをエミュレートすることをいう。

注意
このとき、攻撃者Uにとって、プロトコルNetChan(π,snd,rcv)は
AMモデルにおけるプロトコルSMTと同じ。
すなわち、プロトコルNetChan(π,snd,rcv)は理想的な認証チャネルを実現している。

安全な認証チャネルの構成

プロトコル NetAuth：

• [部品] 鍵共有プロトコル π, 認証子生成関数 f
• [プロトコル] NetAuth(π, f) := NetChan(π, snd, rcv) :
  • snd_κ(m) :
    • return (m, f_κ(m)).
  • rcv_κ(m'=(m,t)) :
    • mがフレッシュ（同じセッション内で受け取ったどのメッセージとも異なる）で、かつ t =^? f_κ(m) ならば、
      • ok = 1、そうでないならば ok = 0
    • ok = 1 ならば v = m、 そうでないならば v = ⊥
    • return (v, ok).

定理(安全な認証チャネル)
鍵共有プロトコルπがUMモデルにおいてSK安全で、
認証子生成関数fが選択文書攻撃で安全ならば、
プロトコルNetAuth(π,f)は認証チャネルである。

証明

秘匿チャネル

秘匿チャネルの安全性定義

NetChan(π,snd,rcv)に対する攻撃者Uの追加アクション：

• Uは任意の時点で１度だけ、テストセッションクエリを発行する：
  • Uは完了・未失効・未暴露のセッション(P_i, P_j, s)を一つ選択する。
  • さらに、Uは2つの異なる(同じ長さの)メッセージm₀とm₁を出力する。
  • b ← {0,1}
  • P_iを(send, P_i, P_j, s, m_b)で活性化する。
    • ただし、例外的に、これによってP_iやP_jのローカル出力にm_bは書き込まれないとする。
  • 以降、Uはテストセッション(P_i, P_j, s)（とそのマッチングセッション）を暴露することはできない。
    • ただし、テストセッションを失効させたのちは、テストセッションのピアをコラプトしてもよい。
  • 終了時にUはビットb' を出力する。

定義(秘匿チャンネル)
NetChan(π,snd,rcv)が秘匿チャネルであるとは、
どのような上記追加アクションが許されたUMモデルにおける攻撃者Uについても、

• Pr[ b' = b ] ≦ 1/2 + (あるネグリジブル関数).

であることをいう。

定義(セキュアチャンネル)
NetChan(π,snd,rcv)がセキュアチャネルであるとは、

• それは認証チャネルであって、
• 秘匿チャネルでもある

ことをいう。

安全な秘匿チャネルの構成

プロトコル NetSec

• [部品] 鍵共有プロトコル π, 認証子生成関数 f , 共通鍵鍵暗号 Enc, 疑似ランダム関数 F
• [プロトコル] NetSec(π, f) = NetChan(π, snd, rcv) :
• snd_κ(m = (m-id, m-pl)) :
  • κ_e = F_κ(0), κ_a = F_κ(1)
  • c = Enc(κ_e, m-pl), t = f(κ_a, m-id, c)
  • return (m-id, c, t).
• rcv_κ(m'=(m-id,c,t))
  • κ_e = F_κ(0), κ_a = F_κ(1)
  • ok = 1 ⇔ 『m-id ≠ 同じセッション内で以前に受け取ったどのメッセージのid、t = f(κ_a, m-id, c)』
  • ok =^? 1 : m-pl = Enc^-1(κ_e, c), m = (m-id, m-pl)
  • else ok =^? 0 : m = ⊥
  • return m.

定理(NetSec)
鍵共有プロトコルπがUMモデルにおいてSK安全で、
認証子生成関数 f が選択文書攻撃において偽造不可能で、
共通鍵暗号 Enc が選択平文攻撃において識別不可能で、
Fが疑似ランダム関数ならば、
プロトコルNetSec(π, f, Enc, F)はセキュアチャネルである。

証明

上へ

---