An Automated Proof of Equivalence on Quantum Cryptographic Protocols

Size: px

Start display at page:

Download "An Automated Proof of Equivalence on Quantum Cryptographic Protocols"

れいなもてぎ
5 years ago
Views:

1 量子暗号のためのプロトコル等価性検証ツール久保田貴大 *, 角谷良彦 *, 加藤豪, 河野泰人, 櫻田英樹 * 東京大学情報理工学系研究科, NTT コミュニケーション科学基礎研究所

2 背景暗号安全性証明の検証は難しい量子暗号でもそうである検証のための形式体系が提案されているが, 実際には, 形式体系の適用は手作業では非常に煩雑である形式検証のためには, 検証ツールが開発されることが望ましい

3 研究の概要量子プロセス計算 qccs [FDY11] における双模倣関係を自動検証するツールを開発した Shor と Preskill による BB84 の安全性証明 [SP00] にツールを適用した

4 本発表の構成量子プロセス計算 qccs Shor-PreskillによるBB84の安全性証明検証ツール実験結果まとめと今後の課題

5 量子ビットと密度行列量子ビットの状態は, C 2 ( 二次元ヒルベルト空間 ) の単位ベクトルとして表される 0, 1 は標準基底, 縦ベクトル α 0 + β 1 ( α 2 + β 2 = 1) 量子ビット列の状態は, 量子ビットの状態のテンソル積として表される量子ビット列の状態が, 確率 p i で ψ i であるという確率分布は, 密度行列 ψ i ψ i で表される ( ) i p i

6 qccs の文法 [FDY11] 量子通信量子演算観測ひとつの qubit 型自由変数には, 2 次元ヒルベルト空間が対応する各 qubit の状態をあらわす密度行列を ρ とする以後, 組 P, ρ のことをコンフィグレーションとよぶ P Q は, qv(p) qv(q) = のときのみ定義される量子通信で空間をやりとりできる

7 ラベル付き状態遷移 a コンフィグレーション P, ρ は行動 α をおこなって, 確率分布 μ に遷移する

8 状態遷移の例 1 τ τ

9 状態遷移の例 1 τ τ 観測したときだけ確率分岐

10 状態遷移の例 1 τ 外に見える遷移 τ 外から見えない遷移

11 双模倣関係ふたつのコンフィグレーション P, ρ, Q, σ が外から見て同じように振る舞うという関係一方のプロセスが遷移可能なら, 他方でも τ 遷移を除いて同様の遷移が可能であり, かつ, 各ステップにおいて, 外の人がアクセスできる量子状態が同じ P, ρ Q, σ と書く

