攻撃者の視点からの完全秘匿性 (1) 完全識別不可能性

今まで議論してきたシャノンの完全秘匿性や識別不可性に基づく完全秘匿性では、「確率が変わらないのだから新たな情報は得られていない」とか「確率分布が変わらないのだから新たな情報は得られていない」ということを数式で定式化して同値性を証明してきました。

しかしこれは暗号のセキュリティの話です。そこではやはり攻撃に対する情報漏洩リスクを明示的に扱いたいですよね。「攻撃者は暗号文を入手してもそこから情報を得られない」のであれば、その暗号を使った場合の情報漏洩リスクはないことがわかります。

参考にしている本

暗号理論入門

作者:安永憲司
森北出版

Amazon

では完全秘匿性と同等な定義として攻撃者を含んだ定義を２つ与えています。今回はそのうちの１つである完全識別不可能性について紹介します。

p18, 定義2.2より　完全識別不可能性

共通鍵暗号方式(Enc, Dec)が完全に識別不可能であるとは、任意の平文$m_0, m_1$及び攻撃者Aに対し、

$$Pr[A(Enc_K (m_0 ) )=1]=Pr[A(Enc_K (m_1 ) )=1]$$

を満たすことである。

ここでAがなければほぼほぼ以前紹介した識別不可能性の定義と同じですね。では攻撃者Aは何者でしょうか。Aは暗号文をみて、元の平文が$m_0$なのか$m_1$なのかを当てようとしています。Aは引数に$Enc_K (m_0 )$などを取っていることから暗号文を入力としていることがわかります。出力として1であればAは元の平文を$m_1$と推測したとします。またAの出力が1以外であればAは元の平文を$m_0$と推測したとします。

そして完全識別不可能性の定義では、任意の攻撃者Aについて1を出力する確率はどんなメッセージの暗号文でも変わらない、ということを主張しています。

もし仮に暗号文が$Enc_K (m_0 )$である時にAが1を出力する確率と暗号文が$Enc_K(m_1)$である時にAが1を出力する確率が異なるようなAが存在するということは暗号文から平文のなんらかの情報が取れることになります。そんな計算ができる攻撃者Aは存在しない、というのがこの定義となります。

Lean4でこの定義を形式化してみましょう。

def perfect_indistinguishability (Enc : K → M → C) (Gen : PMF K) : Prop :=
∀ (m0 m1 : M) (A : C → PMF Bool),
(do let c ← (Enc_dist Enc Gen m0); A c) 1= (do let c ← (Enc_dist Enc Gen m1); A c) 1

攻撃者AをA : C → PMF Boolとして形式化しました。Aは確率的アルゴリズムなので出力はBoolではなく確率分布を表すPMF Boolになります。平文(m0, m1など)から生成した暗号文cをAに見せる部分がA cの部分です。cの生成もAの出力であるA cも確率的であることに注意してください。

ここまで形式化できればこの定義と攻撃者抜きの識別可能性に基づく完全秘匿性の定義が同値である、ということを次のように表すことができます。

/- 識別不可能性に基づく完全秘匿性 -/

def ind_perfect_secrecy (Enc : K → M → C) (Gen : PMF K) :=
∀ (m1 m2 : M) (c : C),
(Enc_dist Enc Gen m1) c = (Enc_dist Enc Gen m2) c

/- 完全識別不可能性 -/

def perfect_indistinguishability (Enc : K → M → C) (Gen : PMF K) : Prop :=
∀ (m0 m1 : M) (A : C → PMF Bool),
(do let c ← (Enc_dist Enc Gen m0); A c) 1 = (do let c ← (Enc_dist Enc Gen m1); A c) 1

/- 完全識別不可能性と識別不可能性に基づく完全秘匿性は同値である -/

theorem ind_perfect_secrecy_iff_perfect_indistinguishability
[DecidableEq C] (Enc : K → M → C) (Gen : PMF K) :
ind_perfect_secrecy Enc Gen ↔ perfect_indistinguishability Enc Gen