papers/lux-quasar-composition/sections/05-composition.tex

\section{Composition Theorems}
\label{sec:composition}

This section states and proves the central security claim of
QuasarCert: forging a profile-$\mathcal{P}$ cert is at least as hard
as the hardest leg in $\mathcal{L}(\mathcal{P})$.

\subsection{Adversary model}

We consider a non-uniform polynomial-time adversary $\mathcal{A}$
against the conjunctive cert verifier. Let $\mathsf{Corrupt}$ be the
subset of $\mathcal{V}_e$ that $\mathcal{A}$ controls; let
$f = |\mathsf{Corrupt}|/|\mathcal{V}_e|$. We require $f < 1/3$
(Byzantine threshold), so $|\mathsf{Honest}| = n - |\mathsf{Corrupt}|
\geq 2n/3$ and $\tau = \lfloor 2n/3 \rfloor + 1 \leq |\mathsf{Honest}|$.

$\mathcal{A}$ is given:
\begin{itemize}[leftmargin=2em,nosep]
\item All primitive public keys: $\mathit{pk}_i^{\mathrm{BLS}}$,
      $\mathit{pk}^{\mathrm{Puls}}$, $\mathit{pk}^{\mathrm{Cor}}$,
      $\mathit{pk}^{\mathrm{Mag}}$, $\{\mathit{pk}_i^{\mathrm{ML}}\}_i$.
\item Signing oracles for the corrupt set: for each $v_i \in \mathsf{Corrupt}$,
      $\mathcal{A}$ may invoke $\mathsf{BLS.Sign}(\mathit{sk}_i^{\mathrm{BLS}},
      \cdot)$, the Pulsar threshold signing protocol with
      $\mathit{sk}_i^{\mathrm{Puls}}$, etc.
\item The Z-Chain verifying key $\mathit{vk}_Z$ and the Groth16 trusted
      setup transcript (i.e., $\mathcal{A}$ knows $\mathit{vk}_Z$ in
      full).
\item Random oracle access to all hash functions, programmable in the
      proof.
\end{itemize}

$\mathcal{A}$ wins the soundness game if it outputs
$(B^{\star}, \mathcal{C}^{\star})$ such that
$\textsf{VerifyQuasarCert}(B^{\star}, \mathcal{V}_{e^{\star}},
\mathcal{C}^{\star}, \mathcal{P}) = 1$ and the block $B^{\star}$ was
not endorsed by a stake-weighted honest quorum on round digest
$\mu^{\star}$ derived from $B^{\star}$ and $\mathcal{V}_{e^{\star}}$.

We consider two adversary variants:
\begin{description}[leftmargin=2em,nosep]
\item[$\mathcal{A}_C$ --- classical PPT.] Standard probabilistic
      polynomial-time non-uniform Turing machine. Access to classical
      random oracles.
\item[$\mathcal{A}_Q$ --- quantum PPT.] Polynomial-time on a quantum
      Turing machine; can run Shor's algorithm on classical discrete
      logarithms; has access to QROM \cite{bellare1993}; subject to
      Grover speedup against unstructured search.
\end{description}

\subsection{Main composition theorem}

\begin{theorem}[QuasarCert conjunctive soundness]
\label{thm:composition}
Let $\mathcal{P}$ be a profile with leg set $\mathcal{L}(\mathcal{P})$.
Under the hardness assumptions of Section~\ref{sec:prelim}, for any
non-uniform PPT adversary $\mathcal{A}$ in either variant
$\mathcal{A}_C$ or $\mathcal{A}_Q$,
\[
\mathsf{Adv}^{\mathrm{forge}}_{\mathcal{A}}\bigl(\mathcal{P}\bigr)
\;\leq\;
\min_{\ell \in \mathcal{L}(\mathcal{P})} \epsilon_\ell\bigl(\mathcal{A}\bigr),
\]
where $\epsilon_\ell(\mathcal{A})$ is $\mathcal{A}$'s advantage against
the standalone unforgeability game of the primitive in leg $\ell$.
\end{theorem}

\begin{proof}
Fix a profile $\mathcal{P}$ and an adversary $\mathcal{A}$ that
produces a winning $(B^{\star}, \mathcal{C}^{\star})$. By
Definition~\ref{def:verify}, every leg $\ell \in \mathcal{L}(\mathcal{P})$
of $\mathcal{C}^{\star}$ verifies under the primitive-specific verifier
on round digest $\mu^{\star}$.

