The GGM prefix hybrids

At level depth, sample an independent label for each newly queried prefix of that length. Remember it for later queries with the same prefix, and evaluate the remaining suffix using the generator. Malformed queries receive the empty word, as in the PRF games.

The cache is an ordinary list. One call preserves a label-width invariant and adds at most one entry. The shared stateful interpreter certifies the entire adaptive game, including copying, sampling, replies and growing storage. This module identifies the endpoint games; adjacent-hybrid security requires a further reduction.

Main definitions

• Cslib.Crypto.GGM.frontierOracle: memoized prefix labels followed by tree evaluation.
• Cslib.Crypto.GGM.hybridGame: the complete adaptive prefix experiment.

Main results

• Cslib.Crypto.GGM.hybridGame_zero, .hybridGame_self: exact real and ideal endpoints.
• Cslib.Crypto.GGM.isPPTOn_hybridGame: uniform strict PPT for the complete experiment.

References

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

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

@[reducible, inline]

abbrev Cslib.Crypto.GGM.Cache : Type

A finite collection of queried prefixes and their sampled labels.

def Cslib.Crypto.GGM.cacheEncoding : Cache ↪ List Bool

Charge every stored prefix and label, including list and pair delimiters.

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

Answer from a cached random label at the chosen level, followed by ordinary tree evaluation.

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

The adaptive hybrid game starts with an empty prefix cache.

theorem Cslib.Crypto.GGM.hybridGame_zero (generator : List Bool → List Bool) (adversary : OracleDistinguisher) (n : ℕ) : (hybridGame generator adversary n 0).eval = (prfRealGame (eval generator) adversary n).eval

At level zero, all valid queries share one root label. Sampling that label on demand agrees with choosing the key at the start of the real PRF game, even if there are no valid queries.

theorem Cslib.Crypto.GGM.frontierOracle_self (generator : List Bool → List Bool) (n : ℕ) : frontierOracle generator n n = cachedRandomFunctionOracle n

The final level caches full query answers directly. There is no suffix left to evaluate.

theorem Cslib.Crypto.GGM.hybridGame_self (generator : List Bool → List Bool) (adversary : OracleDistinguisher) (n : ℕ) : (hybridGame generator adversary n n).eval = (prfIdealGame adversary n).eval

At the final level, the prefix hybrid is exactly the ideal PRF game.

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

Each call preserves label widths and adds at most one encoded entry. Key lengths and duplicate cache keys are unrestricted; only cached label widths are constrained.

theorem Cslib.Crypto.GGM.isPPTOn_frontierOracle {α : Type} {input : α ↪ List Bool} {generator : List Bool → List Bool} {parameter depth : α → ℕ} {query : α → List Bool} {cache : α → Cache} (hgenerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hparameter : Turing.MultiTapeTM.ComputableTidilyInPolyTime parameter 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 : α) => frontierOracle generator (parameter a) (depth a) (query a) (cache a)

Certify a prefix call written with computed parameters, query and full cache.

theorem Cslib.Crypto.GGM.isPPTOn_hybridGame {generator : List Bool → List Bool} (hgenerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) {adversary : OracleDistinguisher} (hadversary : Probability.IsOraclePPT Turing.MultiTapeTM.encBool adversary) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBool fun (pair : ℕ × ℕ) => hybridGame generator adversary pair.1 pair.2

A uniform adversary's complete adaptive prefix game is strict PPT, uniformly over the chosen level. The local invariant accounts for every reply and all added encoded storage.