Cached expansions between adjacent GGM levels

Cache one expansion per queried parent prefix. Generator outputs reproduce the earlier prefix hybrid; independent random child labels give the next hybrid. Only the first two labels of an expansion are retained. These identities hold for arbitrary adaptive randomized adversaries.

The complete expansion game has a uniform strict PPT certificate when its sampler does. A further security reduction must replace these repeated sampler calls with a single PRG challenge.

Main definitions

• Cslib.Crypto.GGM.expansionOracle: memoized sampled expansions and child selection.
• Cslib.Crypto.GGM.expansionGame: the complete adaptive expansion experiment.

Main results

• Cslib.Crypto.GGM.expansionGame_generated, .expansionGame_uniform: adjacent hybrid laws.
• Cslib.Crypto.GGM.isPPTOn_expansionGame: strict PPT for the entire captured-input game.

References

• O. Goldreich, S. Goldwasser, S. Micali, How to Construct Random Functions, Section 3.3, the simulation used in the proof of Theorem 3.

Adapts Crypto/Computational/GGM/Expansion.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8 to the shared typed interpreter.

def Cslib.Crypto.GGM.expansionOracle (generator : List Bool → List Bool) (sample : ProbComp (List Bool)) (n depth : ℕ) (query : List Bool) : StateT Cache ProbComp (List Bool)

Cache a sampled expansion at each parent prefix and follow its selected child.

def Cslib.Crypto.GGM.expansionGame (generator : List Bool → List Bool) (sample : ProbComp (List Bool)) (adversary : OracleDistinguisher) (n depth : ℕ) : ProbComp Bool

Run the adversary using sampled, cached expansions at the selected level.

theorem Cslib.Crypto.GGM.expansionOracle_bounds (generator : List Bool → List Bool) (sample : ProbComp (List Bool)) (n depth : ℕ) (query : List Bool) (cache : Cache) (hcache : ∀ entry ∈ cache, entry.2.length ≤ 2 * n) (result : List Bool × Cache) (hresult : result ∈ (expansionOracle generator sample n depth query cache).eval.support) : (∀ entry ∈ result.2, entry.2.length ≤ 2 * n) ∧ result.1.length ≤ n ∧ (cacheEncoding result.2).length ≤ (cacheEncoding cache).length + 4 * query.length + 4 * n + 3

A cached expansion uses at most two labels of storage. The sampled word may have any length; truncation bounds the stored value and selected child even on malformed challenges.

theorem Cslib.Crypto.GGM.isPPTOn_expansionOracle {α : Type} {input : α ↪ List Bool} {generator : List Bool → List Bool} {sample : α → ProbComp (List Bool)} {width depth : α → ℕ} {query : α → List Bool} {cache : α → Cache} (hgenerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hsample : Probability.IsPPTOn input Turing.MultiTapeTM.encBits sample) (hwidth : Turing.MultiTapeTM.ComputableTidilyInPolyTime width input Turing.MultiTapeTM.encUnary) (hdepth : Turing.MultiTapeTM.ComputableTidilyInPolyTime depth input Turing.MultiTapeTM.encUnary) (hquery : Turing.MultiTapeTM.ComputableTidilyInPolyTime query input Turing.MultiTapeTM.encBits) (hcache : Turing.MultiTapeTM.ComputableTidilyInPolyTime cache input cacheEncoding) : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits cacheEncoding) fun (a : α) => expansionOracle generator (sample a) (width a) (depth a) (query a) (cache a)

Expansion handlers compose a certified sampler with ordinary cache and tree code. Every argument may depend on the caller's captured input, including the entire initial cache.

theorem Cslib.Crypto.GGM.isPPTOn_expansionGame {Caller : Type} {input : Caller ↪ List Bool} {generator : List Bool → List Bool} {sample : Caller → ProbComp (List Bool)} {width depth : Caller → ℕ} (hgenerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hsample : Probability.IsPPTOn input Turing.MultiTapeTM.encBits sample) (hwidth : Turing.MultiTapeTM.ComputableTidilyInPolyTime width input Turing.MultiTapeTM.encUnary) (hdepth : Turing.MultiTapeTM.ComputableTidilyInPolyTime depth input Turing.MultiTapeTM.encUnary) {adversary : OracleDistinguisher} (hadversary : Probability.IsOraclePPT Turing.MultiTapeTM.encBool adversary) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : Caller) => expansionGame generator (sample a) adversary (width a) (depth a)

A complete adaptive expansion game is strict PPT, uniformly in the captured parameters and sampler. The public local contracts account for the clock, replies and full cache growth.

theorem Cslib.Crypto.GGM.expansionGame_generated (generator : List Bool → List Bool) (adversary : OracleDistinguisher) (n depth : ℕ) (hdepth : depth < n) : (expansionGame generator (generator <$> BitString.sampleList n) adversary n depth).eval = (hybridGame generator adversary n depth).eval

Sampling generator expansions reproduces the earlier prefix hybrid for every adaptive randomized adversary. No security or output-width assumption on the generator is needed.

theorem Cslib.Crypto.GGM.expansionGame_uniform (generator : List Bool → List Bool) (adversary : OracleDistinguisher) (n depth : ℕ) (hdepth : depth < n) : (expansionGame generator (BitString.sampleList (2 * n)) adversary n depth).eval = (hybridGame generator adversary n (depth + 1)).eval

Uniform expansions give the next prefix hybrid: the two independent children of each parent are exactly the independent labels at the next level, under randomized adaptive queries.