We exhibit, for each $\ell \in \mathcal{L}(\mathcal{P})$, a reduction
$\mathcal{B}_\ell$ that uses $\mathcal{A}$ to break the standalone
unforgeability game of the primitive at leg $\ell$ with advantage
$\geq \mathsf{Adv}^{\mathrm{forge}}_{\mathcal{A}}(\mathcal{P})$.

\paragraph{BLS leg ($\ell = \mathrm{BLS}$).} $\mathcal{B}_{\mathrm{BLS}}$
plays $\mathcal{A}$ in the QuasarCert game while embedding the
challenge $\mathit{pk}^{\star}$ from the BLS EUF-CMA challenger into
one slot of $\{\mathit{pk}_i^{\mathrm{BLS}}\}$. $\mathcal{B}_{\mathrm{BLS}}$
simulates all signing oracles for the corrupt set using
$\mathcal{B}$'s own access to the BLS signing oracle for the embedded
key. When $\mathcal{A}$ outputs $\mathcal{C}^{\star}$, $\mathcal{B}$
extracts $\sigma^{\mathrm{BLS}}_{\mathrm{agg}}$, computes
$\sigma^{\star}$ by subtracting the contributions of non-target keys
(using the BLS aggregate-verification structure), and returns
$\sigma^{\star}$ on $\mu^{\star}$ as the BLS forgery. By the
EUF-CMA security of BLS-PoP \cite{boneh2001short}, $\mathcal{A}$'s
forgery succeeds with probability $\leq \epsilon_{\mathrm{BLS}}^{\mathrm{co-CDH}}$.

\paragraph{Pulsar leg ($\ell = \mathrm{Puls}$).} $\mathcal{B}_{\mathrm{Puls}}$
embeds the ML-DSA-65 challenge public key $\mathit{pk}^{\star}$ as
the joint Pulsar group public key $\mathit{pk}^{\mathrm{Puls}}$.
$\mathcal{B}$ simulates Pulsar threshold-signing rounds for honest
parties by sampling secret shares for them and invoking the FIPS 204
ML-DSA-65 challenger's signing oracle on $\mathit{pk}^{\star}$ for
the joint signing message; the byte-equivalence property of Pulsar
(any threshold output is byte-identical to the single-party FIPS 204
output, by construction) ensures the simulation is perfect. When
$\mathcal{A}$ outputs $\mathcal{C}^{\star}$, $\mathcal{B}$ extracts
$\sigma^{\mathrm{Puls}}$ and returns it on $\mu^{\star}$ as the
ML-DSA-65 forgery. By EUF-CMA of FIPS 204 ML-DSA-65 under MLWE/MSIS
\cite{fips204,dilithium}, the forgery succeeds with probability
$\leq \epsilon_{\mathrm{Puls}}^{\mathrm{MLWE/MSIS}}$.

\paragraph{Corona leg ($\ell = \mathrm{Cor}$).} Identical structure to
the Pulsar reduction, but with Corona's M-LWE-based two-round threshold
\cite{ringtail,corona}. $\mathcal{B}_{\mathrm{Cor}}$ embeds
the Corona challenge into $\mathit{pk}^{\mathrm{Cor}}$ and simulates
Round-1 commitments and Round-2 responses using the rejection-sampling
oracle. By SUF-CMA of Corona under M-LWE/MSIS, the forgery probability
is $\leq \epsilon_{\mathrm{Cor}}^{\mathrm{MLWE}}$.

\paragraph{Magnetar leg ($\ell = \mathrm{Mag}$).} $\mathcal{B}_{\mathrm{Mag}}$
embeds the SLH-DSA challenge public key as $\mathit{pk}^{\mathrm{Mag}}$.
Because Magnetar v0.1 is reveal-and-aggregate (the joint master seed
is reconstructed in the aggregator's memory, then a single FIPS 205
\texttt{SLHDSA.SignDeterministic} call is made), the simulation
reduces to invoking the FIPS 205 challenger's signing oracle on
$\mathit{pk}^{\star}$. By EUF-CMA of SLH-DSA under SHA-3 / SHAKE
preimage and target-collision resistance \cite{fips205,sphincs}, the
forgery probability is $\leq \epsilon_{\mathrm{Mag}}^{\mathrm{SHA3-OW}}$.

