完全秘匿性の証明のレポジトリを整理して新しく作り直した！

シャノンの完全秘匿性による暗号理論を勉強して、定義の形式化およびそれに基づく定理の形式証明をやってきました。それらの記事は、

から始まる一連の記事でした。せっかくなのでこれらの成果を一つのレポジトリにまとめ直して少しでもわかりやすいものにしてみました。githubのレポジトリとしては以下になります。

レポジトリのフォルダ構造はこんな感じです。

├── lake-manifest.json
├── lakefile.toml
├── lean-toolchain
├── PerfectSecrecy2
│   ├── Defs.lean
│   ├── Equivalences
│   │   ├── IndPS_Eq_IndPriorPS.lean
│   │   └── IndPS_Eq_ShannonPS.lean
│   ├── KeyReuse.lean
│   ├── KeySize.lean
│   └── OTP.lean
├── PerfectSecrecy2.lean
└── README.md

PerfectSecrecy2というフォルダの中に実際の証明のLeanファイルが入っています。このレポジトリに含まれる主な定義と定理を概観します。

以下に登場するK, M, Cは鍵、平文、暗号文を表す型です。多くの定理では有限型であることを仮定します。Enc, Decは暗号化、復号化、PMFは離散確率分布関数（確率質量関数）で、例えばPMF Kは鍵の離散確率分布関数を表します。

Defs.lean

暗号の正当性の定義

def correctness (Enc : K → M → C) (Dec : K → C → M) :=
∀ k:K, ∀ m:M, Dec k (Enc k m) = m

ある鍵で平文を暗号化して、同じ鍵で復号化すると元の平文に戻る、というあれです。ただこの性質を仮定せずに得られる結果が多いです。

シャノンの完全秘匿性の定義

def shannon_perfect_secrecy (Enc : K → M → C) (Gen : PMF K) : Prop :=
∀ (Msg : PMF M) (m : M) (c : C),
(cipher_dist Enc Gen Msg) c ≠ 0 → posterior Enc Gen Msg m c = Msg m

シャノンの論文にも登場するPr[M=m|C=c] = Pr[M=m]、つまり暗号文cを知って平文がmである確率と無条件に平文がmである確率が同じならcからmに関する情報が漏れていない、ということです。ここではposterior Enc Gen Msg m cがPr[M=m|C=c]に相当し、Msg mがPr[M=m]に相当します。

識別不可能性による完全秘匿性の定義

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

どんなメッセージm1, m2と暗号文cに対しても、生成した鍵でm1を暗号化したらcになる確率と、生成した鍵でm2を暗号化したらcになる確率は同じであれば、cからm1やm2の情報は漏洩していない、ということです。

IndPS_Eq_ShannonPS.lean

２つの完全秘匿性の同値

theorem ind_perfect_secrecy_equiv_shannon_perfect_secrecy
　　　(Enc : K → M → C) (Gen : PMF K) :
ind_perfect_secrecy Enc Gen ↔ shannon_perfect_secrecy Enc Gen

シャノンの完全秘匿性と識別不可能性による完全秘匿性は同値であるという定理です。ちなみに意味を考えるとシャノンの完全秘匿性の定義はわかりやすいと思います。一方定義から定理を証明する際には識別不可能性を使う方が楽なようです。それはシャノンの方では任意のメッセージ分布∀ (Msg : PMF M)を扱う必要があるからです。

KeyReuse.lean

２つのメッセージを与えられた２つの鍵での暗号化の定義

def Enc₂ (Enc : K → M → C) : (K × K) → (M × M) → (C × C)
| (k₁, k₂), (m₁, m₂) => (Enc k₁ m₁, Enc k₂ m₂)

２つの鍵を独立に生成してペアにする定義
def Gen_indep (Gen : PMF K) : PMF (K × K) := do
let k₁ ← Gen
let k₂ ← Gen
PMF.pure (k₁, k₂)

１つの鍵を生成してペアにする定義

def Gen_reuse (Gen : PMF K) : PMF (K × K) := do
let k ← Gen
PMF.pure (k, k)

もとのEnc, Genが完全秘匿なら、独立生成した２つの鍵による暗号化では完全秘匿が保たれるという定理

theorem ind_perfect_secrecy_two_time_indep_key
(Enc : K → M → C) (Gen : PMF K) :
ind_perfect_secrecy Enc Gen →
ind_perfect_secrecy (Enc₂ Enc) (Gen_indep Gen)

もとのEnc, Genが何であっても、１つの鍵を使い回すと絶対に完全秘匿にはならないという定理

theorem ind_perfect_secrecy_broken_two_time_same_key
(Enc : K → M → C) (Gen : PMF K) (h_inj_enc : ∀ k : K, Function.Injective (Enc k))
(hM : ∃ m₁ m₂ : M, m₁ ≠ m₂) :
¬ ind_perfect_secrecy (Enc₂ Enc) (Gen_reuse Gen)

この定理からは、実はEncが単射という条件だけで、鍵を再利用すると完全秘匿にならないことが分かります。当然Encが完全秘匿を満たしているとしても（そこからEncの単射性が証明できるので）、鍵の再利用はEncの完全秘匿性を壊してしまうわけです。

KeySize.lean

正当で完全秘匿な暗号系では、鍵の集合のサイズは平文の集合のサイズ以上、という定理

theorem K_GE_M (Enc : K → M → C) (Dec : K → C → M) (Gen : PMF K)
(h_correct : correctness Enc Dec)
(h_ind_PS : ind_perfect_secrecy Enc Gen) :
Fintype.card K ≥ Fintype.card M

シャノンの有名な定理「完全秘匿性を得るためには鍵空間のサイズは平文空間のサイズより大きいことが必要」という定理です。

OTP.lean

One Time Pad (OTP)暗号の定義

def OTP_Enc (n : ℕ) (k : BitVec n) (m : BitVec n) : BitVec n :=
k ^^^ m

def OTP_Dec (n : ℕ) (k : BitVec n) (c : BitVec n) : BitVec n :=
k ^^^ c

One Time Pad暗号では鍵は鍵空間から一様ランダムに選ぶ定義

def OTP_Gen : PMF (BitVec n) :=
PMF.uniformOfFintype (BitVec n)

OTPは完全秘匿性をもつ

theorem OTP_is_ind_perfectly_secret :
ind_perfect_secrecy (OTP_Enc n: BitVec n → BitVec n → BitVec n)
(OTP_Gen : PMF (BitVec n))

こちらも大変有名な定理である、OTPの完全秘匿性を述べています。

全ての定理についてsorryやadmitを使わない検証済みの証明がついています。zipをダウンロード、解凍して、そのディレクトリで

lake clean; lake update; lake exe cache get; lake build