papers/lp-020-quasar-consensus/sections/06-quasarcert-formal-definition.tex

\section{QuasarCert: Formal Definition and Replay Protection}

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

\subsection{QuasarCert}

\begin{definition}[QuasarCert]
\label{def:quasarcert}
A QuasarCert for block $B$ with respect to validator set
$\mathcal{V} = \{v_1, \ldots, v_n\}$, certificate subject
$m = \mathsf{cert\_subject}$ (Definition~\ref{def:subject}), and
verifying-key root $Z_\text{vk}$ is a 4-tuple
\[
\mathcal{C} \;=\; \bigl(\sigma^{\mathrm{BLS}}_{\mathrm{agg}},\;
\sigma^{\mathrm{RT}},\;
\pi_{\mathrm{ZK}},\;
h_x\bigr)
\]
where:
\begin{enumerate}[leftmargin=2em,nosep]
  \item $\sigma^{\mathrm{BLS}}_{\mathrm{agg}} \in \mathbb{G}_1$ is an
    aggregate BLS12-381 signature on $m$ from $\geq t = \lfloor 2n/3
    \rfloor + 1$ validators in $P_\text{val}$. Size: 48 bytes
    (compressed $\mathbb{G}_1$).
  \item $\sigma^{\mathrm{RT}}$ is a Corona threshold signature on $m$
    under the Q-Chain combined public key bound to $Q_\text{cer}$.
    Size: ${\sim}56$\,KB.
  \item $\pi_{\mathrm{ZK}} \in \{0,1\}^{192 \cdot 8}$ is a Groth16
    proof~\cite{groth2016} for the relation $\mathcal{R}_{\mathrm{ZK}}$
    of Section~\ref{sec:lane3}, attesting that $\geq t$ ML-DSA-65
    signatures on $m$ from validators in $P_\text{val}$ exist.
    Size: 192 bytes ($A \in \mathbb{G}_1$, $B \in \mathbb{G}_2$,
    $C \in \mathbb{G}_1$, all compressed).
  \item $h_x \in \{0,1\}^{256}$ is the public-inputs hash:
    $h_x = H_{\text{Poseidon}}\bigl(\{\mathit{pk}_i^{\mathrm{ML}}\}_{i=1}^N
    \,\|\, m\bigr)$. Size: 32 bytes.
\end{enumerate}
\end{definition}

\begin{definition}[QuasarCert Verification]
\label{def:verify-qcert}
$\mathsf{VerifyQuasarCert}(B, \mathcal{V}, \mathcal{C})$ recomputes
$m = \mathsf{cert\_subject}$ from $B$ and the seven chain roots
$\boldsymbol{\rho}$, then returns 1 iff all of:
\begin{align}
&e\bigl(G_2,\, \sigma^{\mathrm{BLS}}_{\mathrm{agg}}\bigr) \;=\;
  e\bigl(\mathit{apk}_{\mathrm{BLS}},\, H_{\mathbb{G}_1}(m)\bigr)
  \label{eq:v-bls} \\
&\mathsf{RT.Verify}\bigl(\mathit{pk}^{\mathrm{RT}},\, m,\,
  \sigma^{\mathrm{RT}}\bigr) = 1 \label{eq:v-rt} \\
&\mathsf{Groth16.Verify}\bigl(\mathit{vk}_{Z},\, h_x,\, \pi_{\mathrm{ZK}}\bigr)
  = 1 \label{eq:v-zk} \\
&h_x \;=\; H_{\text{Poseidon}}\bigl(\{\mathit{pk}_i^{\mathrm{ML}}\}_{i=1}^N
  \,\|\, m\bigr). \label{eq:v-hx}
\end{align}
$\mathit{vk}_Z$ is recovered from $Z_\text{vk}$ via Merkle path. The set
$\{\mathit{pk}_i^{\mathrm{ML}}\}$ is recovered from $P_\text{val}$.
\end{definition}

\paragraph{Component sizes.}

\begin{table}[ht]
\centering
\begin{tabular}{@{}llr@{}}
\toprule
\textbf{Component} & \textbf{Hardness Assumption} & \textbf{Size} \\
\midrule
$\sigma^{\mathrm{BLS}}_{\mathrm{agg}}$ (BLS aggregate) &
  co-CDH on BLS12-381 & 48 B \\
$\sigma^{\mathrm{RT}}$ (Corona) &
  Module-LWE / Module-SIS & ${\sim}56$ KB \\
$\pi_{\mathrm{ZK}}$ (Groth16 of ML-DSA) &
  KEA/AGM + MLWE/MSIS & 192 B \\
$h_x$ (public-inputs hash) & Hash collision resistance & 32 B \\
\midrule
\textbf{Total} & & ${\sim}56.27$ KB \\
\bottomrule
\end{tabular}
\caption{QuasarCert component sizes. The $192 + 32 = 224$ bytes for the
post-quantum identity-binding lane is independent of validator count
$N$. At $N{=}100$ validators a per-validator-ML-DSA scheme would carry
$330{,}900$ bytes for the same lane.}
\label{tab:cert-sizes}
\end{table}

