Comments
Description
Transcript
アリスゲーム
• • • • • • • • • • 講義プラン 入門(本日) 暗号入門 暗号化スキームとプロトコルの安全性 ハイブリッド論法 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回 その他