擬似乱数生成器伸長定理の証明の流れ

擬似乱数を1bit伸ばすことができれば、任意の長さの擬似乱数に伸ばすことができます。この定理をLean4で形式化しました。

定理4.1 擬似乱数生成器$G : \{0,1\}^n \rightarrow \{0,1\}^{n+1}$に対し、$G':\{0,1\}^n \rightarrow\{0,1\}^L$を「 $x_0 = x, i=0,\dots , L-1$に対し、$G(x_i )=(x_{i+1}, b_{i+1})$としたとき$G'(x)=(b_1,\dots ,b_L)$ 」と定める。このときGが$(t+L\,t_G+O(L), \frac{\epsilon}{L})$-擬似乱数生成器であれば、G'は$(t,\epsilon)$-擬似乱数生成器である。ここで$t_G$は関数Gを評価するための計算量である。

theorem PRG_Sequential_Extension
(n L : ℕ) (hL : L > 0)
(G : BitVec n → BitVec (n + 1))
(t : ℕ) (ε : NNReal) (cost_G : ℕ)
(h_G_secure : DistIndistinguishable ( (U n).map G ) (U (n + 1)) (t + L * cost_G) (ε / L)) :
DistIndistinguishable ( (U n).map (G' G L) ) (U L) t ε := by

証明はどうすれば可能でしょうか。G'はL bitの列$(b_1,\dots ,b_L)$を出力します。G'にn bitの一様乱数を入力すると出力がL bitの疑似乱数になる、ということは$(b_1,\dots ,b_L)$の分布がU Lと計算量的に識別不可能を示せば良いわけです。そのための道具としてハイブリッド論法がありました。確率分布U Lと$(b_1,\dots ,b_L)$の分布の間に中間的な確立分布を作り、そのどのステップも計算量的に識別不可能を示せば、証明は終了します。

中間の確率分布の作り方はこんな感じです。

この図で$Y_i$は$b_i$の分布だと思ってください。するとこの図の一番上が$H_0=U_L$、一番下が$H_L=(b_1,\dots ,b_L)$の分布、となっていることがわかります。途中の分布は短い一様分布と$(b_1,\dots ,b_L)$の分布の先頭部分をビット連結したものになっていることがわかります。$H_i$と$H_{i+1}$の差は一様分布が1bit短くなり$(b_1,\dots ,b_L)$由来の分布が1bit長くなっています。

確立分布$H_i$のLean4による定義をみてみましょう。

noncomputable def Hybrid (i : ℕ) : PMF (BitVec L) :=
if h : i <= L then
do
let u_pre ← U (L - i) -- (L-i) uniform random bits
let seed ← U n
let suffix := G' G i seed -- i PRG output bits
return (u_pre ++ suffix).cast (by omega)
else
G'_dist G L

このコードでu_preが一様分布、suffixが$b_i$を集めたビット列になります。それぞれの長さが1 bitづつ変化していてビット連結したu_pre++suffixの長さは常にL bitであることがわかります。

ここまで来ると証明の方針は次の３つを証明することになります。

$H_0 = U_L$
$H_L = G'\, G\, L\, U_n$
$DistIndistinguishable\, H_i\, H_{i+1}$

これらは以下のLean4のコードに登場します。

lemma Sequential_Extension_Step
(n L : ℕ) (G : BitVec n → BitVec (n + 1)) (i : ℕ) (hi : i < L)
(t : ℕ) (ε : NNReal) (cost_G : ℕ)
(h_G_secure : DistIndistinguishable ( (U n).map G) (U (n + 1) ) (t + L * cost_G) (ε / L)) :
DistIndistinguishable (Hybrid G L i) (Hybrid G L (i + 1)) t (ε / L) := by

theorem PRG_Sequential_Extension
(n L : ℕ) (hL : L > 0)
(G : BitVec n → BitVec (n + 1))
(t : ℕ) (ε : NNReal) (cost_G : ℕ)
(h_G_secure : DistIndistinguishable ( (U n).map G) (U (n + 1) ) (t + L * cost_G) (ε / L)) :
DistIndistinguishable ( (U n).map (G' G L) ) (U L) t ε := by
-- Hybrid 0 equals U L (all random bits).
have h_end : U L = Hybrid G L 0 := by
...
-- Hybrid L equals the G' distribution (all PRG bits, zero random bits).
have h_start : (U n).map (G' G L) = Hybrid G L L := by
...
...