Paper 2024/232

On the Security of Nova Recursive Proof System

Abstract

Nova is a new type of recursive proof system that uses a folding scheme as its core building block. This brilliant idea of folding relations can significantly reduce the recursion overhead. In this paper, we study some issues related to Nova’s soundness proof, which relies on the soundness of the folding scheme in a recursive manner. First, due to its recursive nature, the proof strategy inevitably causes the running time of the recursive extractor to expand polynomially for each additional recursive step. This constrains Nova's soundness model to only logarithmically bounded recursive steps. Consequently, the soundness proof in this limited model does not guarantee soundness for a linear number of rounds in the security parameter, such as 128 rounds for 128-bit security. On the other hand, there are no known attacks on the arbitrary depth recursion of Nova, leaving a gap between theoretical security guarantees and real-world attacks. We aim to bridge this gap in two opposite directions. In the negative direction, we present a recursive proof system that is unforgeable in a log-round model but forgeable if used in linear rounds. This shows that the soundness proof in the log-round model might not be applicable to real-world applications that require linearly long rounds. In a positive direction, we show that when Nova uses a specific group-based folding scheme, its knowledge soundness over polynomial rounds can be proven in the Extended Algebraic Group Model (EAGM), which is our novel computational model that lies between Algebraic Group Model (AGM) and the Generic Group Model (GGM). To the best of our knowledge, this is the first result to show Nova's polynomial rounds soundness. Second, the folding scheme is converted non-interactively via the Fiat-Shamir transformation and then arithmetized into R1CS. Therefore, the soundness of Nova using the non-interactive folding scheme essentially relies on the heuristic random oracle instantiation in the standard model. In our new soundness proof for Nova in the EAGM, we replace this heuristic with a new computational assumption for a cryptographic hash function, called the General Zero-Testing assumption. We treat this hash assumption as an independent subject of interest and expect it to contribute to a deeper understanding of Nova's soundness.

Note: (10/03/2024) Modifying the overall description, with a particular focus on revising sections related to the algebraic group model(AGM) and its modifications. (12/14/2024) Modify the definition of AGM variant(extended AGM) and revise security proofs following the definition.