\paragraph{Z-Chain leg ($\ell = \mathrm{ZK}$).} $\mathcal{B}_{\mathrm{ZK}}$
embeds the BLS12-381 discrete-log challenge into $\mathit{vk}_Z$ via
the standard Groth16 trapdoor reduction \cite{groth2016}. Because
$\pi^{\mathrm{ZK}}$ is knowledge-sound in the AGM, an extractor can
extract the witness (the per-validator ML-DSA signatures) from
$\mathcal{A}$'s proof; the witness contains $\geq \tau$ ML-DSA-65
forgeries (by Byzantine-quorum honesty) which can be returned as an
ML-DSA challenger forgery. The forgery probability is bounded by
$\epsilon_{\mathrm{ZK}}^{\mathrm{KEA}} + \epsilon_{\mathrm{MLDSA}}$.

\paragraph{Conjunction.} Because the verification predicate is the
conjunction over $\ell \in \mathcal{L}(\mathcal{P})$, $\mathcal{A}$'s
winning cert $\mathcal{C}^{\star}$ contains a valid forgery at every
populated leg. Each reduction $\mathcal{B}_\ell$ uses $\mathcal{C}^{\star}$
to win the standalone $\ell$-game with the same probability as
$\mathcal{A}$. Therefore
\[
\mathsf{Adv}^{\mathrm{forge}}_{\mathcal{A}}(\mathcal{P})
\;\leq\;
\min_{\ell \in \mathcal{L}(\mathcal{P})} \epsilon_\ell(\mathcal{A}),
\]
because the $\min$ is over a set of upper bounds.
\end{proof}

\subsection{Hardness diversification}

\begin{corollary}[Hardness diversification]
\label{cor:diversification}
For any profile $\mathcal{P}$ with $\mathrm{Puls} \in \mathcal{L}(\mathcal{P})$,
\[
\mathsf{Adv}^{\mathrm{forge}}_{\mathcal{A}_Q}(\mathcal{P})
\;\leq\;
\epsilon_{\mathrm{Puls}}^{\mathrm{MLWE/MSIS}}(\mathcal{A}_Q).
\]
Even if $\mathcal{A}_Q$ runs Shor and breaks the BLS and Groth16 legs
in polynomial time, forging the cert still requires forging the
Pulsar leg.
\end{corollary}

\begin{proof}
Direct from Theorem~\ref{thm:composition}: the upper bound is the
minimum over populated legs. The classical legs (BLS, Z-Chain) have
$\epsilon = O(1)$ under $\mathcal{A}_Q$ (i.e., trivially breakable);
the PQ legs have $\epsilon = \mathsf{negl}(\lambda)$. The minimum is
the PQ leg, in particular the Pulsar leg (since $\mathrm{Puls} \in
\mathcal{L}(\mathcal{P})$ on every profile).
\end{proof}

\begin{corollary}[Cross-family diversification under Polaris]
\label{cor:polaris}
For $\mathcal{P} = \texttt{Polaris}$,
\[
\mathsf{Adv}^{\mathrm{forge}}_{\mathcal{A}}(\texttt{Polaris})
\;\leq\;
\min\bigl(\epsilon_{\mathrm{Puls}}^{\mathrm{MLWE}}, \epsilon_{\mathrm{Cor}}^{\mathrm{MLWE}},
\epsilon_{\mathrm{Mag}}^{\mathrm{SHA3-OW}}\bigr).
\]
A cryptanalytic break against the entire algebraic-lattice family
(Module-LWE, which both Pulsar and Corona rest on) still leaves the
Magnetar / SHA-3 leg standing.
\end{corollary}

\begin{proof}
Direct from Theorem~\ref{thm:composition}. The three populated PQ
legs invoke two independent hardness families: Module-LWE
\cite{fips204,dilithium,regev2009,mlwe,ringtail} --- carried by both
Pulsar (FIPS-204 parameters) and Corona (Ringtail-derived
parameters), distinct parameter sets and codebases within the same
family --- and SHA-3 preimage / target-collision \cite{fips205,
sphincs}. A parameter- or implementation-localized break of one
Module-LWE leg need not transfer to the other, but the family-disjoint
guarantee is supplied by Magnetar: structural attacks against
lattice constructions have not transferred to symmetric / hash-based
constructions \cite{albrechtestimator,bdgl2016}. The minimum over
the three legs is the upper bound.
\end{proof}

