完全秘匿性という概念、せっかく数学的に定義したのですが数式が出てこないと数学している気分になれません。というわけで暗号の完全秘匿性について数式を用いて定義してみましょう。また数式化できればLean4での形式化も見たいですよね。とは言っても暗号というものを定義するために流石に少し準備が必要です。
平文（メッセージとも言います）の集合を$M$, 鍵の集合を$K$, 暗号文の集合を$C$とします。簡単のために$M, K, C$はいずれも空でない有限集合とします。そして鍵$k\in K$と平文$m \in M$を入力として、暗号文$c\in C$を作るアルゴリズムを$Enc$, 暗号文$c$と鍵$k$から平文$m$を作るアルゴリズムを$Dec$とします。また鍵の集合$K$から鍵$k$を選択するアルゴリズムを$Gen$とします。
ちなみにアルゴリズムとは確定的アルゴリズムと確率的アルゴリズムに分かれます。前者は計算量の理論におけるチューリング機械でモデル化されます。また確率的アルゴリズムはアルゴリズムの中で乱数を生成して使用できることとし、確率変数としてモデル化されます。
というわけでようやく暗号が定義できます。
暗号方式：６つ組 $(M, K, C, Gen, Dec, Enc)$ は１つの暗号方式を定める。
暗号方式の正当性：$k\in K, m\in M, c\in C$の時$c=Enc(k, m)$ならば$m=Dec(k, c)$が成り立つことを暗号方式$(M, K, C, Gen, Dec, Enc)$の正当性という。
暗号の正当性とは、ある鍵で平文を暗号化したものを同じ鍵で復号化すると元の平文が得られる、という大事な性質です。
さて前回の記事で定義した完全秘匿性を再掲し、その数式による定義を述べます。
再掲 完全秘匿性：暗号文を知る前に正しい平文を得られる確率と暗号文を知って正しい平文が得られる確率が等しい時、この暗号は完全秘匿性を持つ、と言われます。
数式版 完全秘匿性：暗号方式$(M, K, C, Gen, Enc, Dec)$で、任意の平文$m \in M$と任意の暗号文$c \in C$に関して、$Pr (m | c )=Pr(m)$が成り立つ時、この暗号方式は完全秘匿性を持つという。ここに$Pr(m | c)$は暗号文が$c$であることを知って平文が$m$である条件付き確率、$Pr(m)$は(条件なしで)平文が$m$である確率を表す。
この数式版完全秘匿性と同値であることが分かっているもう少し使いやす形の完全秘匿性についても紹介します。
完全秘匿性２：暗号方式$(M, K, C, Gen, Enc, Dec)$で、任意の平文$m_1, m_2 \in M$と任意の暗号文$c \in C$に関して、
$$ Pr(k \leftarrow Gen, Enc(k, m_1)=c) = Pr(k \leftarrow Gen, Enc(k, m_2)=c) $$
ここで$k \leftarrow Gen$は鍵$k$を鍵の集合$K$から$Gen$を使って１つ選ぶ確率事象を表します。
任意の$m_1, m_2 \in M$に対して$Gen$から生成される鍵で暗号化して得られる暗号文の分布が平文によらず等しいことを主張しています。より詳しく言えば全ての暗号文$c$について確率を求め、それらが等しいことを主張しています。
どの平文もさまざまな鍵で暗号化した結果の暗号文の分布は同じで区別できない、ということがこの主張です。
数式版完全秘匿性と完全秘匿性２が同値であることは証明できることです。また文献によっては完全秘匿性２を完全秘匿性の定義とすることもあります。ここでもこちらを定義として議論を進めます。
ではここまでの道具立てをLean4で形式化したものをお見せしましょう。perfect_secrecyの定義には完全秘匿性２を採用しています。
import Mathlib.Probability.ProbabilityMassFunction.Monad
import Mathlib.Probability.Distributions.Uniform
open PMFsection PerfectSecrecyDefinition
variable {M K C : Type}
variable [Fintype M] [Inhabited M]
variable [Fintype K] [Inhabited K]
variable [Fintype C] [Inhabited C] [DecidableEq C]
noncomputable
def correctness (Enc : K → M → C) (Dec : K → C → M) :=
∀ k:K, ∀ m:M, Dec k (Enc k m) = mnoncomputable
def Enc_dist (Enc : K → M → C) (Gen : PMF K) (m : M) : PMF C :=
do
let k ← Gen
PMF.pure (Enc k m)def 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
意外に短くまとまりました。M, K, Cは有限なタイプとして宣言してあります。正当性はcorrectnessとしてEnc, Decで元に戻ることと定義しました。
Enc_distは暗号化アルゴリズムEncと鍵生成アルゴリズムGenと具体的な平文$m$を与えて、暗号文の確率分布を返します。do文の中で鍵$k$を生成して$(Enc\, m\, k)$で暗号化していることがわかります。
perfect_secrecyは完全秘匿性２を使って定義しています。ここでは両辺で、得られた確率分布に任意の暗号文$c$を引数として与えることで暗号文が$c$である確率を計算していることに注意してください。
今回はここで終了です。次回はこの抽象的に定義された完全秘匿性を満たす具体的な暗号としてワンタイムパッド暗号を紹介します。
ちなみに以前の記事で離散確率分布をPMF (Probability Mass Function / 確率質量関数)で表す方法を紹介しました。Lean4 での確率の扱いについてはそちらをご覧ください。
