最近の記事では暗号とその安全性証明の基礎を勉強したいと思い、シャノンの完全秘匿性やそれを実装するワンタイムパッド暗号、完全秘匿性を持つ暗号における鍵の長さに関する定理の証明などを勉強しました。安永さん（東工大の先生ですね）の本を購入し、また公開されているPDFなどを大いに参考にさせていただきました。
- 暗号システムと完全秘匿性の定義
- ワンタイムパッド暗号の定義と完全秘匿性を満たすことの証明
- 完全秘匿性を満たす暗号での鍵集合と平文集合の大きさに関する定理の証明
を行い、そのLean4での形式化を紹介してきました。最後の定理については前回の記事でその証明の流れを説明しました。
上記全てをGithubにレポジトリとして公開しましたので、興味のある人はぜひ見てみてください。レポジトリはこちらです。
上記のリポジトリにもありますが、とりあえず前回の証明のフルバージョンを見たい方のために証明を貼っておきます。
import PerfectSecrecy.PerfectSecrecy_Def
open PMF
open Set
variable {M K C : Type}
variable [Fintype M] [Inhabited M] [DecidableEq M]
variable [Fintype K] [Inhabited K]
variable [Fintype C] [Inhabited C] [DecidableEq C]
def full_support {T : Type} (A : PMF T) :Prop := ∀t:T, t∈A.support
omit [Fintype C] [Inhabited C]
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
intro FullGen_CR_PS
by_contra K_M
push_neg at K_M
have m₀:M := default
have k₀:K := default
let c₀:C := Enc k₀ m₀
have hc₀ : c₀=Enc k₀ m₀ := by rfl
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
have S₀_le_K: S₀.card ≤ @Fintype.elems.card K := by
exact Finset.card_image_le
have S₀_lt_M : S₀.card < Fintype.card M := by
exact Nat.lt_of_le_of_lt S₀_le_K K_M
obtain ⟨m₁, hm₁⟩ : ∃m₁:M, ¬ m₁ ∈ S₀ := by
by_contra hc
push_neg at hc
have : S₀=Finset.univ := by
exact Finset.eq_univ_iff_forall.mpr hc
simp_rw [this] at S₀_lt_M
exact (lt_self_iff_false Finset.univ.card).mp S₀_lt_M
have Enc_m1_ne_c₀ : ∀ k : K, Enc k m₁ ≠ c₀ := by
intro k
by_contra contra
apply hm₁
have correct:= FullGen_CR_PS.2.1 k m₁
rw [contra] at correct
rw [Finset.mem_image]
use k
constructor
· exact Finset.mem_univ k
· exact correct
have Enc_m1_zero : (Enc_dist Enc Gen m₁) c₀ = 0 := by
simp only [Enc_dist, Bind.bind, PMF.bind_apply, PMF.pure_apply]
rw [tsum_eq_sum]
· apply Finset.sum_eq_zero
intro k _
have : c₀ ≠ Enc k m₁ := by exact fun a => Enc_m1_ne_c₀ k (id (Eq.symm a))
rw [if_neg this]
simp
· intro k _
have : c₀ ≠ Enc k m₁ := by exact fun a => Enc_m1_ne_c₀ k (id (Eq.symm a))
rw [if_neg this]
simp
· exact Finset.empty
have Enc_m0_pos : (Enc_dist Enc Gen m₀) c₀ > 0 := by
simp only [Enc_dist, Bind.bind, PMF.bind_apply, PMF.pure_apply]
have single_le_tsum: (fun a => Gen a * if c₀ = Enc a m₀ then 1 else 0) k₀
≤ (∑' (a : K), Gen a * if c₀ = Enc a m₀ then 1 else 0) := by
exact ENNReal.le_tsum k₀
have single_gt_zero: 0<(fun a => Gen a * if c₀ = Enc a m₀ then 1 else 0) k₀ := by
simp_all [c₀]
have : k₀∈ Gen.support := by
apply FullGen_CR_PS.1
exact (apply_pos_iff Gen k₀).mpr this
apply lt_of_lt_of_le single_gt_zero
simp_all
have ps := FullGen_CR_PS.2.2 m₀ m₁ c₀
simp_all
