まずはなにあれ、一様分布を定義しましょう。一様分布$U_n$とは長さnの全てのビット列の集合$\{0,1\}^n$の各要素について確率$\frac{1}{2^n}$を割り当てた分布として定義します。集合$\{0,1\}^n$の要素の数は$2^n$ですからすべての要素に確率を均等に割り当てると一様分布$U_n$になります。
一様分布と計算量的に識別できない確率分布を擬似ランダム分布、擬似ランダム分布に従って乱数を生成する関数を擬似乱数生成器といいます。数学的な定義は以下の通りです。
定義4.3 擬似ランダム分布：確率分布Xが(t,e)-擬似ランダムであるとは、あるnについてXが$U_n$と(t,e)-識別不可能であることである。
定義4.4 擬似乱数生成器：関数$G : \{0,1\}^n \rightarrow \{0,1\}^m$は$G (U_n)$が(t,e)-擬似ランダムである時(t,e)-擬似乱数生成器という。
関数Gは決定的な関数であり、入力（長さnのビット列）が１つ決まれば出力（長さmのビット列）が一意に定ります。そして入力が$U_n$に従っている時、出力の確率分布$G(U_n)$が$U_m$と(t,e)-識別不可能であればGは擬似乱数生成器といいます。特にn<mであればGは$U_n$からサンプルした長さnの鍵を長さmの鍵に伸ばすことに使えます。
これで道具立てが揃いました。以下、完全秘匿な暗号方式で鍵生成だけを平文より短い鍵に変更すると(完全秘匿は失われますが)計算量的安全性は確保できることを見ていきます。
安永先生の本ではmビットのOTP暗号において、鍵生成をmビットの一様分布からの生成の代わりにそれよりも短いnビットの一様分布から生成した乱数をGでmビットに伸ばした物を使う暗号系を定義しています。そしてその暗号方式が(t,e)-識別不可能であることを証明しています（命題4.4）。
この定理によってXORによる暗号方式ではnビットの鍵を元にしてmビットの擬似乱数を作り、それを鍵としてmビットの平文を暗号化しても計算量的安全性は保たれることが示されています。
実はこれよりも少し一般的な結果を証明することができます。次のような定理です。
theorem IndPS_PRG_implies_Computational_Indistinguishability
(n m : ℕ) [Fintype (BitVec n)] [Fintype (BitVec m)]
[Fintype M] [Fintype K] [Fintype C] [DecidableEq C]
(Enc : (BitVec m) → M → C)
(G : BitVec n → BitVec m)
(t t_enc : ℕ) (ε : NNReal)
(h_ind_ps : ind_perfect_secrecy Enc (U m))
(h_prg : IsPRG G (t + t_enc) (ε / 2)) :
∀ (St : Type) [Fintype St] [Inhabited St],
Indistinguishable Enc (PMF.map G (U n)) t ε (St := St) := by
つまりOTPに限らず、暗号方式(Enc, (U m))が完全秘匿ならば、鍵生成を(t+t_enc,ε/2)-擬似乱数生成器Gで置き換えた暗号方式(Enc, G (U n))は(t,ε)-識別不可能が言えるのです。この一般化は結構綺麗だと思うのですが、安永先生の本では明示的には出てこないようです。
とは言ってもこの定理の証明はOTPの場合の命題4.4の証明と大きく変わるわけではありません。まず暗号方式(Enc, G (U n))では任意の２つのメッセージm0, m1について暗号文の分布が計算量的識別不可能であることを示します。この証明ではハイブリッド論法という技法を使います。
let P0 := Enc_dist Enc (PMF.map G (U n)) m0
let P1 := Enc_dist Enc (PMF.map G (U n)) m1
let Q0 := Enc_dist Enc (U m) m0
let Q1 := Enc_dist Enc (U m) m1
としたときに、P0とQ0、Q0とQ1、Q1とP1が計算量的識別不可能であることを示します。特にQ0とQ1は完全秘匿性の条件h_ind_psからQ0=Q1であることがわかります。これらを示した後で前回紹介した推移性命題4.3を使うことで暗号文の分布P0とP1の(t,e)-識別不可能性が示せます。この部分はsecurity_transferという名前の定理に切り出してあります。
theorem security_transfer
(n m : ℕ) [Fintype (BitVec n)] [Fintype (BitVec m)]
(Enc : (BitVec m) → M → C)
(G : BitVec n → BitVec m)
(t t_enc : ℕ) (ε : NNReal)
(h_perf : ind_perfect_secrecy Enc (U m))
(h_prg : IsPRG G (t + t_enc) (ε / 2)) :
∀ m0 m1, DistIndistinguishable
(Enc_dist Enc (PMF.map G (U n)) m0)
(Enc_dist Enc (PMF.map G (U n)) m1) t ε := by
次に暗号文の分布の(t,e)-識別不可能性から暗号方式の(t,e)-識別不可能性を導く必要があります。暗号文を見て攻撃者A2がm0を暗号したものと答える確率やm1を暗号したものと答える確率を計算しその差がe未満であることを示します。こちらも以下の形で定理として切り出してあります。
def FixedMessageIndistinguishable
(Enc : K → M → C) (Gen : PMF K) (t : ℕ) (ε : NNReal) : Prop :=
∀ (m0 m1 : M), DistIndistinguishable (Enc_dist Enc Gen m0) (Enc_dist Enc Gen m1) t ε
theorem indistinguishability_equivalence
(Enc : K → M → C) (Gen : PMF K) (t : ℕ) (ε : NNReal)
[Fintype M] [Fintype K] [Fintype C] [DecidableEq C] :
FixedMessageIndistinguishable Enc Gen t ε ↔
(∀ (St : Type) [Fintype St] [Inhabited St], Indistinguishable Enc Gen t ε (St := St)) := by
実は暗号文の分布の(t,e)-識別不可能性と暗号方式の(t,e)-識別不可能性は同値です。レポジトリでは双方向で証明してあります。
ここまでの結果をまとめてIndPS_PRG_implies_Computational_Indistinguishabilityという定理を２行で証明できます。
theorem IndPS_PRG_implies_Computational_Indistinguishability
(n m : ℕ) [Fintype (BitVec n)] [Fintype (BitVec m)]
[Fintype M] [Fintype C] [DecidableEq C]
(Enc : (BitVec m) → M → C)
(G : BitVec n → BitVec m)
(t t_enc : ℕ) (ε : NNReal)
(h_ind_ps : ind_perfect_secrecy Enc (U m))
(h_prg : IsPRG G (t + t_enc) (ε / 2)) :
∀ (St : Type) [Fintype St] [Inhabited St],
Indistinguishable Enc (PMF.map G (U n)) t ε (St := St) := byrw [← indistinguishability_equivalence]
exact security_transfer n m Enc G t t_enc ε h_ind_ps h_prg
この定理の応用としてOTP暗号に擬似乱数生成器を組み合わせた暗号方式が(t,e)-識別不可能性を持つことも簡単に証明できます。mビットのOTP暗号は鍵生成をU mで行い完全秘匿性があります。従ってIndPS_PRG_implies_Computational_Indistinguishabilityを直接使ってこちらは３行で証明が終わります。
theorem OTP_PRG_implies_Computational_Indistinguishability
(m m' : ℕ) [Fintype (BitVec m)] [Fintype (BitVec m')]
(t t_enc : ℕ) (ε : NNReal)
(G : BitVec m → BitVec m')
(h_prg : IsPRG G (t + t_enc) (ε / 2)) :
∀ (St : Type) [Fintype St] [Inhabited St],
Indistinguishable (OTP_Enc m') (PMF.map G (U m)) t ε (St := St) := by
apply IndPS_PRG_implies_Computational_Indistinguishability
· exact OTP_is_ind_perfectly_secret
· exact h_prg
これらの内容についてもLean4のコードは公開済みです。
の中のDefs.lean, DistInd.lean, ShortKey_CompSec.leanなどのファイルをご覧ください。
