Paper 2024/232

On the Security of Nova Recursive Proof System

Abstract

Nova is a new type of recursive proof system that uses folding scheme as its core building block. This brilliant idea of folding relations can significantly reduce recursion overhead. In this paper, we study some issues related to Nova's soundness proof that relies on the soundness of the folding scheme in a recursive manner. First, its proof strategy, due to its recursive nature, inevitably expands the running time of the recursive extractor polynomially for each additional recursive step. This constrains Nova's soundness model to have only logarithmically bounded recursive steps, and so the soundness proof in this limited model does not guarantee the soundness for linear rounds in the security parameter, e.g., 128 rounds for 128 bit security. On the other hand, there are no known attacks on 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 a 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 tell nothing about real-world uses 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 algebraic group model with our refinements. 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 algebraic group model, we replace this heuristics with a cryptographic hash function with special property. We view this hash function as an independent object of interest and expect it to help further understand the soundness of Nova.