% !TEX root = main.tex
% !TEX spellcheck = en-US
\section{Introduction}
Zero-knowledge proof systems that allow a prover to convince a verifier of a statement without revealing anything beyond the truth of the statement have broad application in cryptography and theory of computation~\cite{FOCS:GolMicWig86,STOC:Fortnow87,C:BGGHKMR88}.
When restricted to computationally sound proofs, called \emph{argument systems}, proof length can be shorter than the length of the witness~\cite{brassard1988minimum}. 
Zero-knowledge Succinct Non-interactive ARguments of Knowledge (zkSNARKs) are zero-knowledge argument systems that additionally have a succinctness property -- small proof sizes and fast verification. 
Since their introduction in~\cite{FOCS:Micali94}, zk-SNARKs have been a powerful and versatile design tool for secure cryptographic protocols. They became particularly relevant for blockchain applications that demand short proofs and fast verification, such as privacy-preserving cryptocurrencies~\cite{SP:BCGGMT14} in Zcash and scalable and private smart contracts in Ethereum\footnote{\url{https://z.cash/} and \url{https://ethereum.org} respectively}.

%The work of~\cite{EC:GGPR13} proposed a preprocessing zk-SNARK for general NP statements phrased in the language of Quadratic Span Programs (QSP) and Quadratic Arithmetic Programs (QAP) for Boolean and arithmetic circuits respectively. This built on previous works of~\cite{IKO07,AC:Groth10a,TCC:Lipmaa12} and led to several works~\cite{TCC:BCIOP13,SP:PHGR13,C:BCGTV13,AC:Lipmaa13,USENIX:BCTV14,EC:Groth16} with very short proof sizes and fast verification.

While research on zkSNARKs has seen rapid progress~\cite{EC:GGPR13,AC:Groth10a,TCC:Lipmaa12,TCC:BCIOP13,SP:PHGR13,C:BCGTV13,AC:Lipmaa13,USENIX:BCTV14,EC:Groth16} with many works proposing significant improvements in efficiency of different parameters like proof size, verifier efficiency, and complexity of the public setup, less attention has been paid to non-malleable zkSNARKs and succinct signatures of knowledge, (SoK) also known as SNARKY signatures~\cite{C:GroMal17,EPRINT:BKSV20}. A signature of knowledge~\cite{C:CamSta97,C:ChaLys06} uses an instance of an NP-language as the public verification key. Instead of signing using a secret key, which typically would be related to the public key via a discrete logarithm or some other hard relation~\cite{AC:DHLW10}, SoK signing requires knowledge of the NP-witness. Chase and Lysyanskaya~\cite{C:ChaLys06} require signatures of knowledge to be simulatable to assure protection against signing key/witness extraction. Given a trapdoor associated with the public setup, signatures can be simulated without the witness. Furthermore, to model strong existential unforgeability of signatures, even when given an oracle for obtaining signatures on different instances, an attacker must not be able to produce new signatures. Chase and Lysyanskaya model this via the notion of simulation-extractability which guarantees extraction of the witness even in the presence of simulated signatures.
Moreover,  Groth and Maller \cite{C:GroMal17} showed how to construct 
SoK from zkSNARK schemes that have simulation-extractability. 
Therefore, our focus can be moved from SoK to the main building block,  zkSNARK schemes,  for which we have many new efficient constructions in the recent literature. 
 

\paragraph{Relevance of simulation extractability.}

Most zkSNARKs are shown to only satisfy a standard knowledge soundness property. Intuitively, this guarantees that
a prover that creates a valid proof knew a valid witness. However, deployments of zkSNARKs in real-world applications unless they are carefully designed to have application specific malleability protection, e.g.~\cite{SP:BCGGMT14}, require a stronger property -- \textit{simulation-extractability} (SE) that as discussed above corresponds more closely to existential unforgeability of signatures.
In practice, an adversary against the zkSNARK has access to proofs provided by other parties using the same
zkSNARK.  The definition of knowledge soundness ignores the ability of an adversary to see other valid proofs that may occur in real-world applications.  For instance, in applications of
zkSNARKs in privacy-preserving blockchains, proofs are posted on the chain for all
blockchain-participants to see.
%Therefore, it is necessary for a zero-knowledge proof system to be \emph{non-malleable}, that is, resilient against adversaries that additionally get to see proofs generated by different parties before trying to forge.
%Therefore, it is necessary for a zero-knowledge proof system to be \emph{simulation-extractable}, that is, resilient against adversaries that additionally get to see proofs generated by different parties before trying to forge.
%This captures the more general scenario where an adversary against the zkSNARK has access to proofs provided by other parties as it is in applications of zkSNARKs in privacy-preserving blockchains, where proofs are posted on the chain for all
%participants in the network to verify.

\paragraph{Fiat-Shamir based zkSNARKs.}
Most modern zkSNARK constructions follow a modular blueprint that involves the design of an information theoretic interactive protocol, e.g. an Interactive Oracle Proof (IOP), that is then compiled via cryptographic tools to obtain an interactive argument system.  This is then turned into a zkSNARK using the hash-based Fiat-Shamir transform. By additionally hashing the message, the Fiat-Shamir transform is also a popular technique for constructing signatures. While well understood for 3-round sigma protocols and justifiable in the random oracle
model (ROM)~\cite{CCS:BelRog93}, is only a heuristic that should be used with
care since there are counterexamples that it is
unsound~\cite{FOCS:GolKal03}.

%The Fiat--Shamir (FS) transform takes a public-coin interactive protocol and makes it interactive by hashing the current protocol transcript to compute the verifier's public coins.
%
%The FS transform is a popular design tool for constructing
%zkSNARKs. In the updatable universal SRS setting, works like \sonic{}~\cite{CCS:MBKM19}
%\plonk{}~\cite{EPRINT:GabWilCio19}, and \marlin~\cite{EC:CHMMVW20} are designed
%and proven secure as multi-round interactive protocols. Security is then only
%\emph{conjectured} for their non-interactive variants by employing the FS
%transform.

In particular, several schemes such as
$\sonic$~in \cite{CCS:MBKM19}, $\plonk$~\cite{EPRINT:GabWilCio19}, $\textsf{Marlin}$~\cite{EC:CHMMVW20} 
follow this approach where the information theoretic object is a multi-round algebraic variant of IOP, and the cryptographic primitive in the compiler is a polynomial commitment scheme (PC) that requires a trusted setup. To date, this blueprint lacks an analysis in the ROM in terms of simulation extractability.


\paragraph{Updatable setup zkSNARKs}
One of the downsides of efficient zkSNARKs like~\cite{AC:Groth10a,TCC:Lipmaa12,EC:GGPR13,SP:PHGR13,AC:Lipmaa13,AC:DFGK14,EC:Groth16} is that they rely on a \textit{trusted setup}, where there is a structured reference string (SRS) that is assumed to be generated by a trusted party. In practice, however, this assumption is not well founded; if the party that generates the SRS is not honest, then they can produce proofs of false statement. That is, if the trusted setup assumption does not hold, knowledge soundness breaks down.
Groth et al~\cite{C:GKMMM18} propose a setting to tackle this challenge which allows parties -- provers and verifiers -- to \emph{update} the SRS, that is, take a current SRS and contribute to it randomness in a verifiable way to obtain a new SRS. The guarantee in this \textit{updatable setting} is that knowledge soundness holds as long as one of the parties who updates the SRS is honest. The SRS is also \emph{universal}, in that it does not depend on the relation to be proved but only on an upper bound in the size of the statements.
Although inefficient, as the SRS length is quadratic in the size of the statement,~\cite{C:GKMMM18} set a new
paradigm of universal updatable setting for designing zkSNARKs.

The first universal zkSNARK with updatable and linear size SRS was
$\sonic$ proposed by Maller et al.~in \cite{CCS:MBKM19}. Subsequently, Gabizon et
al.~designed $\plonk$~\cite{EPRINT:GabWilCio19} which currently is the
most efficient updatable universal zkSNARK. Independently, Chiesa et
al.~\cite{EC:CHMMVW20} proposed $\textsf{Marlin}$ with comparable efficiency to
$\plonk$.

\paragraph{The challenge of SE in the updatable setting.}

The notion of simulation-extractability for zkSNARKs which is well motivated in practice has not been studied in this updatable setting.

Consider the following scenario: We assume a rushing adversary that starts off with a sequence of malicious updates by colluding parties resulting in a subverted reference string $\srs$. By combining their trapdoor contributions and employing the simulation algorithm, these parties can easily compute a proof $(\srs,x,\pi)$ for a statement $x$ without knowing a witness. Now, assume that at a later stage a party produces a proof $(\srs',x,\pi')$ for the same statement with respect to an updated $\srs'$ that has an honest update contribution. We would like the guarantee that this party must known a witness corresponding to $x$. The ability to ``move" the proof $\pi$ from the old SRS to a proof $\pi'$ for the new SRS without knowing a witness would clearly violates security. A natural idea is to require that honestly \emph{updated} reference strings are indistinguishable from honestly \emph{generated} reference strings. However, this is not sufficient as the rushing adversary can also rush toward the end of the SRS generation ceremony to perform the last update.
%That is, an adversary who does not knows the trapdoor for the update from $\srs$ to $\srs'$ should not be able to break SE. % as long as there was at least one honest update to $\srs$.\markulf{30/09/2021}{We currently don't achieve this strong USE notion.}


A definition of SE in the updatable setting should take these additional powers of the adversary, which are not captured by existing definitions of SE, into consideration.
While generic lifting techniques/compilers~\cite{EPRINT:KZMQCP15,CCS:AbdRamSla20} can be applied to updatable SRS SNARKs to obtain SE, not only do they inevitably incur overheads and lead to efficiency loss, we contend that the standard definition of SE does not suffice in the updatable setting.




We investigate the non-malleability properties of a class of zkSNARK protocols obtained by FS-compiling multi-round protocols in the updatable SRS setting and give a modular approach to analyse the simulation-extractability of zkSNARKs.
\subsection{Our Contributions}
\begin{itemize}
\item 
\emph{Updatable simulation extractability (USE)}. 
We propose a definition of simulation extractability in the updatable SRS setting called USE, that captures the additional power the adversary gets by being able to update the SRS.% and seeing proofs with respect to different SRSs.\michals{28.09}{Now the adversary sees additional proofs wrt to the final SRS.}
    
  \item \emph{General theorem for USE of FS-compiled interactive protocols.} We
        then show that a class of interactive proofs of knowledge that when
        the Fiat--Shamir transform is applied to them are \changedm{trapdoor-less simulatable}, have a
        unique response property in the updatable setting, and satisfy a
        property we define called forking special soundness \emph{are USE
        out-of-the box} in the random oracle model. Informally, our notion of forking
        special soundness is a variant of special soundness where the
        transcripts provided to the extractor are obtained through interaction
        with an honest verifier, and the extraction guarantee is computational
        instead of unconditional. Our extractor only needs oracle access to the
        adversary, it does not depend on the adversary’s code, nor does it rely on
        knowledge assumptions.
    
\item
\emph{USE for concrete zkSNARKs.}
We then prove that the most efficient updatable SRS SNARKS -- Plonk/Sonic/Marlin -- satisfy the notions necessary to invoke our general theorem. We thus show that these zkSNARKs are updatable simulation extractable.
Only in this step we rely on the algebraic group model (AGM).

\item
  \emph{SNARKY signatures in the updatable setting.} Our results validate the folklore that the Fiat--Shamir transform is a natural means for constructing signatures of knowledge. This gives rise to the first SoK in the updatable setting and confirms that a much larger class of zkSNARKs, beside \cite{C:GroMal17}, can be lifted to SoK.
	
%\item
%We make several technical contributions along the way. Our generalized forking lemma is of independent interest.
\end{itemize}



\subsection{Technical Overview}
%unique response, forking special soundness. general theorem without additional assumptions. to apply the theorem to concrete schemes like plonk, we show it satisfies unique response, forking soundness, in AGM.

From a high level, the proof of our general theorem for updatable simulation
extractability is along the lines of the simulation extractability proof for
FS-compiled sigma protocol from~\cite{INDOCRYPT:FKMV12}. However, our theorem
introduces new notions that are more general to allow us to consider proof
systems that are richer than sigma protocols and support an updatable setup. We
discuss some of the technical challenges below.

\plonk{}, \sonic{}, and \marlin{} were originally presented as interactive
proofs of knowledge that are made non-interactive by the Fiat--Shamir transform.
In the following, we denote the underlying interactive protocols by $\plonkprot$
(for $\plonk$), $\sonicprot$ (for $\sonic$), and $\marlinprot$ (for \marlin) and
the resulting non-interactive proof systems by $\plonkprotfs$, $\sonicprotfs$,
$\marlinprotfs$ respectively.

\oursubsub{Forking special soundness in the updatable setting.}
Following~\cite{INDOCRYPT:FKMV12}, one would have to show that for the protocols
we consider, a witness can be extracted from sufficiently many valid transcripts
with a common prefix. The standard definition of special soundness for sigma
protocols requires extraction of a witness from any two transcripts with the
same first message. However, most zkSNARK protocols do not satisfy this notion.
We put forth a notion analogous to special soundness, that is more general and
applicable to a wider class of protocols. Namely, protocols can have more than three
rounds and can rely on an updatable SRS. $\plonkprot$, $\sonicprot$, and
$\marlinprot$ have more than 3 rounds and the number of transcripts required for extraction is more
than two. Concretely, $(3 \noofc + 1)$ -- where $\noofc$ is the number of
constraints in the proven circuit -- for Plonk, $(\multconstr + \linconstr + 1)$
-- where $\multconstr$ and $\linconstr$ are the numbers of multiplicative and
linear constraints -- for Sonic, and $(\multconstr + 3)$ -- where $\multconstr$
is the number of multiplicative constraints -- for Marlin. Hence, we do not have
a pair of transcripts, but a \emph{tree of transcripts}.

In protocols that rely on SRS that come with a trapdoor, an adversary in
possession of the trapdoor can produce multiple valid proof transcripts without
knowing the witness and potentially for false statements. This is true even in
the updatable setting, where there exists a trapdoor for any updated SRS. Recall
that the standard special soundness definition requires witness extraction from
\emph{any} tree of acceptable transcripts that share a common root. This means
that there are no such trees for false statements. We define a different,
forking lemma-related, version of soundness that we call forking special soundness.
Forking special soundness guarantees that it is possible to extract a witness from all
(but negligibly many) trees of accepting transcripts produced by probabilistic
polynomial time (PPT) adversaries, given that the trees are generated as
interactions between a (possibly malicious) prover and an honest verifier. That
is, if extraction from such a tree fails, then we break an underlying
computational assumption. Moreover, this should hold even against adversaries
that contribute in the SRS generation.

\oursubsub{Unique response property in the updatable setting.}  Another property required to
show USE is the unique response property~\cite{C:Fischlin05} which says that for $3$-messages
sigma protocols, all but the first message sent by the prover are deterministic (intuitively,
the prover can only employ fresh randomness in the first message of the protocol). We cannot
use this definition as is since the protocols we consider have other rounds with randomized prover
messages. In Plonk, both the first and the second prover's messages are
randomized. Although Sonic prover is deterministic after it picks its first message, the
protocol has more than $3$ rounds. The same holds for Marlin. We propose a generalisation of
the definition which states that a protocol is $\ur{i}$ if the prover is deterministic starting
from its $(i + 1)$-th message. For our proof it is sufficient that this property is met by
Plonk for $i = 2$. Since Sonic and Marlin provers are deterministic from the second message on,
they are $\ur{1}$.


\oursubsub{Trapdoor-less simulatable protocols.}  In order to invoke our main theorem on
(Fiat--Shamir transformed) Plonk, Sonic and Marlin to conclude USE, we also need to show
that simulators in these protocols produces proofs without relying on the knowledge of
trapdoor. More precisely for our reduction, we need simulators that rely only on reordering the
messages and picking suitable verifier challenges, without knowing the SRS trapdoor.  That is,
any PPT party should be able to produce a simulated proof on its own in a trapdoor-less
way. Note that this property does not necessary break soundness of the protocol as the
simulator is required only to produce a transcript and is not involved in a real conversation
with a real verifier. We show simulators for $\plonkprotfs$, $\sonicprotfs$, and
$\marlinprotfs$ that rely only on the programmability of the RO, where programmability is only
needed from some round $i$ onwards. This property can be understood as a generalization of honest-verifier zero-knowledge for Fiat--Shamir transformed prove systems with an SRS.

\oursubsub{Generalising the general forking lemma.}  Consider an interactive $3$-message
special-sound protocol $\ps$ and its non-interactive version $\ps_\fs$ obtained by the
Fiat--Shamir transform. The general forking lemma provides an instrumental lower bound for the
probability of extracting a witness from an adversary who provides two proofs for the same
statement that share the first message. Since $\plonkprot$, $\sonicprot$, and $\marlinprot$ have more than $3$
messages and are not special-sound, the forking lemma of Bellare and Neven~\cite{CCS:BelNev06},
cannot be used directly. We propose a generalization that covers multi-message protocols where
witness extraction requires more than two transcripts.  Unfortunately, we also observe
that the security gap grows with the number of transcripts and the probability that the
extractor succeeds diminishes; the security loss, albeit big, is polynomial.

Most modern zkSNARKs~\cite{SP:BBBPWM18,CCS:MBKM19} heavily
rely on the Fiat--Shamir transform and thus potentially the forking lemma.
%First, an interactive
%protocol is proposed and its security and forking special soundness analysed.\markulf{30.09}{Unclear here whether forking special soundness is for the interactive of the non-interactive protocol.} Second,
%one uses an argument that the Fiat--Shamir transform can be used to get a
%protocol that is non-interactive and shares the same security properties.
We thus see our generalized forking lemma as contributing to a critical assessment of
this approach. The analysis of the interactive protocol is not enough and one
has to consider the security loss implied by the Fiat-Shamir transform for the target security notion.
%Thus one has to either rely on our generalisation of the forking
%lemma or disclose a transformation that does not suffer this loss.
We note that the security loss of our generalized forking lemma may also apply
when knowledge soundness is proven. This is, e.g., the case for the original
$\sonic$ paper, whose security proof relies on so-called witness-extended
emulation. The authors of $\plonk$ and recent work on
$\sonic$~\cite{cryptoeprint:2020:1351} work around this problem by proving
knowledge soundness directly in the AGM.



\subsection{Related Work}
 

\ourpar{Simulation extractability.}
There are many results on simulation extractability for
non-interactive zero-knowledge proofs (NIZKs). First, Groth \cite{AC:Groth07}
noticed that a (black-box) SE NIZK is
universally-composable (UC)~\cite{EPRINT:Canetti00}. Then Dodis et al.~\cite{AC:DHLW10} introduced a
notion of (black-box) \emph{true simulation extractability} and showed that no
NIZK can be UC-secure if it does not have this property. 

In the context of zkSNARKs, the first
SE zkSNARK was proposed by Groth and Maller~\cite{C:GroMal17} and a SE
zkSNARK for QAP was designed by Lipmaa~\cite{EPRINT:Lipmaa19a}.
Kosba's et
al.~\cite{EPRINT:KZMQCP15} give a general transformation from a NIZK to a
black-box SE NIZK. Although their transformation works for zkSNARKs as well,
succinctness of the proof system is not preserved by the transformation.
Recently, Abdolmaleki et al.~\cite{CCS:AbdRamSla20} showed another transformation that
obtains non-black-box simulation extractability but also preserves
succinctness of the argument. 
The zkSNARK of~\cite{EC:Groth16} has been shown to be SE by introducing minor modifications to the construction and making
stronger assumptions \cite{EPRINT:BowGab18,EPRINT:AtaBag19}. Recently,~\cite{EPRINT:BKSV20} showed that the
original Groth's proof system from~\cite{EC:Groth16} is weakly SE and
randomizable. None of these results are for zkSNARKs in the updatable SRS setting or for zkSNARKs obtained via the Fiat--Shamir transformation.

\ourpar{Forking lemma generalizations.}
There are several task specific variants, e.g.,~\cite{INDOCRYPT:HerSae03,CCS:BagCheJar08,AC:BelDaiLi19}, of the general forking lemma~\cite{JC:PoiSte00,CCS:BelNev06} for analyzing the forking behavior of random-oracle based executions.
In~\cite{EC:BCCGP16}, Bootle et al.~proposed a novel inner-product argument whose
security relies on, so-called, witness-extended emulation. To show that
property, the authors proposed a new version of the forking lemma that gives a
lower bound on the probability that a tree finding algorithm is able to produce a
tree of acceptable transcripts by rewinding a conversation between a
(potentially malicious) prover and verifier.

Although the result in that paper is dubbed a ``forking lemma'' it
differs from forking lemmas known from e.g.~\cite{JC:PoiSte00,CCS:BelNev06}.
First of all, the forking lemmas in these papers analyse the probability of building
a tree of acceptable transcripts for Fiat--Shamir based non-interactive proof
systems, while the protocol presented by Bootle et al.~is intended to work for
interactive proof systems.

Importantly, it is not obvious how the result of Bootle et al.~can be used to
show security of non-interactive protocols as it relies on interactive provers
whose proving strategies are more limited than proving strategies of
non-interactive provers. For example, if a challenge given by the verifier does not
suit an interactive prover, it can only try to finish a proof with that challenge or
abort. On the other hand, a non-interactive prover has far wider scope of
possible actions--when the protocol is non-interactive the prover may
adapt its strategy based on the random oracle outputs. 
This is reminiscent of \emph{state restoration} security~\cite{TCC:BenChiSpo16,EPRINT:Holmgren19} which is also about the security loss incurred by the Fiat--Shamir transformation albeit when proving knowledge soundness from witness extended emulation.

Here, we directly capture the state restoration capability of the prover in the forking lemma instead of defining an interactive game where the prover can rewind the verifier to an earlier state as is done in~\cite{C:GhoTes21}. 
The work of~\cite{C:GhoTes21} further shows that state restoration security gives tight security guarantees for the
non-interactive versions of Bulletproof~\cite{SP:BBBPWM18} and \sonic. 
Our work differs from~\cite{C:GhoTes21} in the following ways. First, they
focus on showing security of concrete proof systems, while we show
a general theorem about the security of a wide class of protocols. 
Second, they only consider knowledge soundness, while we focus on the stronger notion of simulation extractability. Third, the proof of~\cite{C:GhoTes21} is in the AGM which allows for online extraction, whereas we aim to reduce our reliance on the AGM. In particular, our extractor and main theorem do not rely on the AGM and we thus tackle technical challenges arising from extraction by rewinding.
However, arguably due to the design of Plonk, Sonic, and Marlin, we show that these concrete protocols satisfy the preconditions of our main theorem in the AGM.

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End:
