Paper 2024/232 Original: eprint.iacr.org/2024/232 ↗

On the Security of Nova Recursive Proof System: Limitations of and Alternatives to Bounded-Depth Analysis

Abstract

Standard definitions of Knowledge Soundness for Incrementally Verifiable Computation (IVC) are formulated to accommodate rewinding based analysis, effectively limiting their security guarantees to bounded (logarithmic) recursion depths. We demonstrate that this limitation is critical: we construct an artificial IVC scheme that satisfies this standard, bounded-depth definition but becomes efficiently forgeable when the recursion extends to a polynomial scale. This finding exposes a theoretical gap in Nova (CRYPTO '22), leaving its intended unbounded usage theoretically unfounded. We bridge this gap by establishing the Polynomial-depth Knowledge Soundness of Nova. Our analysis framework is anchored in the Extended Algebraic Group Model (EAGM). Specifically, the EAGM extends the algebraic requirement to intermediate values involved in algebraic operations, allowing the extractor to reconstruct the recursive witness directly from the representations of these internal operations to bypass the exponential overhead of rewinding. Leveraging this extraction capability, we crucially depart from standard Fiat-Shamir analyses that rely on the Random Oracle Model (ROM) to guarantee that the extracted witnesses satisfy the intended relations. While the ROM is theoretically uninstantiable and necessitates heuristic realizations, we instead enforce the validity of the extracted witnesses using the General Zero-Testing (GZT) property. This property replaces the random oracle with a targeted requirement offering a plausible pathway to standard-model instantiation, providing the first rigorous security foundation for recursive proof systems in unbounded use cases.