Lean4によるワンタイムパッド暗号の完全秘匿性の形式証明

シャノンが暗号に関する論文で「完全秘匿性」という概念を定式化したことを紹介し、そのLean4での形式化までを前回の記事で紹介しました。

この概念がただの抽象概念で、そのような性質を満たす暗号など簡単には作れない、、、という話かというとそうではありません。具体的に構成できるワンタイムパッド暗号という暗号方式ではこの完全秘匿性がまさに成り立ちます。

今回はこのワンタイムパッド暗号を紹介し、Lean4での形式化を見ていただきます。さらにワンタイムパッド暗号が完全秘匿性を持つことの証明をLean4で形式化してみました。形式証明の一部をお見せしたいと思います。

ワンタイムパッド暗号の定義

nを与えられたセキュリティパラメータとして、Mは平文の集合、Kは鍵の集合、Cは暗号文の集合とします。以下を満たす暗号システムをワンタイムパッド暗号と定義します。

$M = K = C =$ nビットのビット列の集合

$m\in M, k\in K$に対して、$Enc (k, m) = k\, \oplus m$, $Dec (k, c)=k\, \oplus c$、ただし$\oplus$はビットごとの排他論理和を表します。

鍵の集合$K$から鍵を取りだすアルゴリズム$Gen$は一様ランダムに値を１つ取り出す関数とし、暗号化のたびに異なる鍵を使用することにします。

コンピュータの中で文字列はバイトの並びで表されます。1バイトは8ビットの並びですから結局長さ$m$バイト分の文字列は$8\,m$ビットの長さのビット列になります。これを同じビット長の鍵とビットごとに排他論理和をとっていくと暗号化ができます。復号化も同じ手順です。

なんとも単純な暗号システムですね。特徴としては鍵の長さがとても長く、暗号化したい平文と同じ長さが要求されている点です。日常使われている共有鍵暗号、例えばAES256では鍵長は256ビット固定です。長いメッセージを１つの鍵を使ってAES256で暗号化する場合には長いメッセージを256ビットに区切り、それらを同じ鍵で暗号化します。たとえ1GBのファイルを暗号化する場合にも鍵長は256ビットです。一方ワンタイムパッド暗号では1GBのファイルを暗号化するには1GB=8Gビットの鍵が必要になります。

では早速Lean4による定義をみてみましょう。

variable {n : ℕ}

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

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

example : correctness (@OTP_Enc n) (@OTP_Dec n) := by
  unfold OTP_Enc OTP_Dec correctness
  intro k m
  simp
  rw [← BitVec.xor_assoc, BitVec.xor_self, BitVec.zero_xor]

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

まずBitVec nという型が平文、鍵、暗号文の型として使われています。Lean4ですでに定義されている型で長さ$n$のビット列を表すことができます。またBitVec n型には^^^という演算が定義されています。ビットごとの排他的論理和の演算です。

OTP_Enc, OTP_Decをビットごとの排他論理和の演算で定義します。そしてこれらがcorrectnessの性質を満たす頃を証明しています。correctnessは前回暗号システムと完全秘匿性の定義の中で定義したものをそのまま使っています。証明はcorrectnessの定義、OTP_Enc, OTP_Decの定義を展開して、ビットごとの排他論理和演算の結合法則及び簡単な演算結果を持って証明できました。

最後に鍵生成アルゴリズムをOTP_Genとして確立質量関数として定義してあります。BitVec n型の全ての要素が等しい確率で鍵として選ばれます。

これでワンタイムパッド暗号を構成するOTP_Enc, OTP_Dec, OTP_Genがすべて定義できました。また暗号の正当性も証明できました。ビットごとの排他的論理和に関する簡単な補題を示し、最後に完全秘匿性の証明をお見せします。

lemma mkc_symm (m k c : (BitVec n)) : c=k^^^m ↔ k=c^^^m := by
  constructor
  · intro hc
    rw [hc, BitVec.xor_assoc, BitVec.xor_self, BitVec.xor_zero]
  · intro hk
    rw [hk, BitVec.xor_assoc,BitVec.xor_self, BitVec.xor_zero]

c=k^^^mとk=c^^^mが同値であるという補題です。ビットごとの排他的論理和ではごく当然成り立つ式です。証明もほぼ正当性の証明と同様な道具を使って終了します。

最後に完全秘匿性の証明です。perfect_secrecyという性質は前回定義したものをそのまま使っています。

theorem OTP_is_perfectly_secret :
  perfect_secrecy (@OTP_Enc n) (@OTP_Gen n) := by
    intro m₁ m₂ c

    unfold  Enc_dist
    simp_rw [Bind.bind]
    unfold OTP_Gen OTP_Enc

    simp [PMF.bind_apply]
    simp [mkc_symm]

証明はまずperfect_secrecyの定義を展開します。さらにEnc_distの定義を展開し、確率モナドのdo記法を展開します。そこに残っているOTP_Gen, OTP_Encの定義を展開します。最後に証明済みの補題を使って整理すると証明が終了する算段です。