Microsoft PowerPoint - sakurada3.pptx

Size: px

Start display at page:

Download "Microsoft PowerPoint - sakurada3.pptx"

あつのかくはり
5 years ago
Views:

1 チュートリアル :ProVerif による結合可能安全性の形式検証櫻田英樹日本電信電話株式会社 NTT コミュニケーション科学基礎研究所

2 アウトライン前半 :ProVerif の紹介後半 :ProVerifを用いた結合可能安全性証明 [Dahl Damgård, EuroCrypt2014, eprint2013/296] の記号検証パート 2

3 ProVerif フランス国立情報学自動制御研究所 (INRIA) の B. Blanchetを中心に開発されているプロトコル自動検証ツール π 計算と呼ばれる言語 ( 理論 ) に基づく様々な暗号技術を等式を用いて定義利用可能様々な種類の安全性を定義検証可能 ( 認証弱秘匿性非干渉性観測等価性 ) Unboundedな ( プロトコルの並列実行数などを制限しない ) 検証が可能 3

4 ProVerif におけるプロトコルの記述例 (1) 乱数生成メッセージ受信条件分岐メッセージの操作 ( 暗号化など ) メッセージ送信 4

5 ProVerif におけるプロトコルの記述例 (2) プロトコル全体鍵などの生成 ( 下のプロセスから参照できる ) 前のスライドのプロセスプロトコルで用いられる暗号等の性質 ( 必要な分だけ定義 ) 5

6 ProVerif による安全性 ( 観測等価性 ) 検証観測等価性 ( 攻撃者からは区別できない ) 任意のプロセスA(= 攻撃者 ) について A P が通信路 dからメッセージを出力 iff A Q が通信路 dからメッセージを出力攻撃者 A も単なるプロセスなのでメッセージの送受信と決められた演算しか用いない ( 記号モデルでの検証 ) ProVerif では P と Q がほぼ同じ形をしている場合のみ扱える ( 後述 ) 6

7 結合可能安全性の検証 (Dahl Damgård 2014) 実プロトコル ( 検証したいプロトコル ) が理想プロトコル ( 理想機能 + シミュレータ ) と同じように振る舞う ( 攻撃者から見て区別できない ) という等価性を示せば良い Theorem 5.6, 6.3 ( プロトコルによらず成立 ) 計算論的モデルでの等価性 ( 識別不能性 ) 自動検証が難しい記号モデルでの等価性 ( 観測等価性 ) 自動検証が容易個別のプロトコルについては ProVerif を使ってこれ検証すればよい 7

8 ProVerif を用いた検証の流れ ProVerif はほぼ同じ形の 2 つのプロセスの等価性しか検証できないため人手で以下を行う 1. 実プロトコルと理想プロトコルを記述 2. 両者がなるべく同じ形になるよう変形して 1 つのプロセス B にまとめる 3. B を ProVerif に入力して検証 ( ここは自動 ) corruption の各シナリオについて以上を行う 8

9 OT の実プロトコル記述 (Fig.97) sender 認証付き通信路による参加者間通信 receiver 環境 ( 攻撃者 ) との入出力 9

10 実プロトコルを変形 (Fig.99) 不要なチェックを削除複数のプロセスとして記述していたものをひとまとめに不要なチェックを削除正しく作った暗号文はチェック不要なので削除 10

11 OT の理想プロトコル (Fig.98) 理想機能シミュレータ (sender をシミュレート ) シミュレータ (receiver をシミュレート ) 11

12 理想プロトコルを変形 (Fig.100) 不要なチェックを削除削除実プロトコルと同様に複数のプロセス ( 理想機能シミュレータ ) をひとまとめに不要なチェックを削除 12

13 実プロトコルと理想プロトコルをまとめる両者の違いを choice で吸収 : choice[m0 M1] の形の箇所をすべて M0 で置き換えると実プロトコルすべて M1 で置き換えると理想プロトコルが得られるようにする (Fig.101) 13

14 ProVerif に入力して検証その前に暗号 ( コミットメント NIZK) の性質なども記述する必要がある ( 実はたくさんあります ) 停止しない場合は工夫が必要 ( 例では準同型暗号の暗号文の書き換え回数を制限 ) 安全でない場合は ( 内部モデルの ) 攻撃例を出力 $ proverif -in pi honest-tagged.pi Process: {1}new cks_483; : : ( ノート PC で 90 秒程度 ) 4800 rules inserted. The rule base contains 4708 rules. 661 rules in the queue rules inserted. The rule base contains 4908 rules. 565 rules in the queue rules inserted. The rule base contains 5108 rules. 417 rules in the queue rules inserted. The rule base contains 5308 rules. 217 rules in the queue rules inserted. The rule base contains 5508 rules. 17 rules in the queue. RESULT Observational equivalence is true (bad not derivable). 14

15 停止しない場合の工夫 ( タグ付け ) 準同型暗号の暗号文の書換規則 (eval_sel 関数 ) 書き換えられた暗号文は更に書換可能だが private reduc そのせいでProVerifが停止しなくなる ( 無限ループ ) eval_sel(enc(zero, x_rb, ek(x_dk)), zero, zero, xr) = enc(zero, xr, ek(x_dk)); eval_sel(enc(zero, x_rb, ek(x_dk)), zero, one, xr) = enc(zero, xr, ek(x_dk)); eval_sel(enc(zero, x_rb, ek(x_dk)), zero, two, xr) = enc(zero, xr, ek(x_dk)); eval_sel(enc(zero, x_rb, ek(x_dk)), one, zero, xr) = enc(one, xr, ek(x_dk)); eval_sel(enc(zero, x_rb, ek(x_dk)), one, one, xr) = enc(one, xr, ek(x_dk)); : 書き換えられた暗号文に違う記号を割り当てて再度の書換を禁止 ProVerifが停止するように private reduc eval_sel(enc(zero, x_rb, ek(x_dk)), zero, zero, xr) = encn(zero, xr, ek(x_dk)); eval_sel(enc(zero, x_rb, ek(x_dk)), zero, one, xr) = encn(zero, xr, ek(x_dk)); eval_sel(enc(zero, x_rb, ek(x_dk)), zero, two, xr) = encn(zero, xr, ek(x_dk)); eval_sel(enc(zero, x_rb, ek(x_dk)), one, zero, xr) = encn(one, xr, ek(x_dk)); eval_sel(enc(zero, x_rb, ek(x_dk)), one, one, xr) = encn(one, xr, ek(x_dk)); : 15

16 まとめ ProVerif の紹介等式により暗号の性質を記述可能観測等価性で表される安全性を検証可能結合可能安全性の証明に使える ProVeirf を用いた結合可能安全性証明 1. 計算論的モデルでの安全性を記号モデルでの安全性に帰着 ( いわゆる計算論的健全性 ) 2. 記号モデルでの安全性をProVerif 自動検証 ( とは言うものの結構手作業があります ) 16

An Automated Proof of Equivalence on Quantum Cryptographic Protocols

An Automated Proof of Equivalence on Quantum Cryptographic Protocols 量子暗号のためのプロトコル等価性検証ツール久保田貴大 *, 角谷良彦 *, 加藤豪, 河野泰人, 櫻田英樹 * 東京大学情報理工学系研究科, NTT コミュニケーション科学基礎研究所背景暗号安全性証明の検証は難しい量子暗号でもそうである検証のための形式体系が提案されているが, 実際には, 形式体系の適用は手作業では非常に煩雑である形式検証のためには, 検証ツールが開発されることが望ましい