定理(NetSec)の証明のアイデア
プロトコルNetSec(π,f)は、指定された2者間で、
- 鍵共有プロトコルπを用いてセッション鍵κを共有し、
- κを疑似ランダム関数Fのシードとして用いて、2つのストリングκe, κaを生成し、
- 送信メッセージm = (m-id, m-pl)に対し、
- メッセージ識別子 m-id について、κaを鍵とするメッセージ認証子t=fκa(m-id)を付加し、
- ペイロード m-pl はκeを鍵として共通鍵暗号で暗号化する。
プロトコルNetSec(π,f)について、
- 部品である鍵共有プロトコルπのSK安全性より、攻撃者にとってセッション鍵κは未知の乱数。
- よって、κe=Fκ(0)もκa=Fκ(1)も未知の乱数。
- κaを知らない攻撃者はメッセージ認証子を偽造できない。
- よって、攻撃者はメッセージの改ざん・挿入はできない。
- κeを知らない攻撃者は暗号文cをみてもペイロードm-plの情報は得られない。
定理(NetSec)の証明
- 定理(安全な認証チャネル)より、NetSec(π, f)は認証つきチャネル。
- プロトコルNetSec(π, f)が秘匿チャネルであることを示せばよい。
- (κe, κa)はまとめてπによって直接生成されているとしてよい。※ Fは疑似ランダム関数
NetSec(π, f)に対する任意のUM攻撃者をUとする。
Uを用いて共通鍵暗号Encに対する選択平文攻撃者Bを構成する。
選択平文攻撃者B:
- ※ 暗号化オラクルEncκ(・)を用いて、Encを選択平文攻撃したい。
- Uを起動する。
- セッション(Pi, Pj, s0)をランダムに選択する。
- Uに対し、セッションs0以外のセッションについては、オネストにシミュレートする。
- セッション(Pi, Pj, s0)について、
- 以下を除いて、オネストにシミュレートする：
- (Pi, Pj)間でオネストに鍵共有プロトコルπをシミュレートする。
- （これによって生成されたセッション鍵を(κe,κa)とおく。）
- Uが実行要求(send, Pi, Pj, s0, m=(m-id,m-pl))を発したら、
- m-plを自身の暗号化オラクルEncκ(・)に発し、cを受け取る。
- t = f(κa, m-id, c)
- Pj宛てメッセージ (Pi , s0, m'=(m-id,c,t))をUに渡す。
- UがPj宛てメッセージ(Pi , s0, m'=(m-id', c', t'))を発したら、
- m-id'のフレッシュネスとt' = f(κa, m-id', c') を確認する。
- m-plをPjのローカル出力に書き込む。
- ※ NetSec(π, f)は認証チャネルなのでUはcを書き換えられない
- Uが(Pi, Pj, s0)をテストセッションに指定したら、
- ※ s0以外をテストセッションに指定したらランダムビットb' を出力してアボート
- Uより、m0 = (m-id*, m0-pl), m1 = (m-id*, m1-pl)を受け取り、
- (m0-pl, m1-pl)を自身のチャレンジオラクルに発し、暗号文c*を受け取る。
- κaを用いて(m-id*,c*)のタグt*を計算し、
- メッセージ (Pi , s0, (m-id*,c*,t*)) のPjへの送信をシミュレートする。
- Uがb' を出力として停止したら、b' を出力して停止する。
[攻撃者Bの解析]:
κ=κeの条件のもとで、 テストセッションのランダム推測が当たれば(確率1/l)、
BのUに対するシミュレートは完ぺき。よって、
- Pr[Bが識別に成功 | κ=κe] ≧ (1-1/l)・(1/2) + (1/l)・Pr[Uが識別に成功].
一方、πのSK安全性より、
- Pr[Bが識別に成功] ≧ Pr[Bが識別に成功 | κ=κe] - (ネグリジブル)1
- ※ 定理(認証つきチャネル)の証明と同様にして、Bを用いてπのSK安全性に対する攻撃者を構成できる
以上より、Uの識別利得をεとするとき、
- Pr[Bが識別に成功]≧ (1-1/l)・(1/2) + (1/l)・Pr[Uが識別に成功] - (ネグリジブル)1.
仮定よりBは選択平文攻撃で安全なので、
- Pr[Bが識別に成功] = 1/2 + (ネグリジブル)2 .
よって、
- 1/2 + (ネグリジブル)2 ≧ (1-1/l)・(1/2) + (1/l)・(1/2 + ε) - (ネグリジブル)1
- (ネグリジブル)1 + (ネグリジブル)2 ≧ ε/l.
よって、εもネグリジブル。
Q.E.D.
最終更新：2009年12月16日 18:40
