今回は完全秘匿性の話題に戻り、シャノンの論文でも証明されている、鍵の集合$K$と平文の集合$M$の大きさに関する定理をLean4で形式化して証明します。
https://tcc.c.titech.ac.jp/yasunaga/appmath6/perfect.pdf
では定理６として述べられている次の定理です。
定理 6 (Shannon の定理) 秘密鍵暗号方式 $(M, K,Gen, Enc, Dec)$ が完全秘匿であるならば，$|K| \ge |M|$.
平文集合$M$も鍵集合$K$もそれぞれ一定の長さのビット列からなるとすると、鍵の長さの方が平文の長さよりも長い、という風にも解釈できます。
この定理の驚きは、暗号アルゴリズム$Enc, Dec$に寄らずに成り立つ、というところです。
PDFでは簡潔な証明が11行で述べられています。流れとしてはこんな感じです。
1. 背理法を使います。$|K| \lt |M|$として矛盾を導きます。
2. 適当に$k_0\in K$, $m_0 \in M$を選んで暗号化し$c_0 \in C$を得ます。
3. $K$の全ての鍵を使って$c_0$を復号して得られる平文の集合を$S_0$とします。この定義から$|S_0| \le |K|$です。
4. $|S_0| \le |K| \lt |M|$から$S_0$に含まれない平文があることがわかります。これを１つとって$m_1$とします。
5. $m_1$の定義から$Enc(k, m_1)=c_0$となるような$k$は存在しません。従って$Pr(k \leftarrow Gen, Enc(k, m_1)=c_0) =0$です。
6. 一方$m_0$の定義から $Pr(k \leftarrow Gen, Enc(k, m_0) =c_0) \gt 0$です。
7. これは完全秘匿性の定義式
$$ Pr(k \leftarrow Gen, Enc(k, m_0)=c_0) = Pr(k \leftarrow Gen, Enc(k, m_1)=c_0) $$
に矛盾します。
証明の途中で必要だったので、この定理６に２つの条件を追加してLean4では以下のように形式化してみました。
def full_support {T : Type} (A : PMF T) :Prop := ∀t:T, t∈A.support
theorem K_GE_M (Enc : K → M → C) (Dec : K → C → M) (Gen : PMF K) :
(full_support Gen ∧ correctness Enc Dec ∧ perfect_secrecy Enc Gen)
→ Fintype.card K ≥ Fintype.card M := by
full_supportとはPMFの台となる有限型の全ての要素に0より大きい確率が定義される、という意味です。
その上で、$K\_GE\_M$という定理の意味は、与えられた暗号システム$K, M, C, Enc, Dec, Gen$が、鍵についてfull_supportであり$Enc, Dec$が正当性を満たし、$Enc, Gen$が完全秘匿性を持てば$K$の要素数は$M$の要素数以上である、ということです。追加した２つの条件はGenがfull_supportであることと暗号の正当性でした。
Lean4による証明はほぼ上記の流れに沿っているのですが、それぞれが10行から15行くらいあり、それにプラスアルファの部分を合わせると全体は90行弱の証明になってしまいました。上記の各ステップに対応する形で概要を下記にお見せします。
theorem K_GE_M (Enc : K → M → C) (Dec : K → C → M) (Gen : PMF K) :
(full_support Gen ∧ correctness Enc Dec ∧ perfect_secrecy Enc Gen)
→ Fintype.card K ≥ Fintype.card M := byby_contra K_M
have m₀:M := default
have k₀:K := default
let c₀:C := Enc k₀ m₀
let f : K → M := fun k => Dec k c₀
-- let S₀ := {m:M | ∃k:K, m=Dec k c₀}
let S₀ := Finset.image f Finset.univ...
obtain ⟨m₁, hm₁⟩ : ∃m₁:M, ¬ m₁ ∈ S₀ := by
...
have Enc_m1_ne_c₀ : ∀ k : K, Enc k m₁ ≠ c₀ := by
...
have Enc_m1_zero : (Enc_dist Enc Gen m₁) c₀ = 0 := by
...
have Enc_m0_pos : (Enc_dist Enc Gen m₀) c₀ > 0 := by
...
have ps := FullGen_CR_PS.2.2 m₀ m₁ c₀
simp_all
1. に対応するのがby_contra K_Mです。K_Mは結論を否定したFintype.card K < Fintype.card Mとなり、仮定に付け加えられます。ゴールはFalseに変わり、なにかしら矛盾を導くことが仕事になります。
2. に対応するのが、
have m₀:M := default
have k₀:K := default
let c₀:C := Enc k₀ m₀
の部分です。ここでは略してありますが、[Inhabited M] [Inhabited K]が宣言されており、その場合にはK, Mから元を適当に選ぶことがdefaultという関数で可能になります。
3. に対応するのがlet S₀ := Finset.image f Finset.univです。Finset.univはFinset.univ Kであり、その全ての元でf (c₀を復号する)を呼び出して作られるimageがS₀ です。
4.に対応するのが、obtain ⟨m₁, hm₁⟩ : ∃m₁:M, ¬ m₁ ∈ S₀ := by の部分です。このobtainを実行すると、仮定に m₁:Mとhm₁ : ¬ m₁ ∈ S₀が付け加えられます。
5. に対応するのが、have Enc_m1_zero : (Enc_dist Enc Gen m₁) c₀ = 0 := by、
6. に対応するのがhave Enc_m0_pos : (Enc_dist Enc Gen m₀) c₀ > 0 := by です。
7. に対応するのが have ps := FullGen_CR_PS.2.2 m₀ m₁ c₀ です。これで仮定に
ps : (Enc_dist Enc Gen m₀) c₀ = (Enc_dist Enc Gen m₁) c₀
が加わります。すでに仮定には5, 6で上式の「左辺が正、右辺がゼロ」が加わっています。そこで最後にsimp_allで矛盾が出て、証明が終了します。
次回はLean4による証明を全てお見せします。
