量 子 鍵 配 送 プロトコルの 無 条 件 安 全 性 証 明 の 自 動 化 に 向 けて 久 保 田 貴 大 1, 角 谷 良 彦 1, 加 藤 豪 2, 河 野 泰 人 2 1 東 京 大 学 大 学 院 情 報 理 工 学 系 研 究 科 2 NTTコミュニケーション 科 学 基 礎 研 究 所
量 子 鍵 配 送 プロトコル(QKD) 量 子 通 信 を 用 いた 秘 密 鍵 共 有 プロトコル 無 条 件 安 全 性 が 得 られる 攻 撃 者 は 量 子 チャネルに 任 意 の 攻 撃 が 可 能 攻 撃 者 に 漏 れる 情 報 量 が 無 視 できるほど 小 さい 攻 撃 者 の 計 算 能 力 によらない BB84, B92, DPS-QKD, COW-QKD 安 全 性 証 明 が 複 雑 [Mayers97] 形 式 手 法 の 有 効 性 を 調 べたい
研 究 の 概 要 BB84プロトコルの Shor-Preskillの 証 明 法 [Shor-Preskill00] を 形 式 化 した 変 形 ステップ BB84プロトコルを Modified Lo-Chauプロトコルに 変 形 するステップ 変 形 を 自 動 的 に 行 う 枠 組 みを 作 った 解 析 ステップ Modified Lo-Chauプロトコルが 安 全 であることを 証 明 するステップ 量 子 ホーア 論 理 [Kakutani09]で 証 明 を 形 式 化 した
発 表 の 流 れ BB84プロトコルについて 変 形 ステップの 自 動 化 について 解 析 ステップの 形 式 化 について まとめと 今 後 の 課 題
攻 撃 者 の 能 力 に 関 する 仮 定 ( ) Alice, the initiator Public classical channel Public quantum channel ( _ ) Eve, the attacker ( Д #) Bob, the responder 古 典 チャネルは 盗 聴 可 能 改 ざん 不 可 量 子 チャネルには 任 意 の 攻 撃 が 可 能 無 限 の 計 算 能 力 を 持 つ
安 全 性 無 条 件 安 全 性 任 意 の 攻 撃 者 (イブ)に 対 して プロトコルが 中 断 する 確 率 が 無 視 できるほど 小 さいならば アリスの 鍵 とイブの 推 測 の 相 互 情 報 量 が 無 視 できる ほど 小 さい
Preliminaries 量 子 の 純 粋 状 態 純 粋 状 態 ψ> は C 2 の 単 位 ベクトルである Z 基 底 X 基 底
観 測 (1) 0>, 1> が Z 基 底 で 観 測 された 場 合 結 果 は 確 率 1でそれぞれ 0>, 1> である 0>, 1> が X 基 底 で 観 測 された 場 合 結 果 は 確 率 1/2で +> か -> のどちらかである
観 測 (2) +>, -> が X 基 底 で 観 測 された 場 合 結 果 は 確 率 1でそれぞれ +>, -> である +>, -> が Z 基 底 で 観 測 された 場 合 結 果 は 確 率 1/2で 0> か 1> のどちらかである
BB84 で 用 いられる 状 態 と 観 測 4 種 類 の 状 態 を 用 いる: 0>, 1>, +>, -> 2 種 類 の 観 測 基 底 を 用 いる: Z, X 0>, 1> はZ 基 底 で 識 別 可 能 +>, -> はX 基 底 で 識 別 可 能 アリスはボブに 送 る 状 態 を 基 底 ビットとランダムビットに 従 って 生 成 する 基 底 0 0 1 1 ランダム 0 1 0 1 状 態 0> 1> +> ->
BB84 Protocol Alice Bob
BB84 Protocol Alice Bob (4+δ)n ビットの 乱 数 列 をふたつ 生 成 する ba := 00110011 ( 基 底 用 ) ZZXXZZXX da := 01010011
BB84 Protocol Alice Bob (4+δ)n ビットの 乱 数 列 をふたつ 生 成 する ba := 00110011 ( 基 底 用 ) ZZXXZZXX da := 01010011 qb := 0>, 1>, +>, ->, 0>, 0>, ->, ->
BB84 Protocol Alice (4+δ)n ビットの 乱 数 列 をふたつ 生 成 する ba := 00110011 ( 基 底 用 ) ZZXXZZXX da := 01010011 qb := 0>, 1>, +>, ->, 0>, 0>, ->, -> Bob (4+δ)n ビットの 乱 数 列 を 生 成 する bb := 01110100 ( 観 測 基 底 用 ) ZXXXZXZZ
BB84 Protocol Alice (4+δ)n ビットの 乱 数 列 をふたつ 生 成 する ba := 00110011 ( 基 底 用 ) ZZXXZZXX da := 01010011 qb := 0>, 1>, +>, ->, 0>, 0>, ->, -> Bob (4+δ)n ビットの 乱 数 列 を 生 成 する bb := 01110100 ( 観 測 基 底 用 ) ZXXXZXZZ
BB84 Protocol Alice (4+δ)n ビットの 乱 数 列 をふたつ 生 成 する ba := 00110011 ( 基 底 用 ) ZZXXZZXX da := 01010011 qb := 0>, 1>, +>, ->, 0>, 0>, ->, -> qb Bob (4+δ)n ビットの 乱 数 列 を 生 成 する bb := 01110100 ( 観 測 基 底 用 ) ZXXXZXZZ db := 0?010???
BB84 Protocol Alice (4+δ)n ビットの 乱 数 列 をふたつ 生 成 する ba := 00110011 ( 基 底 用 ) ZZXXZZXX da := 01010011 qb := 0>, 1>, +>, ->, 0>, 0>, ->, -> ba i bb i なる da i を 捨 てる da := 0 010 qb ba bb Bob (4+δ)n ビットの 乱 数 列 を 生 成 する bb := 01110100 ( 観 測 基 底 用 ) ZXXXZXZZ db := 0?010??? ba i bb i なる db i を 捨 てる db := 0 010
BB84 Protocol Alice (4+δ)n ビットの 乱 数 列 をふたつ 生 成 する ba := 00110011 ( 基 底 用 ) ZZXXZZXX da := 01010011 qb := 0>, 1>, +>, ->, 0>, 0>, ->, -> ba i bb i なる da i を 捨 てる da := 0 010 qb ba bb Bob (4+δ)n ビットの 乱 数 列 を 生 成 する bb := 01110100 ( 観 測 基 底 用 ) ZXXXZXZZ db := 0?010??? ba i bb i なる db i を 捨 てる db := 0 010 δ が 十 分 大 きければ 高 い 確 率 で2nビット 以 上 が 残 る (そうでなければ プロトコルを 中 断 する)
BB84 Protocol Alice da := 001010110 (2n) Bob db := 001010110 (2n)
BB84 Protocol Alice da := 001010110 (2n) daからランダムに 半 分 選 び チェック 用 ビット 列 にする Bob db := 001010110 (2n)
BB84 Protocol Alice Bob da := 001010110 (2n) daからランダムに 半 分 選 び チェック 用 ビット 列 にする チェック 用 ビット 列 db := 001010110 (2n) ビットが 何 個 反 転 しているか 数 え エラーレートを 計 算 する
BB84 Protocol Alice Bob da := 001010110 (2n) daからランダムに 半 分 選 び チェック 用 ビット 列 にする エラーレートが 閾 値 より 大 きければプロトコルを 中 断 チェック 用 ビット 列 エラーレート db := 001010110 (2n) ビットが 何 個 反 転 しているか 数 え エラーレートを 計 算 する
BB84 Protocol Alice Bob da := 001010110 (2n) daからランダムに 半 分 選 び チェック 用 ビット 列 にする エラーレートが 閾 値 より 大 きければプロトコルを 中 断 チェック 用 ビット 列 エラーレート db := 001010110 (2n) ビットが 何 個 反 転 しているか 数 え エラーレートを 計 算 する n ビットが 残 る エラー 訂 正 プライバシー 増 幅
変 形 ステップ [Shor-Preskill00] BB84プロトコルをModified Lo-Chauプロトコル に 変 形 するステップ Modified Lo-Chauプロトコルは 直 接 解 析 しやすい 変 形 ステップを 自 動 化 する 枠 組 みを 作 った BB84をプログラミング 言 語 で 形 式 化 し 変 形 のための 書 き 換 え 規 則 を 作 り 自 動 化 に 有 用 な 性 質 を 考 察 した [SP00]の 方 法 今 回 の 方 法 BB84 CSS 書 き 換 え 書 き 換 え BB84 書 き 換 え Modified Lo-Chau Modified Lo-Chau
構 文 論 自 動 化 の 枠 組 み BB84を 形 式 化 するのに 十 分 な 表 現 力 の プログラミング 言 語 [Selinger04] 攻 撃 者 の 存 在 のもとでのBB84の 実 行 を プログラムとして 形 式 化 した
意 味 論 プログラム 変 数 の 量 子 状 態 は 密 度 行 列 で 表 現 される プログラムは 実 行 前 の 密 度 行 列 を 実 行 後 の 密 度 行 列 に 写 すオペレータとして 解 釈 される[Selinger04]
書 き 換 え 規 則 健 全 性 書 き 換 え 後 のプログラムが 安 全 ならば 書 き 換 え 前 のプログラムが 安 全 である 書 き 換 え 規 則 の 例 意 味 が 同 じ 攻 撃 者 のプロジージャの 扱 い プロシージャの 性 質 # 上 側 が ke[], qe[], qb[] 以 外 の 変 数 を 含 まない
書 き 換 え 系 の 性 質 適 当 な 制 約 のもとで 以 下 が 成 立 することを 示 した 強 正 規 化 性 (SN) 任 意 のプログラムの 書 き 換 えが 停 止 する 合 流 性 (CR) 正 規 形 があれば 書 き 換 えの 戦 略 によらず 一 意 BB84は 必 ず Modified Lo-Chau プロトコルに 書 き 換 えられて 書 き 換 えが 停 止 する
解 析 ステップ Modified Lo-Chauプロトコルが 安 全 であること を 示 すステップ 証 明 を 量 子 ホーア 論 理 を 用 いて 形 式 化 した 書 き 換 え 書 き 換 え BB84 書 き 換 え 安 全 であることを 示 す Modified Lo-Chau
解 析 ステップ Modified Lo-Chauプロトコルが 安 全 であること を 示 すステップ 証 明 を 量 子 ホーア 論 理 を 用 いて 形 式 化 した 書 き 換 え 書 き 換 え BB84 書 き 換 え 安 全 であることを 示 す Modified Lo-Chau BB84 Modified Lo-Chauの 安 全 性 が BB84の 安 全 性 を 含 意 ( 書 き 換 え 規 則 の 健 全 性 ) 安 全 である Modified Lo-Chau
量 子 ホーア 論 理 量 子 プログラムの 性 質 を ホーアトリプルで 表 明 する 枠 組 み[Kakutani09] {Φ} P {Ψ} Φが 成 り 立 つときにPを 実 行 するとΨが 成 り 立 つ プログラムの 構 文 と 意 味 は 変 形 ステップで 用 いたものと 同 じ
証 明 したいこと
証 明 したいこと Modified Lo-Chau プロトコル プロトコルの 実 行 後 に 成 り 立 つべき 性 質
まとめ Shor-PreskillのBB84 安 全 性 証 明 を 形 式 化 した 変 形 ステップ BB84をプログラムとして 形 式 化 し 意 味 論 に 対 して 健 全 な 書 き 換 え 規 則 を 作 り 書 き 換 え 系 の 性 質 解 析 ステップ 量 子 ホーア 論 理 で 形 式 化 した
今 後 の 課 題 より 多 くの 量 子 鍵 配 送 プロトコル(QKD) が 扱 えるよう 枠 組 みを 拡 張 する 現 在 BB84とB92の 変 形 が 可 能 六 状 態 プロトコル[GB98] SARGプロトコル[SARG04] など 多 数 のQKDが 扱 えることを 示 す 別 の 検 証 要 件 並 列 実 行 が 形 式 化 しやすい 枠 組 みを 検 討 する マルチセッションを 想 定 した 安 全 性 マルチパーティ プロトコル