アリスゲーム

•
•
•
•
•
•
•
•
•
•
講義プラン
入門（本日）
暗号入門
暗号化スキームとプロトコルの安全性
ハイブリッド論法
Abadi-Rogaway
ゲームとその形式化 --- 2回
記号論的アプローチ --- 2回
Mapping Lemma --- 2回
UC --- 2回
その他
講義プラン（改訂後）
•
•
•
•
•
•
•
•
•
入門
暗号入門
暗号化スキームとプロトコルの安全性
ハイブリッド論法
Abadi-Rogaway
Mapping Lemma
記号論的アプローチ（ストランド空間・PCL）
ゲームとその形式化（確率Hoare・Cryptoverif）
その他（UC・署名・ハッシュ・ゼロ知識証明・・・）
参考文献
• 萩谷昌己:
フォーマルメソッドによる暗号安全性,
情報処理, Vol.49, No.5, 2008, pp.537-543
• 萩谷昌己:
数理的技法による情報セキュリティの検証,
応用数理, Vol.17, No.4, 2007, pp.8-15
SSL2.0のハンドシェイク
（アリス・ボブ記法）
Mitchell たちによる定式化
サーバ
クライアント
C, SuiteC, NC
SuiteS, NS, signCA{S, KS+}
{Secret C}KS+
SuiteC と SuiteS とから
以後用いる暗号スイーツを決定
サーバ
クライアント
クライアントが指定した暗号スイーツ
クライアントが作ったノンス
nonce --- number once
C, SuiteC, NC
クライアント名
サーバが作ったノンス
サーバが指定した
暗号スイーツ
SuiteS, NS, signCA{S, KS+}
クライアントが作った秘密鍵を
サーバの公開鍵で暗号化
サーバの公開鍵の証明書
{Secret C}KS+
SuiteC と SuiteS とから
以後用いる暗号スイーツを決定
攻撃者
クライアント
サーバ
C, SuiteC, NC
C, SuiteI, NC
SuiteI, NS, signCA{S, KS+}
SuiteS, NS, signCA{S, KS+}
{SecretC}KS+
{SecretC}KS+
以後用いる暗号スイーツは
SuiteI に決定
Dolev-Yaoモデル
記号論的解析
SSL3.0では解消
Dolev-Yaoモデル
SSL3.0のハンドシェイク
クライアントが指定したSSLバージョン
SSL3.0のハンドシェイク
サーバが指定したSSLバージョン
クライアントの検証鍵の証明書
それまでにやりとりされた
メッセージ全体のハッシュ
Million message attack
クライアント
サーバ
{SecretC}KS+ の代わりの暗号文
PCKS#1のフォーマット
00 | 02 | padding string | 00 | 03 | 00 | premastersecret
に適合しているかどうか
論
• Dolev-Yaoモデル
• プロトコルの記述
– CSP
– π計算
• モデル検査
• 定理証明
記号論的アプローチ
• 完璧に安全な暗号を仮定。
– Dolev-Yaoモデル
• メッセージを項によって表現（メッセージ代数）
• フォーマルメソッド（数理的技法もしくは
形式的手法）の駆使
– モデル化
• 状態遷移系
• プロセス計算（汎用・専用）
• ストランド空間
– 自動検証
• モデル検査系
• 専用の検証系
記号論的アプローチの事例
• Needham-Schroeder の公開鍵暗号による
認証プロトコル（1978）の本質的部分
（アリス・ボブ記法）
A → B : {A, NA}KB
B → A : {NA, NB}KA
A → B : {NB}KB
アリス
乱数・ノンス
（作った人しか知り得ない）
{A, NA}KB
{アリス, アリスの秘密}ボブの公開鍵
このとき、アリスの秘密は、
アリスとボブしか知り得ない。
{NA, NB}KA
{アリスの秘密, ボブの秘密}アリスの公開鍵
アリスの秘密が帰って来たということは、
ボブが最初のメッセージを受信したはず。
{NB}KB
ボブ
{A, NA}KB
{アリス, アリスの秘密}ボブの公開鍵
{NA, NB}KA
{アリスの秘密, ボブの秘密}アリスの公開鍵
このとき、ボブの秘密は、
アリスとボブしか知り得ない？
{NB}KB
同様
Man-in-the-Middle攻撃
• Lowe が20年近くたってから発見（1995）
– プロトコルの厳格なモデル化が一つの理由
チャーリー
{A, NA}KC
{A, NA}KB
{NA, NB}KA
{NA, NB}KA
{NB}KC
{NB}KB
修正されたプロトコル
• Needham-Schroeder-Lowe
A → B : {A, NA}KB
B → A : {B, NA, NB}KA
A → B : {NB}KB
ストランド空間モデル
• ストランド空間モデル
–
–
–
–
Guttman, et al.（1998）
ストランド（個々の主体の実行トレース）
バンドル （因果関係について閉じたストランドの集合）
後ろ向き推論 によるバンドルの網羅
• 攻撃者のストランド
攻撃者によるあらゆる攻撃を想定。
アリス
攻撃者（チャーリー）
{NA, A}KC
ボブ
{NA, A}KB
{NA, NB}KA
{NB}KC
{NB}KB
ストランド空間モデルによる検証
• agreement の検証
ある主体のストランドを仮定して、
それを含むバンドルを網羅し、
対応する主体のストランドが必ずバンドルに
含まれることを示す。
• 認証性（authenticity）
• 相互認証性（mutual authenticity）
ボブ
{NA, A}KB
{B, NA, NB}KA
{NB}KB
アリス
{NA, A}KB
ボブ
{NA, A}KB
{B, NA, NB}KA
{B, NA, NB}KA
{NB}KB
{NB}KB
論
• 計算論的アプローチ
• 記号論的と計算論的の融合
– 直接的方法
– 間接的方法
計算論的アプローチ
• 暗号の脆弱性を考慮。
– IND-CPA
– IND-CCA
• 確率的多項式時間チューリング機械
– 攻撃者のモデル化
– 現実的な解析
• guessing attack
• 煩雑
– 機械化も容易でない。
– 多くの証明間違いの報告
計算論的な安全性
• ゲーム
• 汎用的結合可能性
IND-CCA2 ゲーム
攻撃者
元締め
pk
二つのメッセージ
m0 と m1 を生成
c 以外のメッセージ
c′ を送る
b の値を推測した
結果を b′ とする
公開鍵 pk と
秘密鍵 sk を生成
m0, m1 0 か 1 をランダムに
選んで b とする
mb を pkで暗号化した
c
結果を c とする
c′
m′
c′ を復号した結果
m′ を送る
b = b′ ?
IND-CCA2 ゲーム
攻撃者
元締め
pk
二つのメッセージ
m0 と m1 を生成
正確には、m0 と m1 を
生成する前にも、復号
を行うことができる。
c 以外のメッセージ
c′ を送る
b の値を推測した
結果を b′ とする
公開鍵 pk と
秘密鍵 sk を生成
m0, m1 0 か 1 をランダムに
選んで b とする
mb を pkで暗号化した
c
結果を c とする
c′
m′
c′ を復号した結果
m′ を送る
b = b′ ?
PKCS#1
IND-CPA ゲーム
攻撃者
元締め
pk
二つのメッセージ
m0 と m1 を生成
b の値を推測した
結果を b′ とする
公開鍵 pk と
秘密鍵 sk を生成
m0, m1 0 か 1 をランダムに
選んで b とする
mb を pkで暗号化した
ψ
結果を ψ とする
b = b′ ?
IND-CPA ゲーム
攻撃者
元締め
pk
r ⇐ R,
(m0, m1) ← A(r, pk)
b′ ← A(r, pk, ψ)
ランダム生成
(pk, sk) ⇐ KeyGen( )
m0, m1
ψ
b ⇐ {0, 1},
ψ ⇐ E(pk, mb)
b = b′ ?
IND-CPA ゲーム
•
•
•
•
•
例：公開鍵暗号
元締め： (pk, sk) ⇐ KeyGen( )
攻撃者： r ⇐ R, (m0, m1) ← A(r, pk)
元締め： b ⇐ {0, 1}, ψ ⇐ E(pk, mb)
攻撃者： b′ ← A(r, pk, ψ)
| Pr[b=b′] − 1/2 | : negligible?
ElGamal Encryption
• プロトコル
鍵生成： x ⇐ Zq, α ← γx, pk ← α, sk ← x
暗号化： y ⇐ Zq, β ← γy, δ ← αy, ζ ← δ·m, ψ ← (β, ζ)
復号： m ← ζ/βx
• IND-CPA ゲーム
x ⇐ Zq, α ← γx
r ⇐ R, (m0, m1) ← A(r, α)
b ⇐ {0, 1}, y ⇐ Zq, β ← γy, δ ← αy, ζ ← δ·mb
b′ ← A(r, α, β, ζ)
ゲーム変換
• DDH-advantage
| Pr[D(γx,
γy, γxy) | x, y ⇐ Zq] −
Pr[D(γx, γy, γz) | x, y, z ⇐ Zq] |
（D : 多項式時間述語）
• ElGamal Encryption ゲームの成功確率を
DDH-advantage に変換。
• Blanchet-Pointcheval（2006）
– プロセス計算の中でゲーム変換を形式化。
融合の試み
• 世界的な動向
• IEEE Computer Security Foundations Workshop
• Theory of Cryptography Conference
• ICALP Track C
• Formal and Computational Cryptography
• 間接的方法
– 記号論的推論に計算論的解釈を付与。
「記号論的に正しければ計算論的に正しい。」
– 必然的に暗号スキームを境界として上のレベル
• 直接的方法
– 計算論的解析をそのまま形式化。自動検証
– 主として下のレベル
間接的方法
• 受動的な識別可能性
• 能動的な攻撃
• 汎用的結合可能性に向かって
受動的な識別可能性
• Abadi-Rogaway（2000, 2002）
– 間接的方法のパイオニア
– 対称鍵
• Dolev-Yaoモデルに基づいて、
メッセージを表す項の間の等価性を定義。
(K1, ({m1}K1, {m2}K2}))
見えない部分は
等価
≈ (K1, ({m1}K1, {m3}K2}))
≈ (K1, ({m4}K1, {m3}K2}))
等価⇒識別不能
• m1 ≈ m2 ならば、
任意の確率的多項式時間述語 D に対して、
| Pr[D(x) | x∈[[m1]]η] − Pr[D(x) | x∈[[m2]]η] |
は security parameter η に関して negligible
• 根底にある暗号の type-0 安全性に帰着。
– ゲーム変換
能動的な攻撃
• Micciancio-Warinschi（2004）
• 例：Needham-Schroeder-Lowe
• 相互認証性（mutual authentication）
イニシエータにおいても
レスポンダにおいても agreement が成立。
• 記号論的に相互認証性が成り立つならば、
計算論的にも相互認証性が成り立つ。
– 相互認証性が成り立たない確率は negligible
– 能動的な攻撃も含まれる。
Mapping Lemma
• negligible な確率を除いて、
計算論的なトレース（実行過程）には、
記号論的なトレースが対応する。
– 記号論的なトレースに対応しないような
計算論的なトレースの確率は negligible
– 例えば guessing attack が成功する可能性は
negligible
• IND-CCA2 を仮定。
– 公開鍵暗号
直接的方法
• ゲーム変換の形式化
• ゲーム変換の自動化
•
•
•
•
•
•
•
•
•
•
講義プラン
入門（本日）
暗号入門
暗号化スキームとプロトコルの安全性
ハイブリッド論法
Abadi-Rogaway
ゲームとその形式化 --- 2回
記号論的アプローチ --- 2回
Mapping Lemma --- 2回
UC --- 2回
その他