\begin{remark}
In epoch mode (one Corona signature per epoch of $k$ blocks, with
per-block BLS and Z-Chain only), the amortized header overhead is
$56\,\text{KB}/k + 48\,\text{B} + 224\,\text{B}$ per block. With $k =
1000$ this is ${\sim}328$ bytes/block.
\end{remark}

\paragraph{Cryptographic assumptions.}
The QuasarCert relies on:
\begin{enumerate}[leftmargin=2em,nosep]
  \item co-CDH on BLS12-381~\cite{boneh2001short}: given
    $(g, g^a, h) \in \mathbb{G}_2^2 \times \mathbb{G}_1$, computing
    $h^a$ is hard.
  \item Module-LWE~\cite{regev2005}: distinguishing
    $(\mathbf{A}, \mathbf{As}+\mathbf{e})$ from $(\mathbf{A},
    \mathbf{u})$ is hard (Corona basis).
  \item MLWE / MSIS~\cite{nist-pqc}: ML-DSA-65 (FIPS 204) is EUF-CMA
    secure under Module-LWE and Module-SIS at NIST Level 3.
  \item Knowledge of Exponent + Algebraic Group Model~\cite{groth2016}:
    Groth16 is knowledge-sound.
\end{enumerate}

\subsection{Replay Protection via Subject Binding}
\label{sec:replay}

\begin{theorem}[Cross-Chain / Cross-Epoch Replay Impossibility]
\label{thm:replay-impossible}
Let $\mathcal{C} = (\sigma^{\mathrm{BLS}}_{\mathrm{agg}},
\sigma^{\mathrm{RT}}, \pi_{\mathrm{ZK}}, h_x)$ be a QuasarCert that was
produced for block $B$ on chain $c$ at epoch $e$, round $r$, mode $\mu$,
under chain roots $\boldsymbol{\rho}$ with parent context
$(h_{\text{parent}}, s, x, g, b)$. For any block $B'$ on chain
$c' \neq c$, or epoch $e' \neq e$, or round $r' \neq r$, or mode
$\mu' \neq \mu$, or any tuple $(\boldsymbol{\rho}', h'_{\text{parent}},
s', x', g', b') \neq (\boldsymbol{\rho}, h_{\text{parent}}, s, x, g, b)$,
$\mathsf{VerifyQuasarCert}(B', \mathcal{V}', \mathcal{C})$ returns 0
except with probability $\mathsf{negl}(\lambda)$.
\end{theorem}

\begin{proof}
The verifier of Definition~\ref{def:verify-qcert} recomputes
$m = \mathsf{cert\_subject}$ from the inputs of $B'$ before checking
each lane. Suppose $B'$ differs from $B$ in any of $c, e, r, \mu,
\boldsymbol{\rho}, h_{\text{parent}}, s, x, g, b$. Then the input to
$\mathsf{keccak}_{256}$ in Definition~\ref{def:subject} differs by at
least one byte. By collision resistance of $\mathsf{keccak}_{256}$, the
new $m'$ equals the original $m$ with probability $\leq 2^{-256}$.

If $m' \neq m$:
\begin{itemize}[leftmargin=2em,nosep]
\item Equation~\eqref{eq:v-bls} fails because BLS verification is
      message-binding under co-CDH (EUF-CMA).
\item Equation~\eqref{eq:v-rt} fails because Corona is EUF-CMA under
      MLWE.
\item Equation~\eqref{eq:v-hx} fails because $h_x$ depends on $m$ via
      Poseidon hashing, and Poseidon is collision-resistant.
\item Equation~\eqref{eq:v-zk} fails because $\pi_{\mathrm{ZK}}$ was
      proved against the original $h_x$, not the new one; an adversary
      adapting $\pi_{\mathrm{ZK}}$ to the new $h_x$ contradicts Groth16
      knowledge-soundness in the AGM.
\end{itemize}
Each lane independently rejects, so verification returns 0.

The forgery probability is bounded by the union of
$\mathsf{negl}(\lambda)$ from co-CDH, MLWE, Poseidon collision
resistance, and Groth16 knowledge-soundness:
$\mathsf{Pr}[\text{replay accepted}] \leq \mathsf{negl}(\lambda)$.
\end{proof}

\begin{corollary}[Replay across Modes]
A QuasarCert produced in mode $\mu = 3$ (Quantum) cannot be presented
as a valid mode-$\mu' \neq 3$ certificate, because $\mu$ enters the
subject and the lower-mode verifiers would still recompute the original
mode-3 subject.
\end{corollary}

\begin{remark}
This binding is \emph{structural}: it does not rely on any nonce
registry, sequence number, or external replay cache. The certificate
itself encodes its full context, so the verifier can decide replay
locally and statelessly.
\end{remark}

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