\subsection{Why this is not weaker than the OR composition}

A common confusion in PQ cert design is whether the legs should be
OR-composed (``valid if any leg verifies'') or AND-composed (``valid
only if all populated legs verify''). The OR composition is
\emph{weaker}: forging the cert requires forging only the weakest
leg. The AND composition (conjunctive) is what we use: forging
requires forging \emph{all} populated legs.

The accompanying analysis in
\texttt{lux/proofs/pq-finality-no-bls.tex}~\cite{pqfinalitynobls}
spells this out for the BLS+PQ composition:

\begin{itemize}[leftmargin=2em,nosep]
\item Under AND composition: $\mathsf{Adv}^{\mathrm{forge}} \leq
      \min(\epsilon_{\mathrm{BLS}}, \epsilon_{\mathrm{PQ}})$. A quantum
      adversary still must forge the PQ leg.
\item Under OR composition: $\mathsf{Adv}^{\mathrm{forge}} \leq
      \min(\epsilon_{\mathrm{BLS}}, \epsilon_{\mathrm{PQ}})$? No ---
      \emph{the bound is wrong}. Under OR, the cert verifies as soon
      as one leg does, so the adversary need only forge the
      \emph{easier} leg, which under quantum attack is BLS
      ($\epsilon_{\mathrm{BLS}} = O(1)$). PQ security is reduced to
      zero.
\end{itemize}

QuasarCert uses the AND composition: a cert with the Pulsar profile
verifies iff the BLS leg verifies \emph{and} the Pulsar leg verifies
\emph{and} the Z-Chain leg verifies. This is what gives the
conjunctive hardness diversification of Theorem~\ref{thm:composition}.

\subsection{Subject-binding soundness}

\begin{theorem}[Subject-binding soundness]
\label{thm:subject-binding}
Suppose $\mathcal{C}$ is a valid QuasarCert for block $B$ at chain $c$,
epoch $e$, round $r$ under profile $\mathcal{P}$. Then $\mathcal{C}$
is not a valid cert for any $(c', e', r', B')$ with $(c, e, r, B)
\neq (c', e', r', B')$, except with negligible probability.
\end{theorem}

\begin{proof}
Theorem~\ref{thm:replay} establishes this for the BLS / Pulsar /
Corona / Magnetar legs (each leg is bound to a unique $\mu$). The
Z-Chain leg is bound to $h_x = H_{\mathsf{Poseidon}}(\{\mathit{pk}_i^{\mathrm{ML}}\}
\,\|\, \mu)$; collision resistance of Poseidon \cite{poseidon} ensures
a Z-Chain proof for $\mu$ does not verify against $\mu' \neq \mu$.
The profile-match clause (Definition~\ref{def:verify} clause 1) is
deterministic in the cert byte string, and is independent of the
block being verified.
\end{proof}

\begin{remark}[Static vs adaptive corruption]
The proofs above are stated under static corruption: the corrupt set
$\mathsf{Corrupt}$ is fixed before $\mathcal{A}$ begins the soundness
game. Adaptive corruption is handled via secure-erasure or
programmable-RO hybrids \cite{fischlin2005} with at most an
$O(n \cdot Q_H)$ multiplicative loss, where $Q_H$ is the random-oracle
query count. The Lux production deployment uses Go-side memory
zeroing of all per-signature randomness (and HSM-backed signing on
M-Chain custody deployments) to satisfy the erasure precondition;
this is documented in the per-primitive deployment runbooks
\cite{pulsar,corona,magnetar}.
\end{remark}

\begin{remark}[Aggregator-TCB in v0.1 primitives]
Pulsar v0.1 and Magnetar v0.1 share a common aggregator-as-TCB caveat:
the threshold-combine step is performed by a single aggregator that
holds enough material to construct the final signature. A malicious
aggregator can fail to produce a signature (a liveness fault) but
cannot produce a forgery, because the aggregator's material is
derived solely from honest parties' contributions: forging a
signature requires forging at the underlying primitive level, not
just compromising the aggregator. The reductions above hold even
when the aggregator is adversarial. The Tier B status of Magnetar
v0.1 (and the documented gating of the Polaris profile on Tier A
audit) reflects that this caveat has not yet been audited
end-to-end \cite{magnetar}.
\end{remark}