12 BB84 の安全性証明の概要 [SP00] BB84 ( ) Alice, the initiator Public classical channel Public quantum channel ( Д #) Bob, the responder

13 BB84 の安全性証明の概要 [SP00] BB84 ( ) Alice, the initiator Public classical channel Public quantum channel ( Д #) Bob, the responder 外から見て区別できないことを示す EDP ( ) Alice, the initiator Public classical channel Public quantum channel Secret classical channel ( Д #) Bob, the responder

14 BB84 の安全性証明の概要 [SP00] BB84 ( ) Alice, the initiator Public classical channel Public quantum channel ( Д #) Bob, the responder 安全であることを示す EDP ( ) Alice, the initiator Public classical channel Public quantum channel Secret classical channel 外から見て区別できないことを示す ( Д #) Bob, the responder

15 形式検証の概要 BB84 ( ) Alice, the initiator Public classical channel Public quantum channel ( Д #) Bob, the responder 外から見て区別できないことを示す EDP ( ) Alice, the initiator Public classical channel Public quantum channel Secret classical channel ( Д #) Bob, the responder

16 形式検証の概要 BB84 コンフィグレーション qccs ( プロセスとして ) として形式化形式化した Alice, the initiator Public quantum channel Public classical channel 双模倣の証明 ( Д #) Bob, the responder EDP ( ) Alice, the initiator Public classical channel Public quantum channel Secret classical channel ( Д #) Bob, the responder

17 これまでの研究 [KKKKS 12] 双模倣を手作業で示した状態遷移が長く, 分岐が多い攻撃者がアクセスできる量子状態が等しいことは, 元論文の証明と同じように示した検証ツールがあるとよい遷移が対応することを自動的に検証したい量子状態の等しさも自動で計算したい

18 ツールの設計 ( 量子状態の表現 ) 量子状態は記号列で表現鍵の長さなどを決めるセキュリティパラメタは, 自然数の定数記号として扱う n 個の EPR ペア

19 観測の形式化について構文にある観測書いた場合で + + qa τ τ qa 1 1 qa 観測をあらわす量子演算で書いた場合 1 τ qa ( ) qa 量子演算観測

20 観測の形式化について [KKKKS 12] 観測の形式化は二種類あり, 使い分ける必要がある攻撃者にとって分岐が見えるような観測だったら M[q ; x] で形式化する観測の結果によって違うラベルで遷移する場合など見えないならで形式化する量子演算観測

21 ツールの設計 ( 確率分岐 ) 形式化の使い分けを自然に行うため, M[q ; x] は if 分岐に組み込んだ τ τ

22 ツールの設計 ( 確率分岐 ) 形式化の使い分けを自然に行うため, M[q ; x] は if 分岐に組み込んだ if q if q c!r

23 ツールの設計 ( 確率分岐 ) 形式化の使い分けを自然に行うため, M[q ; x] は if 分岐に組み込んだ if q if q c!r

24 ツールの設計 ( 確率分岐 ) 形式化の使い分けを自然に行うため, M[q ; x] は if 分岐に組み込んだ if q if q c!r

25 ツールの設計 ( 確率分岐 ) 形式化の使い分けを自然に行うため, M[q ; x] は if 分岐に組み込んだ if q if q c!r

26 双模倣の検証状態遷移の対応を調べる外の人 ( 攻撃者 ) がアクセス可能な量子状態が常に一致しているか確認する

27 量子状態の等しさの判定コンフィグレーション P, ρ に対し, 外の人 ( 攻撃者 ) がアクセス可能な量子状態は, 部分トレース Tr[qv(P)](ρ) で表されるツールは, 変数の出現に着目して, 消去できる記号を消去する ( トレースアウト ) Tr[qv(P)](ρ) 全体の量子状態 ρ のうち, P に現れる量子変数に対応する空間を, 攻撃者に見えなくする

28 トレースアウト例 Tr[q, r](op1[q](x[q]*y[r]*z[s])) Tr[q, r](op2[q](u[q]*z[s]*v[r]))

29 トレースアウト例 Tr[q, r](op1[q](x[q]*y[r]*z[s])) Tr[q, r](op2[q](u[q]*z[s]*v[r])) Z[s] Z[s]

30 ユーザ定義等式の適用左辺にマッチする部分を, 右辺に書き換えるユーザ定義 : Tr[q](EPR[q, r]) = Tr[q](PROB[q,r]) 対象の環境 : Tr[q](op[s, t](epr[q, r]*x[s]*y[t])) Tr[q](op[s, t](prob[q, r]*x[s]*y[t])) 判定する機会ごとに, 各等式は高々一度ずつしか適用しない等式適用の手続は必ず停止する

31 量子状態の等しさの判定トレースアウトと等式適用の両方によって, 書き換える書き換えたあとの環境どうしが構文的に等しいか判定する量子演算の記号, 状態の記号を適切に交換して, 等しい記号列にできるかを調べる ( 例 ) E[q](F[r, s](u[q]*v[r]*w[s])) = F[r, s](e[q](v[r]*u[q]*w[s]))

32 ツールの概要 Ruby で動作確認入力 : 双模倣を検証したい二つのコンフィグレーション P, ρ, Q, σ と, ユーザ定義等式の集合出力 : true または false

33 ツールの性質どんな入力に対しても停止するツールが true を出力したとき, 等式が正しければ, P, ρ, Q, σ は双模倣であるツールが false を出力しても, P, ρ, Q, σ は双模倣かもしれない双模倣であることを示すための等式が不足している可能性がある

34 等式のためのオプション量子状態, 部分トレース, プロセスを表示する部分トレースが等しくならないときなど不足している等式を見つけることや, 等式の誤りを見つけるのに役立つ

35 実験環境 Panasonic CF-J9 Intel(R) Core(TM) i5 CPU 2.53GHz, 1GB memory

36 実験結果 Shor-Preskill の, BB84 と EDP の等価性検証状態遷移木 BB84: 588ノード, 165パス EDP: 621ノード, 165パス双模倣の検証までに, 秒かかった再帰手続きは, 951 回呼び出された

37 まとめ量子プロセス計算 qccs の双模倣関係を検証するツールを開発した量子状態は記号で表される量子状態間の等式は人間が与えるツールは等式を使って部分トレースを計算し, 状態遷移の対応をチェックする Shor-Preskill による BB84 の安全性証明に検証ツールを適用した BB84 と EDP の等価性の自動検証を行った

38 今後の課題項書き換え戦略のより詳しい検討確率双模倣 EDP の安全性証明の形式化自動化他のプロトコルへの応用 B92, 六状態プロトコルなどは, Shor-Preskill と似た方法による安全性証明がある

Microsoft PowerPoint - sakurada3.pptx

Microsoft PowerPoint - sakurada3.pptx チュートリアル :ProVerif による結合可能安全性の形式検証櫻田英樹日本電信電話株式会社 NTT コミュニケーション科学基礎研究所アウトライン前半 :ProVerif の紹介後半 :ProVerifを用いた結合可能安全性証明 [Dahl Damgård, EuroCrypt2014, eprint2013/296] の記号検証パート 2 ProVerif フランス国立情報学自動制御研究所