papers/lp-020-quasar-consensus/sections/07-security-analysis.tex

\section{Security Analysis}

\label{sec:security}
%% ============================================================================

We state seven theorems. Full proofs are machine-checked in Lean~4
(\texttt{Quasar.lean}, \texttt{BFT.lean}, \texttt{BLS.lean},
\texttt{Corona.lean}, \texttt{MLDSA.lean},
\texttt{Groth16.lean}) and protocol-level network attacks are verified in
Tamarin (\texttt{QuasarConsensus.spthy}). The companion proof
sketch~\cite{qcert-proof} contains full circuit analysis (App.~B), the
adaptive corruption argument (App.~C), trusted-setup analysis (App.~D),
and concrete-quantum security tightness (App.~E).

\subsection{Safety}

\begin{theorem}[Safety]
\label{thm:safety}
If fewer than $f+1$ validators are Byzantine ($f < n/3$), then no two
conflicting blocks $B_h$ and $B_h'$ at the same height $h$ can both
obtain valid QuasarCerts.
\end{theorem}

\begin{proof}[Proof sketch]
A QuasarCert requires an aggregate BLS signature from a quorum
$Q^{\mathrm{BLS}}_h$ with $|Q^{\mathrm{BLS}}_h| \geq 2f+1$. Suppose
both $B_h$ and $B_h'$ have valid certificates. Then
\[
|Q^{\mathrm{BLS}}_h \cap Q^{\mathrm{BLS}}_{h'}| \;\geq\;
2(2f+1) - n \;=\; f + 2 \;\geq\; 1
\]
where $n \leq 3f+1$. The intersection contains at least $f+1$ validators,
of which at least one is correct. A correct validator never signs two
conflicting subjects at the same height (the certificate subject binds
the parent block hash and the height). Contradiction.

The same intersection argument applies independently to the Corona
quorum (threshold $t = 2f+1$ contributors required by
$\mathsf{qchain\_ceremony\_root}$) and to the Groth16 lane (the rollup
proves $\geq t$ valid ML-DSA-65 signatures from validators in
$P_\text{val}$). Each lane independently prevents conflicting
certificates.
\end{proof}

\subsection{Liveness}

\begin{theorem}[Liveness]
\label{thm:liveness}
After GST, if the leader for height $h$ is correct, then a valid
QuasarCert for some block at height $h$ is produced within bounded time
$3\Delta + T_{\mathrm{sign}}$ where $T_{\mathrm{sign}}$ is the maximum
signing latency across the three lanes (BLS sign,
Corona two rounds, ML-DSA sign + Z-Chain prover).
\end{theorem}

\begin{proof}[Proof sketch]
After GST, a correct leader's proposal reaches all correct validators
within $\Delta$. Wave converges in finite rounds (since
$\theta_{\max} < 1$ and $\beta$ is finite). At least $2f+1$ correct
validators lock their preference and enter Ray. Each correct validator
produces a BLS signature (non-interactive), an ML-DSA-65 signature
(non-interactive), and contributes to Corona Round~1 and Round~2
(interactive, $2\Delta$). The Z-Chain prover is non-blocking on
network-delivery and bounded by $T_{\mathrm{ZK}}$ ($\leq$15\,ms GPU
batched). Total: proposal delivery ($\Delta$) + Wave + Corona rounds
($2\Delta$) + Z-Chain proof ($T_{\mathrm{ZK}}$) + finalization message
($\Delta$). The dominant term is $3\Delta + T_{\mathrm{sign}}$.
\end{proof}

\subsection{QuasarCert Unforgeability}

\begin{theorem}[QuasarCert Unforgeability]
\label{thm:unforgeability}
Forging a QuasarCert requires simultaneously breaking: (i) co-CDH on
BLS12-381, (ii) Module-LWE for Corona, (iii) MLWE/MSIS for ML-DSA,
\emph{and} (iv) Groth16 knowledge-soundness in the AGM. The probability
of forgery is bounded by:
\[
\mathsf{Pr}[\mathrm{Forge}_{\mathrm{Quantum}}] \;\leq\;
\mathsf{Adv}^{\text{co-CDH}} \cdot
\mathsf{Adv}^{\text{MLWE-RT}} \cdot
\bigl(\mathsf{Adv}^{\text{MLWE/MSIS-ML}} +
       \mathsf{Adv}^{\text{KEA}}\bigr).
\]
\end{theorem}

\begin{proof}[Proof sketch]
A valid QuasarCert verifies on all three lanes (Definition~\ref{def:verify-qcert}).
An adversary without $f+1$ corrupted validators must forge at least one
signature in each lane. The three lanes rest on algebraically independent
primitives---BLS12-381 over an elliptic curve, Corona over $R_q =
\mathbb{Z}_q[X]/(X^N+1)$ with $q \approx 2^{48}$, ML-DSA over $R_q$ with
$q = 8380417$ and disjoint module dimensions, and Groth16 over the same
pairing as BLS but distinct relation. By a standard hybrid argument the
adversary's joint forgery advantage is bounded by the product of the
per-lane advantages.
\end{proof}

\subsection{Single-Compromise Insufficiency}

\begin{theorem}[Single-Compromise Insufficiency]
\label{thm:single}
An adversary that breaks exactly one of the three cryptographic lanes
cannot produce a valid conflicting QuasarCert, provided $f < n/3$
honest validators remain.
\end{theorem}

\begin{proof}[Proof sketch]
Case analysis on which lane is compromised.

\textbf{Case 1: BLS broken.} The adversary forges the aggregate
$\sigma^{\mathrm{BLS}}_{\mathrm{agg}}$. It still needs (a) a valid
Corona $\sigma^{\mathrm{RT}}$ from $\geq t$ Q-Chain shares and (b) a
valid Groth16 $\pi_{\mathrm{ZK}}$ proving $\geq t$ ML-DSA signatures.
The adversary controls at most $f$ shares and $f$ ML-DSA keys; since
$f < t$, neither component can be assembled.

\textbf{Case 2: Corona broken.} Symmetric. The adversary still needs
$\geq t$ valid BLS signatures and a valid Groth16 proof.

\textbf{Case 3: ML-DSA / Groth16 broken.} Symmetric. The adversary still
needs $\geq t$ valid BLS signatures and a valid Corona signature.

In each case the two intact lanes enforce the quorum-intersection
argument of Theorem~\ref{thm:safety}.
\end{proof}

\subsection{QuasarCert Soundness}

\begin{theorem}[QuasarCert Soundness]
\label{thm:qcert-sound}
Let $\mathcal{C} = (\sigma^{\mathrm{BLS}}_{\mathrm{agg}},
\sigma^{\mathrm{RT}}, \pi_{\mathrm{ZK}}, h_x)$ be a QuasarCert that
verifies for block $B$ under validator set $\mathcal{V}$ with $|\mathcal{V}|
= n$ and threshold $t = \lfloor 2n/3 \rfloor + 1$. Under co-CDH,
Module-LWE, MLWE/MSIS, and KEA/AGM, at least $t$ validators in
$\mathcal{V}$ signed $\mathsf{cert\_subject}(B)$. Equivalently, for any
$B' \neq B$ not agreed upon by an honest quorum, no QuasarCert for $B'$
verifies except with $\mathsf{negl}(\lambda)$ probability.
\end{theorem}

\begin{proof}
We show forging any single component requires breaking its assumption.
Since all three must verify (Definition~\ref{def:verify-qcert}), forging
the full certificate requires breaking all three.

\textbf{Lane 1: $\sigma^{\mathrm{BLS}}_{\mathrm{agg}}$.}
By Boneh--Lynn--Shacham~\cite{boneh2001short}, BLS signatures are
EUF-CMA secure under co-CDH in the random oracle model. PoP prevents
the rogue-key attack. For the aggregate to verify with the expected
quorum key, the contributing set $S$ has $|S| \geq t$.

\textbf{Lane 2: $\sigma^{\mathrm{RT}}$.}
By the EUF-CMA theorem for Corona~\cite{corona}, an adversary
controlling $f < t$ parties cannot produce a valid threshold signature
on a message not signed by an honest quorum. Advantage:
$\mathsf{Adv}^{\text{EUF-CMA}}_{\text{RT}} \leq Q_H \cdot
\mathsf{Adv}^{\text{MLWE}} + Q_S / 2^{128}$.

\textbf{Lane 3: $(\pi_{\mathrm{ZK}}, h_x)$.}
Groth16 is knowledge-sound under KEA in the AGM~\cite{groth2016}: a
valid proof admits an extractor that recovers a witness, here the
$\geq t$ ML-DSA-65 signatures. Each extracted signature is valid under
$\mathit{pk}_i^{\mathrm{ML}}$, which by FIPS~204 EUF-CMA implies
validator $v_i$ produced it. The Poseidon binding
$h_x = H(\{\mathit{pk}_i^{\mathrm{ML}}\} \,\|\, m)$ ensures the extracted
signatures are over the recomputed certificate subject $m$.

\textbf{Composition.}
By a union bound on independent reductions:
\[
\mathsf{Adv}^{\mathsf{forge}} \leq
\mathsf{Adv}^{\text{co-CDH}} +
\mathsf{Adv}^{\text{MLWE-RT}} +
\mathsf{Adv}^{\text{MLWE/MSIS-ML}} +
\mathsf{Adv}^{\text{KEA}} \;=\; \mathsf{negl}(\lambda).
\]
\end{proof}

\subsection{Parallel Liveness}

\begin{theorem}[Parallel Liveness]
\label{thm:par-liveness}
If $f < n/3$ and the network is synchronous after GST with delay $\leq
\Delta$, then for every valid block $B$ proposed by an honest leader, a
valid QuasarCert is produced within
$\max\bigl(\Delta_{\mathrm{BLS}},\, \Delta_{\mathrm{RT}},\,
\Delta_{\mathrm{ZK}}\bigr) + O(\Delta)$.
An adversary must stall all three lanes simultaneously to prevent
finality.
\end{theorem}

\begin{proof}
Each lane completes independently:

\textbf{BLS path.} Each honest validator signs $\mathsf{cert\_subject}$
on receipt of $B$. The proposer collects $\geq t$ signatures within
$2\Delta$. Aggregation is non-interactive (${\sim}3$\,ms GPU).
Total: $2\Delta + O(1)$.

\textbf{Corona path.} Round 1 commitments arrive within $\Delta$;
Round 2 responses arrive within $2\Delta$ once $\geq t$ valid Round 1
messages are collected; Q-Chain combination in 7\,ms.
Total: $2\Delta + O(1)$.

\textbf{Z-Chain path.} Each honest validator signs
$\mathsf{cert\_subject}$ with ML-DSA-65 (254\,$\mu$s) and submits to
Z-Chain. Z-Chain collects honest signatures within $\Delta + O(1)$ and
runs the Groth16 prover ($\approx 2^{22.5}$ R1CS constraints; App.~B
of~\cite{qcert-proof}); 200\,ms CPU or 5--15\,ms GPU. For missing
signatures from Byzantine validators Z-Chain waits up to
$T_{\mathrm{ZK}}$ then proves the relation for the validators that did
sign.
Total: $\Delta + T_{\mathrm{ZK}} + O(1)$.

\textbf{Why all three must be stalled.} Stalling any single lane
requires preventing $> n - t \geq n/3$ validators from contributing.
With $f < n/3$ no bounded adversary can stall even one lane, much less
all three.
\end{proof}

\subsection{Post-Quantum Safety}

\begin{theorem}[Post-Quantum Safety]
\label{thm:pq-safety}
If a quantum adversary breaks BLS12-381 co-CDH (Shor on the pairing
group), QuasarCert verification restricted to the Corona and
MLDSAGroth16 lanes still guarantees soundness under Module-LWE and
MLWE/MSIS. The Groth16 lane has a pre-configured fallback to direct
verification of $\geq t$ raw ML-DSA-65 signatures.
\end{theorem}

\begin{proof}
\textbf{Corona under quantum attack.} Best known quantum attack on
Module-LWE is lattice sieving with Grover speedup, achieving
$2^{0.265\beta}$ time for BKZ blocksize $\beta$. With Corona
parameters ($N{=}256$, $q \approx 2^{48}$, module dimension 8, LWE
dimension 2048), the cost is $\geq 2^{130}$ operations
(App.~E of~\cite{qcert-proof}). $\mathcal{A}_Q$ cannot forge
$\sigma^{\mathrm{RT}}$.

\textbf{ML-DSA under quantum attack.} ML-DSA-65 is parameterized for
NIST Level~3 ($\geq$128-bit quantum security)~\cite{nist-pqc}. Best
quantum attack (Core-SVP with quantum sieving) requires $\geq 2^{128}$
operations.

\textbf{Groth16 under quantum attack.} A quantum adversary breaks KEA
on the pairing group (Shor extracts discrete logs, enabling proof
forgery). In this case Quasar 3.0 falls back to the
$\mathsf{VerifyPQ}$ predicate:
\[
\mathsf{VerifyPQ}(B, \mathcal{V}, \mathcal{C}) =
\mathsf{RT.Verify}(\cdot) \;\land\;
\mathsf{MLDSA.VerifyQuorum}(\cdot)
\]
where $\mathsf{MLDSA.VerifyQuorum}$ checks $\geq t$ raw ML-DSA-65
signatures (the proposer-side ``signal flare'' broadcasting validators'
raw signatures). This costs $t \cdot 254\,\mu$s extra CPU per block and
is acceptable in the post-CRQC fallback regime.

\textbf{Explicit reduction.} Suppose $\mathcal{A}_Q$ forges under
$\mathsf{VerifyPQ}$. Construct $\mathcal{R}$ from MLWE: embed the
challenge as either the Corona public key or as a target ML-DSA-65
public key, simulate the protocol, and extract a short vector solving
the SIS instance dual to the LWE challenge. By a standard hybrid
argument:
\[
\mathsf{Adv}^{\mathsf{VerifyPQ}}_{\mathcal{A}_Q} \;\leq\;
2 \cdot \max\bigl(\mathsf{Adv}^{\text{MLWE-RT}},\,
                  \mathsf{Adv}^{\text{MLWE/MSIS-ML}}\bigr) \;=\;
\mathsf{negl}(\lambda).
\]
\end{proof}


%% ============================================================================