定理(安全な認証チャネル)の証明 - 暗号理論教室

定理(安全な認証チャネル)の証明のアイデア

プロトコルNetAuth(π,f)は、指定された2者間で、

• 鍵共有プロトコルπを用いてセッション鍵κを共有し、
• 送信メッセージmに対し、そのκを鍵とするメッセージ認証子t=f_κ(m)を付加し、
• 正しいメッセージ認証子tをもつフレッシュな受信メッセージのみ受け入れる。

プロトコルNetAuth(π,f)について、

• 部品である鍵共有プロトコルπのSK安全性より、攻撃者にとってセッション鍵κは未知の乱数。
• セッション鍵κを知らない攻撃者はメッセージ認証子を偽造できない。
• よって、攻撃者は送信者のメッセージを改ざんしたり、送信者の生成していないメッセージを挿入したりできない。

定理(安全な認証チャネル)の証明

プロトコルNetAuth(π,f)に対する、UMモデルにおける、任意の攻撃者をUとする。
Uを用いて、AMモデルにおける、プロトコルSMTの攻撃者Aを構成する：

攻撃者A:

• πの初期化関数Iを実行。
• Uを呼び出す。:
  • ※ オネストパーティへの実行要求
  • Uが、ある内部パーティP_iに、実行要求(establish-session, P_i , P_j , s)を発したら、
    • 内部P_iと内部P_j間でπのサブセッションsをオネストにシミュレートする：
      • コラプトクエリやセッション開示クエリなど、πのサブセッションsの実行に関わるUのクエリは、
        • 内部パーティについてオネストに処理し、結果を返す。
      • πのサブセッションsで内部P_iや内部P_jが生成するメッセージはそのままUに渡し、
      • Uが配達するメッセージは対応する内部パーティにそのまま届ける。
      • ※ このとき、Uはメッセージを改ざん・挿入・欠落させる可能性がある。
    • Uがすべてのメッセージを配達し、内部P_iがπのサブセッションsのローカル出力として(established, P_j, s)を生成したら、
      • 外部P_iに (establish-session, P_i , P_j , s) を送る。
  • UがあるパーティP_iに実行要求(expire-session, P_i , P_j , s)を発したら、
    • 内部P_iのセッションsを失効させ、
    • 外部P_iに実行要求(expire-session, P_i , P_j , s)を送る。

