ワンタイムパッド暗号で鍵の再利用は危険だよ。 Lean4で形式証明してみた

以前ワンタイムパッド暗号を紹介し、その完全秘匿性をLean4で形式証明しました。暗号の定義の中で「使った鍵は再利用してはいけない」、ということを書きました。ただしその条件は証明の中で明示的に使われているようには見えないし、数学的な条件なのか一般的な注意事項（鍵を使い回すのはよくないよ、的な）なのかよくわかっていませんでした。

購入して読んでいる本

の目次を見ていたら、「第5章　複数回の暗号化」という章に気がつきました。ひょっとしてここに関連事項が書いてあるのか、と思って読んでみると、、、なんと「同じ鍵で２つの平文を暗号化する」をした場合計算量的安全が失われることの証明が載っています。「計算量的安全性」はこのブログではまだ定義していないし、、、とも思ったのですが、よく読むと鍵の再利用で完全秘匿性が失われる証明にもなることに気がつきました。

まず非常に大雑把な議論としては以下のようなものがあります。２つの平文を$m_1, m_2$, 鍵を$k$, ２つの平文を$k$で暗号化した暗号文を$c_1, c_2$とします。ワンタイムパッド暗号の定義から$c_1 = k\, \oplus m_1, \, c_2 = k\, \oplus m_2$です。攻撃者が２つの暗号文$c_1, c_2$を見て$c_1 \oplus c_2$を計算します。すると、

$$ c_1 \oplus c_2 = (k\, \oplus m_1) \oplus (k\, \oplus m_2) = m_1 \oplus m_2$$

となります。この値は$m_1, m_2$の排他的論理和であり$k$は関係ありません。これは２つの平文そのものではないにしてもそれらに関する情報が漏洩したことになります。これは完全秘匿性に反します。

雰囲気としてはいいんですが、これでは数式で定義した完全秘匿性にどう反しているのかわかりませんよね。ただ、$ c_1 \oplus c_2 =m_1 \oplus m_2$という式からは、同じ鍵を使い回すと生成される２つの暗号文の間に強い制約がかかってしまい、暗号文の分布が影響を受けそうなことが読み取れます。これを利用すれば証明ができそうです。

実際の証明は次のようになります。まず証明したい命題を言葉で書くとこんな感じです。

「ワンタイムパッド暗号で同じ鍵を２つの平文の暗号化に使う場合、任意の２つの平文を１つの鍵で暗号化すると、暗号文の確率が元の平文によって異なることがある」

ようは完全秘匿性が成り立たない例がある、ということです。反例を作ってそれが完全秘匿性を満たさないことを示します。

Lean4でまず定理の形式化の部分をお見せして説明します。

variable {n : ℕ}
local notation "N2" => (2 : ℕ)

-- Enc2_dist_n2 is defined to be the distribution of ciphertext pairs
-- when the same key is used to encrypt two messages m1 and m2.
noncomputable
def Enc2_dist_n2 (m1 m2 : BitVec 2) : PMF (BitVec 2 × BitVec 2) := do
let k ← (OTP_Gen : PMF (BitVec 2))
PMF.pure (OTP_Enc k m1, OTP_Enc k m2)

-- Fix two pairs of messages (m10,m20) and (m11,m21).
def m10 : BitVec 2 := 0 -- 00
def m20 : BitVec 2 := 0 -- 00
def m11 : BitVec 2 := 0 -- 00
def m21 : BitVec 2 := 3 -- 11

theorem reuse_breaks_perfect_secrecy_n2 :
∃ c : BitVec 2 × BitVec 2,
Enc2_dist_n2 m10 m20 c ≠ Enc2_dist_n2 m11 m21 c := by

まず平文、鍵、暗号文の長さは２ビット(BitVec 2)に固定します。また２つの平文m1, m2を同じ鍵kで暗号化して２つの暗号文OTP_Enc k m1, OTP_Enc k m2を得る確率試行をEnc2_dist_n2(m1, m2)で定義します。

反例は１つあれば十分なので、m10=00, m20=00, m11=00, m21=11を固定した４つの平文とします。m10とm20を同じ鍵で暗号化し、m11とm20を同じ鍵で暗号化します。この時ある暗号文cが存在してm10, m20の暗号化確率試行とm11, m21の暗号化確率試行でcとなる確率が異なる、というのが定理reuse_breaks_perfect_secrecy_n2の主張となります。

以下に証明を貼り付けて流れだけ説明します。証明の流れとしてはこの暗号文c（２つの平文を同じ鍵で暗号化したもの）を具体的に構成します。そしてuse cでそれをゴールに代入します。

つぎにEnc2_dist_n2 m10 m20 c ≠ Enc2_dist_n2 m11 m21 cの左辺が1/4であることを証明しp1とします。さらに右辺が0であることを証明しp2とします。これらをゴールに代入すると1/4≠0となり、norm_numでこの式が正しいことを確かめて証明が終了します。

variable {n : ℕ}
local notation "N2" => (2 : ℕ)

-- Enc2_dist defined to be the distribution of ciphertext pairs
-- when the same key is used to encrypt two messages m1 and m2.
noncomputable
def Enc2_dist_n2 (m1 m2 : BitVec 2) : PMF (BitVec 2 × BitVec 2) := do
let k ← (OTP_Gen : PMF (BitVec 2))
PMF.pure (OTP_Enc k m1, OTP_Enc k m2)

-- Fix two pairs of messages (m10,m20) and (m11,m21).
def m10 : BitVec 2 := 0 -- 00
def m20 : BitVec 2 := 0 -- 00
def m11 : BitVec 2 := 0 -- 00
def m21 : BitVec 2 := 3 -- 11

theorem reuse_breaks_perfect_secrecy_n2 :
∃ c : BitVec 2 × BitVec 2,
Enc2_dist_n2 m10 m20 c ≠ Enc2_dist_n2 m11 m21 c := by

-- choose c generated by taking k = 0 and encrypting (m10,m20)
let k0 : BitVec 2 := 0
let c := (OTP_Enc k0 m10, OTP_Enc k0 m20)
use c

have p1 : Enc2_dist_n2 m10 m20 c = 1/4 := by
-- = (1 : ENNReal) / (Fintype.card (BitVec 2) : ENNReal) := by
unfold Enc2_dist_n2 OTP_Gen
simp [Bind.bind,PMF.bind_apply, PMF.pure_apply, PMF.uniformOfFintype]
unfold OTP_Enc m10 m20
simp [c, OTP_Enc, k0,m10,m20]
have (a b : BitVec 2) : a = b ↔ b = a := by exact eq_comm
simp [this]
norm_cast

have p2 : Enc2_dist_n2 m11 m21 c = 0 := by
unfold Enc2_dist_n2 OTP_Gen
simp [Bind.bind,PMF.bind_apply, PMF.pure_apply, PMF.uniformOfFintype]
intro k
unfold OTP_Enc m11 m21
simp [c,OTP_Enc,k0,m10,m20]
intro kval
rw [kval.symm]
norm_num
norm_cast

rw [p1,p2]
norm_num