n bitの一様乱数を入力としてn+1 bitの擬似乱数をつくる擬似乱数生成器$G : \{0,1\}^n \rightarrow \{0,1\}^{n+1}$があるとします。Gを組み合わせることによって任意のL (L ≧ 1) bitまで擬似乱数を伸ばすことができます。具体的にはn bitの一様乱数を入力としてL bit擬似乱数を作る擬似乱数生成器$G':\{0,1\}^n -> \{0,1\}^L$を構成することができます。このことを数学的にきちんと定義して証明することができます（擬似乱数生成器伸長定理）。
これは何を意味していて、なぜ重要なのでしょうか。
以前にOTP暗号の鍵生成を一様乱数から擬似乱数に変更することができてその場合にも(完全秘匿性はなくなりますが)計算量的安全性は確保できることを証明しました。平文の長さが一定であればこれで暗号化ができます。
一方平文が非常に長い場合（あるいは終わりの長さが決まっていない場合）には平文を一定の長さに区切り、区切りごとに暗号していけばよさそうです。（ストリーム暗号と呼ばれています）。ただその場合鍵はどうしたら良いでしょうか。最初に一様乱数を１つ生成し、それから擬似乱数をどんどん伸ばしながら作ることができればそれらを順に鍵とすることでいくらでも長い平文を暗号化することができます。この場合暗号化する人と復号化する人の間で共有するべき鍵は最初の一様乱数だけです。そして暗号文のどの部分も異なる擬似乱数で暗号化されており、計算量的安全性は確保されそうです（別途証明が必要かもですね）。
このようなユースケースはネットワーク上では多くみられるもので、そこでの暗号利用の理論的基礎の１つがこの擬似乱数生成器伸長定理ということになります。実際の暗号プロトコル(SSL/TLSなど)では証明可能な安全性には基づかない技術も使われているため、あくまで「理論的基礎」の位置付けではあります。
この定理は安永さんの本「暗号理論入門」では定理4.1となっています。
定理4.1 擬似乱数生成器$G : \{0,1\}^n \rightarrow \{0,1\}^{n+1}$に対し、$G':\{0,1\}^n -> \{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を評価するための計算量である。
1 bit伸ばせる擬似乱数生成器Gが与えられれば任意のbit数を出力する擬似乱数生成器G'が作れること、G'はL bitの擬似乱数を出力すること、などが分かります、、、がこの定理を読んでも具体的構成がよく分かりませんね。では次の図をみてください。
Unはn bitの一様乱数分布でそこからxをサンプルし上記の構成に入力します。左端のGによってn+1 bitの疑似乱数が出力されるのですが、そのうちのMSBの1 bitを$b_1$、のこりのn bitを$x_1$とします。あとはこの過程を繰り返し1bitをL個集めます。集まった$(b_1, \dots , b_L)$がG'の出力となります。これをフォーマルに書いたのが先ほどの定義です。よく読むと図の中の記号がいい感じ(!?)で登場しているのが分かります！
まずこの構成をLean4で書いてみましょう。Gは与えられたものとします。n+1 bitを$(b_i, x_i)$に分割する部分、ループさせてできた1bitを拾い集める部分、拾い集めたbit列をG'の出力とする部分と考えると以下のようになります。
/-- n+1 bitを1 bitのbiとn bitのxiに分割する関数 -/
def split_next (v : BitVec (n + 1)) : BitVec 1 × BitVec n :=
let v_aligned : BitVec (1 + n) := v.cast (by omega)
let p := bitvec_equiv 1 n v_aligned
(p.1, p.2)/-- Gを繰り返し適用してループさせる部分とbiを拾い集める部分 -/
def G_ext (G : BitVec n → BitVec (n + 1)) : (L : ℕ) → BitVec n → BitVec L
| 0, _ => BitVec.zero 0
| l + 1, s =>
let res := G s
let (bit, s_next) := split_next res
bit ++ G_ext G l s_next |>.cast (by omega)/-- 拾い集めたビット列をG'の出力にする部分 -/
def G' (G : BitVec n → BitVec (n + 1)) (L : ℕ) (s : BitVec n) : BitVec L :=
G_ext G L s
これらの関数は適当なGを与えれば実行な関数として定義されています。
GやG'が準備できたので定理4.1をLean4で形式化することができます。こんな感じになります。
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
DistIndistiguishableは２つの確率分布が計算量的に識別できない、ということを表す命題でした。(U n)はn bitの一様分布でした。したがって仮定にあるh_G_secureはGの入力がn bitの一様分布であるとき、その出力の分布はn+1 bitの一様分布と計算量的に識別できない、と読むことができます。まさにGは1 bit伸ばしの疑似ランダム生成器、という仮定です。
そして結論部分ではG' (= G' G L)の入力がn bitの一様分布であるとき、G'の出力はL bitの一様分布と区別できないと読むことができます。まさに関数G'はL bit出力の疑似ランダム生成器という結論です。
計算量のパラメータの部分も含めて定理4.1と完全に対応していることが分かります。