• • Uが、ある内部パーティP_iに、実行要求(send, P_i, P_j, s, m)を発したら、
    • 内部P_iから内部P_jにNetAuth(π,f)に従ってmをU経由で送信する。
    • Uがメッセージを実際に配達したら、内部P_jが出力したメッセージ m' について、
      • 外部P_iに実行要求(send, P_i, P_j, s, m')を送る。
      • ※ このとき、Uはメッセージmを改ざんしてm'にしている可能性がある。
  • 外部P_iから外部P_j宛てのメッセージ(P_i,s,m)を受け取ったら、
    • メッセージ(P_i,s,m)をそのまま外部P_jに届ける。
  • ※ コラプトパーティとしての実行要求
  • Uが、以上の実行要求やメッセージ配達をコラプトされたパーティP_iの名前で実行するとき、
    • Aは内部パーティに対し対応する動作を忠実にシミュレートするとともに、
    • コラプトされた外部パーティP_iの名前で外部パーティに向けて対応する動作を行う。
  • ※ コラプトクエリ
  • UがパーティP_iにコラプトクエリを発したら、
    • Aは外部P_iにコラプトクエリを発し、P_iの（長期的な秘密情報を含む）状態を知る。
    • Aはそれとシミュレートされた内部P_iの状態をあわせて返す。
  • ※ セッション状態開示クエリ
  • UがパーティP_iにセッション状態開示クエリを発したら、
    • Aは外部P_iの該当セッションにセッション状態開示クエリを発し、
      • P_iの該当セッションの（長期的な秘密情報を含まない）セッション状態を知る。
    • Aはそれとシミュレートされた内部P_iのセッション状態をあわせて返す。
  • ※ セッション出力クエリ
  • UがパーティP_iにセッション出力クエリを発したら、
    • Aは外部P_iの該当セッションにセッション出力クエリを発し、
    • P_iの該当セッションのセッション出力を知り、Uに渡す。
• Uが停止したら、Uの出力を自身の出力としてAも停止する。

[攻撃者Aの解析]:

• AはAMモデルにおけるSMTに対する正当な攻撃者である。
• AによってUは完ぺきにシミュレートされている。
• ※ AはUのいいなり。
• 内部パーティと外部パーティのローカル出力の内容が異なり得るのは、内部パーティに関して以下のForgeyイベントが発生するケースのみ：
• ※ Uがメッセージmをm'に改ざんするとき、Aは最初から改ざん後の m' を送信していることに注意。
  • セッション(P_i, P_j, s)が局所暴露されていないにも関わらず、
  • ※ 局所暴露されていたら、ローカル出力への書き込みはないので、そもそも食い違いはあり得ない。
  • 内部P_jのローカル出力には『P_iからセッションsにおいてメッセージm'を受け取った』とあるのに、
  • 内部P_iのローカル出力には『P_jへセッションsにおいてメッセージm'を送った』との記録がない。
  • ※ メッセージm'は改ざんされたか挿入されたメッセージ。

以上より、Pr[Forgey]がネグリジブルならば、

• UNAUTH_{NetAuth(π,f),U} ≡^s AUTH_SMT,A.

主張
任意のUについて、ε = Pr[Forgey] はネグリジブルである。

証明
まず、Uを用いて、認証子生成関数 f の認証子の偽造者Fを構成する。

偽造者F:

• ※ オラクルf_κ(・)を用いて、あるメッセージm'の認証子t'を偽造したい。
• Uを起動する。
• セッション(P_i, P_j, s₀)をランダムに選択する。
• Uに対し、セッションs₀以外のセッションについてはAと全く同じように振る舞う。
  • Aにとっての外部パーティもF内でシミュレートする。
• セッション(P_i, P_j, s₀)について、
  • 以下を除いて、Aと全く同じように振る舞う。
  • (P_i, P_j)間でオネストに鍵共有プロトコルπをシミュレートする。
  • これによって生成されたセッション鍵をκ₀とおく。
  • ※ このκ₀とオラクルf_κ(・)がもっているκは別物。
  • Uが実行要求(send, P_i, P_j, s₀, m)を発したら、
    • mをオラクルf_κ(・)に発し、認証子 t を受け取る。
    • メッセージ (P_i , s₀, (m, t)) のP_jへの送信をシミュレートする。
  • UがP_jへのメッセージ(P_i , s₀, (m', t'))を発したら、
    • (m', t')をオラクルf_κ(・)に発し、okを受け取る。
    • ok = 1 で m'≠mならば(イベントForgey)、(m',t')を出力する。
  • 途中で、セッション(P_i, P_j, s₀)または(P_j, P_i, s₀)の局所暴露が要求されたら、アボートする。

[偽造者Fの解析]:

• κ=κ₀ならば、FのUに対するシミュレートは完ぺき。
• イベントForgeyがセッションs₀で起これば(確率は1/l)、Fは偽造結果(m', t')を出力できる。
• このとき、メッセージのフレッシュネスより、m' はそれ以前のどのmとも異なる。
• ※ ok = 1 の定義はメッセージのフレッシュネスを含んでいた。
• よって、Fはオラクルf_κ(・)には尋ねていないメッセージm'の認証子t'を生成している。

以上より、

• Pr[Fがfの認証子を偽造 | κ=κ₀] ≧ ε/l.

つぎに、偽造者Fを用いて、鍵共有プロトコルπに対する攻撃者Vを構成する：

攻撃者V:

• ※ UMモデルにおいて、鍵共有プロトコルπを攻撃したい。
• Fを起動する。
  • F内部のUに対し、
    • 鍵共有プロトコルπの実行については、Uの要求するとおりに、
      • Vが代理として、自身の外部パーティへ実行要求・メッセージ送信・その他のクエリを発し、その結果をUに返す。
      • ※ VもUMモデルにおける攻撃者なので、Uの命じるままに振る舞える。
    • πの実行以降のシミュレーションについて、
      • πの完了セッションからランダムにセッション(P_i, P_j, s₀)を選択し、
        • それをテストセッションと宣言して、その鍵候補κ*を得る。
      • セッションs₀について認証子を計算する必要がある場合には、κ*を鍵として用いて計算する。
      • その他のセッションsについて認証子を計算する必要がある場合には、
        • Vが自身の外部パーティの該当セッションsに対し、セッション出力開示クエリを発して、
        • ※ セッションsはテストセッションでないのでセッション出力開示クエリが許される
        • そのセッションの鍵κを入手し、κを用いて認証子を計算する。
  • Fが偽造に成功したらb'=1を、そうでないならb'=0を出力して停止する。

[攻撃者Vの解析]:

• s₀以外のセッションにおいて、
  • VによるFへのシミュレーションは完ぺき。
• セッションs₀において、
  • b = 0 のとき
    • πで共有された鍵と認証子生成に用いられた鍵κ*とは独立。
    • ∴　(V内のFのview) ≡ (Fのreal view).
  • b = 1 のとき
    • πで共有された鍵と認証子生成に用いられた鍵κ*とは同一。
    • ∴　(V内のFのview) ≡ (Fのreal view | κ = κ₀).

よって、

• Pr[Fがfの認証子を偽造] = Pr[ b' = 1 | b = 0]
• ≧ Pr[b' = 1 | b = 1] - (ネグリジブル)      ※ πはSK安全
• ≧ Pr[Fがfの認証子を偽造 | κ=κ₀] - (ネグリジブル)
• ≧ ε/l - (ネグリジブル) .

仮定より、認証子生成関数fは選択文書攻撃で安全なので、最左辺はネグリジブル。
よって、εもネグリジブル。
q.e.d.

Q.E.D.

上へ

---