意味的安全性と計算量的識別不可能性の定義を再掲し、それぞれのLean4による形式化をみてみます。簡単な方から行くのが良いですよね。まずは定義3.5とその形式化です。
定義3.5 (t, ε)-識別不可能性 共通鍵暗号方式(Enc, Dec)が(t, ε)-識別不可能であるとは、計算量t以下の任意の攻撃者$(A_1, A_2)$に対して、
$$ p_b = Pr [ (m_0, m_1, st) \leftarrow A_1 ; c\leftarrow Enc_K(m_b) : A_2 (c,st)=1]$$
と定めた時、
$$| p_0 - p_1| \le \epsilon $$
を満たすことです。
noncomputable def p0 (Enc : K → M → C) (Gen : PMF K)
(A1 : PMF (M × M × St)) (A2 : C → St → PMF Bit) : ENNReal :=
(do let (m0, _, st) ← A1; let k ← Gen; A2 (Enc k m0) st) 1noncomputable def p1 (Enc : K → M → C) (Gen : PMF K)
(A1 : PMF (M × M × St)) (A2 : C → St → PMF Bit) : ENNReal :=
(do let (_, m1, st) ← A1; let k ← Gen; A2 (Enc k m1) st) 1/-- Definition 3.5: (t, ε)-Indistinguishability.
An encryption scheme (Enc, Gen) is (t, ε)-indistinguishable if
for every adversary (A1, A2) with combined complexity at most t,
the advantage |p0 - p1| in distinguishing encryptions of m0 and m1 is at most ε.
-/
def Indistinguishable (Enc : K → M → C) (Gen : PMF K)
(t : ℕ) (ε : NNReal) : Prop :=
∀ (A1 : PMF (M × M × St)) (A2 : C → St → PMF Bit) (tA1 tA2 : ℕ),
tA1 + tA2 ≤ t → |(p0 Enc Gen A1 A2).toReal - (p1 Enc Gen A1 A2).toReal| ≤ (ε : ℝ)
定義3.5のPrの中身とp0, p1の定義は大体対応していることはわかります。Lean4のコードでは鍵生成を明示していること、暗号文をcとせず直接$A_2$の引数にしていることが変化点です。
次に定義3.4の再掲とそのLean4による形式化を見てみます。まあわかりにくいので雰囲気だけでも、、、という感じです。
定義3.4 意味的安全性 共通鍵暗号(Enc, Dec)が(t, α, ε)-意味的安全性であるとは、計算量t以下の任意の攻撃者(A1, A2)に対し、シミュレータSで(A1, S)の計算量がt+α以下のものが存在して、
$$p_a = Pr [(M,h,R,st) \leftarrow A_1 ; m \leftarrow M ; a \leftarrow A_2 ( (Enc_K(m), h(m), st) : R(m, a)=1]$$
$$p_s = Pr [(M,h,R,st) \leftarrow A_1 ; m \leftarrow M ; s \leftarrow S(h(m), st) : R(m, s)=1]$$
と定めた時、
$$| p_a - p_s| \le \epsilon $$
を満たすことです。
noncomputable def pa (Enc : K → M → C) (Gen : PMF K)
(A1 : PMF (PMF M × (M → Bit) × (M → Bit → Bit) × St))
(A2 : C → Bit → St → PMF Bit) : ENNReal :=
(do let (mDist, h, R, st) ← A1; let m ← mDist; let k ← Gen;
let a ← A2 (Enc k m) (h m) st; PMF.pure (R m a)) 1noncomputable def ps (A1 : PMF (PMF M × (M → Bit) × (M → Bit → Bit) × St))
(S : Bit → St → PMF Bit) : ENNReal :=
(do let (mDist, h, R, st) ← A1; let m ← mDist; let s ← S (h m) st;
PMF.pure (R m s)) 1/-- Definition 3.4: (t, α, ε)-Semantic Security.
An encryption scheme (Enc, Gen) is (t, α, ε)-semantically secure if
for every adversary (A1, A2) with combined complexity tA1 + tA2 ≤ t,
there exists a simulator S with complexity tS ≤ tA1 + tA2 + α such that
the advantage |pa - ps| is at most ε. -/
def SemanticallySecure
(Enc : K → M → C) (Gen : PMF K) (t α : ℕ) (ε : NNReal) : Prop :=
∀ (A1 : PMF (PMF M × (M → Bit) × (M → Bit → Bit) × St))
(A2 : C → Bit → St → PMF Bit)
(tA1 tA2 : ℕ), tA1 + tA2 ≤ t →
∃ (S : Bit → St → PMF Bit) (tS : ℕ),
tS ≤ tA1 + tA2 + α ∧ |(pa Enc Gen A1 A2).toReal - (ps A1 S).toReal| ≤ (ε : ℝ)
Lean4による形式化ではh, Rなどは任意の関数として抽象化されていて、意味は分かりにくいですが、定義自体はコンパクトです。
ここまでくるとIndistinguishableとSemanticallySecureの同値性を示す２つの定理の形式化を見ることができます。
定理3.1 共通鍵暗号方式(Enc, Dec)は、(t, α, ε/2)-意味的安全であれば、(t, ε)-識別不可能である。ここでα≧0は任意の値である。
theorem semantic_security_implies_indistinguishable
(Enc : K → M → C) (Gen : PMF K) (t α : ℕ) (ε : NNReal)
(hss : SemanticallySecure (St := St) Enc Gen t α (ε / 2)) :
Indistinguishable (St := St) Enc Gen t ε := by
定理3.2 共通鍵暗号方式(Enc, Dec)は、($t + t_M + t_h + t_R$, ε)-識別不可能であるとき、($t, t_{Gen} + t_{Enc}$, ε)-意味的安全である。theorem indistinguishable_implies_semantically_secure
(Enc : K → M → C) (Gen : PMF K)
(t tM th tR tGen tEnc : ℕ) (ε : NNReal)
(hind : Indistinguishable (St := St_B M St)
Enc Gen (t + tM + th + tR) ε) :
SemanticallySecure (St := St) Enc Gen t (tGen + tEnc) ε := by
ここで１点白状すると、アルゴリズムの計算量はt+tM+th+tRのように定理の条件には登場しますが、それ以上の役割はありません。ちゃんとやるためにはdo文の中の確率試行の計算量を自動で見つけ出す必要があり、定式化も形式化も非常に難しいです。このシリーズではその計算は箸折ってあると思ってください。
証明は以下のレポジトリにあります。
Defs.leanに上記の意味的安全性、計算量的識別不可能性の定義があります。SemSec_Implies_Ind.leanには定理3.1の証明があります。Ind_Implies_SemSec.leanには定理3.2の証明があります。
レポジトリはこちらです。
