papers/lp-073-pulsar/sections/05-security.tex

\section{Security}
\label{sec:security}

This section states the four production-grade security claims of Pulsar
and points to the canonical proof artefact for each. Proof bodies live
exactly once in \texttt{proofs/quasar-cert-soundness.tex}
\cite{quasarcertsoundness} and the Lean tree under
\texttt{proofs/lean/Crypto/} \cite{leancrypto}; this paper cites them
verbatim and does not duplicate the bodies.

\subsection{Security games}
\label{sec:security:games}

We adopt the standard \emph{existential unforgeability under chosen
message attack} (EUF-CMA) and \emph{strong unforgeability under chosen
message attack} (SUF-CMA) games for threshold signatures. Throughout,
$\lambda$ is the security parameter, $\mathcal{A}$ is a non-uniform
PPT adversary (classical, $\mathcal{A}_C$, or quantum, $\mathcal{A}_Q$),
$\mathcal{O}_{\mathrm{Sign}}$ is the threshold signing oracle, and
$\mathcal{O}_H$ is the random oracle (programmable in QROM hybrids,
following App.~C of \cite{quasarcertsoundness}). The full validator
set is $\mathcal{V}$ with $|\mathcal{V}| = n$, threshold $t$, and stake
distribution $\mathrm{stk}: \mathcal{V} \to \mathbb{N}$.

\begin{definition}[Threshold EUF-CMA / SUF-CMA games]
\label{def:tuf-cma}
The game $\mathsf{Game}^{\mathrm{tEUF-CMA}}_{\Pi}(\mathcal{A}, \lambda)$
proceeds as follows.
\begin{enumerate}[nosep, leftmargin=2em]
  \item \textbf{Setup.} The challenger runs $\mathsf{Gen}(1^\lambda) \to
        (\mathsf{GK}, \{\mathbf{s}_v\}_{v \in \mathcal{V}})$, where
        $\mathsf{GK} = (\mathbf{A}, \tilde{\mathbf{b}})$ is the public
        group key and $\mathbf{s}_v$ the share for $v$. $\mathsf{GK}$
        is given to $\mathcal{A}$.
  \item \textbf{Corruption.} $\mathcal{A}$ commits to a corrupt set
        $F \subseteq \mathcal{V}$ with stake $\mathrm{stk}(F) < t$ and
        receives $\{\mathbf{s}_v : v \in F\}$. (Static model. Adaptive
        is treated by App.~C of \cite{quasarcertsoundness} via
        Fischlin's transform with $O(n \cdot Q_H)$ loss.)
  \item \textbf{Queries.} $\mathcal{A}$ may invoke
        $\mathcal{O}_{\mathrm{Sign}}(\mu_i)$ for messages
        $\mu_1, \ldots, \mu_{Q_S}$ chosen adaptively; each query returns
        a Pulsar signature $\sigma_i$ produced by an honest threshold
        protocol over a quorum the challenger selects.
        $\mathcal{A}$ may invoke $\mathcal{O}_H$ up to $Q_H$ times.
  \item \textbf{Forgery.} $\mathcal{A}$ outputs
        $(\mu^\star, \sigma^\star)$.
        $\mathcal{A}$ \emph{wins} the EUF-CMA game iff
        $\mathsf{Verify}(\mathsf{GK}, \mu^\star, \sigma^\star) = 1$ and
        $\mu^\star \notin \{\mu_1, \ldots, \mu_{Q_S}\}$.
        $\mathcal{A}$ wins the SUF-CMA game iff
        $\mathsf{Verify}(\mathsf{GK}, \mu^\star, \sigma^\star) = 1$ and
        $(\mu^\star, \sigma^\star) \notin \{(\mu_i, \sigma_i)\}_{i=1}^{Q_S}$.
\end{enumerate}
The advantages are
\[
  \mathsf{Adv}^{\mathrm{tEUF-CMA}}_{\Pi, \mathcal{A}}(\lambda)
  = \Pr\bigl[\mathcal{A} \text{ wins EUF-CMA}\bigr],
  \qquad
  \mathsf{Adv}^{\mathrm{tSUF-CMA}}_{\Pi, \mathcal{A}}(\lambda)
  = \Pr\bigl[\mathcal{A} \text{ wins SUF-CMA}\bigr].
\]
$\Pi$ is $(\mathcal{Q}, \epsilon)$-tEUF-CMA secure if
$\mathsf{Adv}^{\mathrm{tEUF-CMA}}_{\Pi, \mathcal{A}} \leq \epsilon$ for
every $\mathcal{A}$ running within budget $\mathcal{Q} = (Q_S, Q_H, T)$.
\end{definition}

For the lifecycle layer we additionally consider the
\emph{key-era unforgeability} game, in which $\mathcal{A}$ may also
invoke $\mathcal{O}_{\mathrm{Reshare}}, \mathcal{O}_{\mathrm{Refresh}},
\mathcal{O}_{\mathrm{Reanchor}}$ subject to corruption-budget bounds at
each transition.

\begin{definition}[Key-era unforgeability]
\label{def:keyera-uf}
The game $\mathsf{Game}^{\mathrm{KE-UF}}_{\Pi}(\mathcal{A}, \lambda)$
extends Definition~\ref{def:tuf-cma} with three lifecycle oracles. At
each transition, $\mathcal{A}$ commits to the corrupt subset of the
post-state validator set with $\mathrm{stk}(F) < t$. $\mathcal{A}$
\emph{wins} iff it produces a forgery $(\mu^\star, \sigma^\star)$ on
\emph{any} live key era's GroupKey for an unsigned $\mu^\star$.
\end{definition}

\subsection{Theorem 5.1: Pulsar SUF-CMA under MLWE / MSIS}
\label{sec:security:thm51}

\begin{theorem}[Pulsar threshold SUF-CMA, MAC-bound Round 1]
\label{thm:pulsar-suf-cma}
Let $\Pi_{\mathrm{Pulsar}}$ be the LP-073 protocol of
\S\ref{sec:protocol} at the parameter set of \S\ref{sec:parameters}.
Under the Module-LWE assumption
$\mathsf{MLWE}_{q, m_{\mathrm{pk}}, n_{\mathrm{vec}}, \chi_E}$ on
$R_q = \mathbb{Z}_q[X]/(X^{256}+1)$ with $q \approx 2^{48}$ and
secret/error distribution $\chi_E = \mathcal{D}(\sigma_E)$,
$\sigma_E \approx 6.108$, and the Module-SIS assumption
$\mathsf{MSIS}_{q, m_{\mathrm{pk}}, \beta}$ at norm bound
$\beta = B \approx 2^{48.61}$, in the random-oracle model on
$\mathsf{BLAKE3}$ and the PRF assumption on the BLAKE3-keyed MAC,
\[
  \mathsf{Adv}^{\mathrm{tSUF-CMA}}_{\Pi_{\mathrm{Pulsar}}, \mathcal{A}}(\lambda)
  \;\leq\;
  \epsilon_{\mathrm{MLWE}}(\lambda)
  + \epsilon_{\mathrm{MSIS}}(\lambda)
  + \frac{Q_H + Q_S}{2^{256}}
  + Q_S \cdot 2^{-128}
  + \frac{Q_M}{2^{256}},
\]
where $Q_H, Q_S, Q_M$ are random-oracle, signing, and MAC queries
respectively. The first two terms are negligible at the LP-073 \S2
parameters (App.~E of \cite{quasarcertsoundness}); the third bounds
challenge collisions on the 256-bit transcript hash; the fourth bounds
the rejection-sampling slack at $\eta_\varepsilon = 2.650104$ over
$Q_S$ signing transcripts at the $80$-bit statistical-distance margin
\cite{dilithium}; the fifth bounds MAC forgery on Round 1 broadcasts.
\end{theorem}

\begin{proof}[Proof reference]
The two-round lattice-threshold kernel SUF-CMA reduction is the standard
Fiat--Shamir-with-aborts argument, instantiated at the parameter set of
\S\ref{sec:parameters}. The Pulsar wrapper adds (i) the Round 1 MAC layer
and (ii) the lifecycle compatibility (Lemmas~10--13 of
\cite{quasarcertsoundness}, ``Pulsar Key-Era Lifecycle Lemmas''
section). The Lean specification
\texttt{Crypto.Pulsar.pulsar\_pq\_unforgeability} in
\texttt{proofs/lean/Crypto/Pulsar/} \cite{leancrypto} encodes the
unforgeability axiom against quantum adversaries with $\mathrm{compromised}
< t$. The detailed bound derivation, including App.~E parameter analysis
and the BDGL/Grover cost equations, is in \cite{quasarcertsoundness}
Theorem~5 (classical soundness, lattice-threshold lane case) and App.~E.
\end{proof}

\paragraph{Byte-equal ML-DSA mode and its proof posture.} The claims of
this section are stated for the two-round lattice-threshold \emph{kernel}
of \S\ref{sec:protocol} (the $(c, z, \Delta)$ output, shared with
Corona). Pulsar's \emph{byte-equal ML-DSA} mode
(\S\ref{sec:protocol:bcc}) additionally proves
Theorem~\ref{thm:bcc-byte-equal} (BCC/CEF byte-equality): a boundary-clear
threshold signature verifies byte-for-byte under unmodified FIPS~204
$\mathsf{ML\text{-}DSA.Verify}$ at ML-DSA-65 / ML-DSA-87. That mode is
\emph{review-ready, not production-certified}: the byte-equality is
demonstrated under \texttt{cloudflare/circl} and \texttt{pq-crystals} and
the boundary-clearance / hint-recovery correspondence is machine-checked
in Lean, but the tight small-norm lattice range proofs and the in-MPC
$\mathsf{HighBits}$ evaluation are fail-closed pending external review
(\S\ref{sec:protocol:bcc:status}).

\paragraph{Round 1 MAC subgame.} A network attacker that observes
Round 1 broadcasts cannot replace any party's $D_i$ with a malicious
$D_i'$ unless it forges the corresponding $\textsc{MAC}_{i \to j}$. The
MAC is BLAKE3 \cite{blake3} truncated to 256 bits over a payload that
includes the symmetric pairwise key $\textsc{MACKeys}[i][j]$. Under the
PRF assumption on BLAKE3, the attacker's MAC-forgery advantage is
$Q_M / 2^{256}$ where $Q_M$ is the number of MAC queries observed; at
$Q_M \leq 2^{30}$ over an epoch lifetime, this is below $2^{-220}$.
The attack class of \cite{drijvers2019} (sub-exponential forgery on
unauthenticated concurrent commitment broadcast) is closed by the
combination of MAC authentication and per-party PRNG seeding from
$\textsc{BLAKE3}(\textsc{WriteTo}(\mathrm{sk}_i))$
(\texttt{sign.go:103}).

\paragraph{Full-rank subgame.} \textsc{SignRound2Preprocess} performs a
per-coefficient full-rank check on $D_\Sigma$ after dropping column 0
(\texttt{sign.go:348}). This rules out residual malicious commitments
that pass the MAC layer (e.g., $D_i' = D_i + V$ where $V$ has
rank-deficient slot $k$) but admit a re-opening attack. The check costs
$\varphi$ Gaussian eliminations on $m_{\mathrm{pk}} \times \bar D = 8
\times 48$ matrices over $\mathbb{F}_q$.

\paragraph{$L_2$ acceptance.} The verifier accepts iff the squared
$L_2$ norm of $(\Delta, z)$ over signed coefficients in $(-q/2, q/2]$
is at most $B^2 = 184\,960\,669\,042\,442\,604\,975\,662\,780\,477$.
The slack reservation $\eta_\varepsilon \cdot \sigma_*$ in $r^*$
ensures honest signers pass with probability $> 1 - 2^{-128}$ at the
canonical parameters; a forger cannot inflate $\Delta$ to compensate
for an arbitrary $c$ without exceeding the bound, by SIS hardness on
$[\mathbf{A}\,|\,\mathbf{I}]$ at norm $\beta = B$.

\subsection{Theorem 5.2: Activation-certificate circuit-breaker}
\label{sec:security:thm52}

\begin{theorem}[Activation-certificate soundness]
\label{thm:pulsar-activation}
Let $\Pi$ be a pre-activation Pulsar state at $(\eta, g)$ and $\Pi'$
the proposed post-activation state at $(\eta, g+1)$. Define
$\mathsf{VerifyActivation}(\Pi, \Pi', \sigma) = 1$ iff $\sigma$ is a
valid Pulsar threshold signature on the activation message
$\mathsf{ActivationMsg}_{\eta, g+1}$ of \S\ref{sec:lifecycle:activation}
that verifies under the \emph{unchanged} GroupKey
$\mathsf{GK}(\Pi) = (\mathbf{A}, \tilde{\mathbf{b}})$. Then under
MLWE/MSIS at the LP-073 \S2 parameters,
\[
  \Pr\bigl[
    \mathsf{VerifyActivation}(\Pi, \Pi', \sigma) = 1
    \;\wedge\;
    \Pi' \text{ does not Lagrange-recombine to } \mathbf{s}
  \bigr]
  \;\leq\;
  \mathsf{Adv}^{\mathrm{tSUF-CMA}}_{\Pi_{\mathrm{Pulsar}}, \mathcal{A}}(\lambda)
  \;=\; \mathsf{negl}(\lambda).
\]
Equivalently: \textsf{VerifyActivation} accepts iff the new committee
shares can sign under the unchanged GroupKey, except with negligible
probability.
\end{theorem}

\begin{proof}[Proof reference]
This is Theorem~14 of \cite{quasarcertsoundness} (``Activation-
certificate soundness''). The proof reduces acceptance under the
unchanged GroupKey to a Pulsar SUF-CMA challenge: a malformed
$\Pi'$ that nonetheless produces an accepting $\sigma$ would yield a
fresh MLWE/MSIS instance breaking Theorem~\ref{thm:pulsar-suf-cma}
above. The forward direction follows from the Lagrange-recombination
identity~(see Theorem~5.3 below).
\end{proof}

\subsection{Theorem 5.3: Resharing preserves master secret}
\label{sec:security:thm53}

\begin{theorem}[Lagrange-recombination identity]
\label{thm:pulsar-reshare}
Let $f(x) \in R_q[X]$ be the old-set sharing polynomial of degree
$t_{\mathrm{old}} - 1$ with $f(0) = \mathbf{s}$ and
$f(\alpha_v) = \mathbf{s}_v$ for $v \in V$. After
$\mathrm{Reshare}(V', t')$ with qualified subset
$Q \subseteq V$, $|Q| \geq t_{\mathrm{old}}$, where each $i \in Q$
samples $g_i(x)$ of degree $t' - 1$ with $g_i(0) = \mathbf{s}_i$, the
new sharing polynomial
\[
  G(x) = \sum_{i \in Q} \lambda^Q_i(0) \cdot g_i(x)
\]
satisfies
\begin{align}
  G(0)
  \;&=\; \sum_{i \in Q} \lambda^Q_i(0) \cdot g_i(0)
  \;=\; \sum_{i \in Q} \lambda^Q_i(0) \cdot \mathbf{s}_i
  \nonumber \\
  \;&=\; \sum_{i \in Q} \lambda^Q_i(0) \cdot f(\alpha_i)
  \;=\; f(0)
  \;=\; \mathbf{s},
  \label{eq:pulsar-lagrange}
\end{align}
where the penultimate equality is the standard Lagrange interpolation
identity over $R_q$. Consequently,
$(\mathbf{A}, \mathbf{s}, \mathbf{e})$ is preserved across Reshare,
$\tilde{\mathbf{b}} = \lfloor \mathbf{A} \mathbf{s} +
\mathbf{e} \rceil_\xi$ is byte-preserved, and
$\mathsf{GKH}(\Pi) = \mathsf{GKH}(\Pi')$.
\end{theorem}

\begin{proof}[Proof reference]
This is Lemma~12 of \cite{quasarcertsoundness} (``GroupKey
byte-identity across Refresh and Reshare''), proved via
equation~\eqref{eq:pulsar-lagrange}. The Lean encoding is
\texttt{Crypto.Threshold.Reshare.reshare\_preserves\_public\_key} in
\texttt{proofs/lean/Crypto/Threshold/Reshare.lean} \cite{leancrypto},
which derives $\mathsf{pubkey\_from\_shares}(\mathsf{newShares}, t')
= \mathsf{pubkey}(\mathsf{key})$ from the underlying axiom
\texttt{reshare\_same\_secret}.
\end{proof}

For Refresh (HJKY97), an analogous identity applies with $z_i(x)$ a
zero-polynomial of degree $t-1$ \cite{hjky97}: the constant term
contributes nothing to $G(0)$, so $\mathbf{s}, \mathbf{e},
\tilde{\mathbf{b}}$ are byte-preserved. Verifiability of each
contribution under lattice Pedersen commits is per
Wong--Wang--Wing \cite{wongwangwing02} (LP-073
\S\ref{sec:lifecycle:dkg}); the binding/hiding properties hold under
MSIS on $[\mathbf{A}\,|\,\mathbf{B}]$ and MLWE on $\mathbf{B}$
respectively.

\subsection{Theorem 5.4: Lineage unforgeability}
\label{sec:security:thm54}

\begin{theorem}[KeyEraID and Generation lineage unforgeability]
\label{thm:pulsar-lineage}
Let $\mathcal{C} = (\eta_i, g_i, r_i)_{i=0}^{N}$ be the on-chain
lineage record across an arbitrary execution of Pulsar lifecycle
transitions. Under the activation-cert soundness theorem
(Theorem~\ref{thm:pulsar-activation} above) and the collision
resistance of $\mathsf{BLAKE3}$, no PPT adversary $\mathcal{A}$ can
produce
$\mathcal{C}^\star \neq \mathcal{C}$ that the chain accepts as a valid
lineage on the same epoch sequence, except with probability
$\mathsf{Adv}^{\mathrm{tSUF-CMA}} + Q_H / 2^{256}$.
\end{theorem}

\begin{proof}[Proof reference]
The lifecycle record is enforced by chain-state transitions that each
require a valid activation cert (Theorem~\ref{thm:pulsar-activation}
above). By Lemmas~10--13 of \cite{quasarcertsoundness} (Generation
monotonicity, KeyEraID stability, GroupKey byte-identity, Rollback-
lineage forward reconstruction), the triple $(\eta, g, r)$ uniquely
determines the lineage chain up to permutation of forward-then-rolled-
back branches; these are unambiguously labelled by $r > 0$. Forging a
different valid $\mathcal{C}^\star$ requires either (a)~forging an
activation cert (reduces to Theorem~\ref{thm:pulsar-activation}) or
(b)~finding a BLAKE3 collision on $\mathsf{ActivationMsg}$
($Q_H / 2^{256}$). The detailed reverse-walk construction that
recovers the canonical forward path appears in the proof of
Lemma~13 of \cite{quasarcertsoundness}.
\end{proof}

\subsection{Concrete parameter analysis}
\label{sec:security:concrete}

The classical and post-quantum cost analysis for the Pulsar parameter
set lives in App.~E of \cite{quasarcertsoundness} and is summarised
here for the bound substitutions in Theorems~5.1--5.4.

\paragraph{Lattice dimension.} Module-LWE underlying Pulsar has
$d = m_{\mathrm{pk}} \cdot \varphi = 8 \cdot 256 = 2048$ over
$\mathbb{Z}_q$ with $\log_2 q \approx 48$.

\paragraph{Classical cost (BDGL primal sieving).} For
$d = 2048, q \approx 2^{48}, \sigma_E \approx 6.108$, the optimal BKZ
block size is $\beta \approx 430$. Under the Becker--Ducas--Gama--
Laarhoven exponent $0.292$ \cite{bdgl2016},
\[
  T_{\mathrm{classical}}
  \;=\; 2^{0.292\beta + c_0}
  \;\approx\; 2^{0.292 \cdot 430 + 16.4}
  \;=\; 2^{142}.
\]

\paragraph{Quantum cost (Grover-amplified sieving).} Under the
Laarhoven--BDGL exponent $0.265$ for Grover-amplified
sieving \cite{laarhoven2015,bdgl2016},
\[
  T_{\mathrm{quantum}}
  \;=\; 2^{0.265 \beta + c_0}
  \;\approx\; 2^{0.265 \cdot 430 + 16.4}
  \;=\; 2^{130.35}.
\]
This is the substitution in Theorem~\ref{thm:pulsar-suf-cma}'s
$\epsilon_{\mathrm{MLWE}}, \epsilon_{\mathrm{MSIS}}$ at
$\lambda = 128$: the bound saturates the NIST Cat.~3 quantum target
with $\geq 2^{130}$ headroom.

\paragraph{MSIS bound.} The verifier accepts at $L_2$-norm bound
$\beta = B \approx 2^{48.61}$. SIS at $(\mathbf{A}, \beta)$ on the
$2048$-dimensional module is hard at the same BKZ block size; the
honest forger must find $(\Delta, z)$ within $\beta$ that satisfies the
$Az - bc$ identity, which by linear-algebra reduces to a
short-vector search on a coset of the SIS lattice. The cost
matches the MLWE estimate above to within $O(1)$ in the exponent.

\paragraph{Substitution into Theorem~5.1.} At $\lambda = 128$ and
$Q_S, Q_H \leq 2^{60}$ (a generous epoch-lifetime bound):
\begin{align*}
  \mathsf{Adv}^{\mathrm{tSUF-CMA}}_{\Pi_{\mathrm{Pulsar}}, \mathcal{A}_C}
  &\;\leq\; 2^{-142} + 2^{-142} + 2^{-196} + 2^{-68} + 2^{-196}
  \;\leq\; 2^{-67}, \\
  \mathsf{Adv}^{\mathrm{tSUF-CMA}}_{\Pi_{\mathrm{Pulsar}}, \mathcal{A}_Q}
  &\;\leq\; 2^{-130} + 2^{-130} + 2^{-196} + 2^{-68} + 2^{-196}
  \;\leq\; 2^{-67}.
\end{align*}
The dominant term is the rejection-sampling slack
$Q_S \cdot 2^{-128}$; the lattice term is far below the budget. To
shrink the slack one shrinks $Q_S$ by limiting per-epoch signing or
by adopting the tighter slack of $2^{-256}$ at the cost of one extra
$\sigma_E$-deviation in the Gaussian sampler. Lux production accepts
$2^{-67}$ as the operative bound at the LP-073 parameters; raising the
slack tier is tracked as a live parameter knob.

\subsection{Side-channel posture}
\label{sec:security:sidechannel}

Lattigo's \texttt{MRed} and \texttt{MRedLazy} \cite{lattigov7} are
constant-time on a 64-bit \texttt{bits.Mul64} substrate (Go and C++ on
x86/ARM 64). The Ziggurat \cite{ziggurat} and ternary samplers contain
rejection-sampling loops whose iteration count depends on the random
bytes consumed; the PRNG seed is independent of the secret in every
call site except $\textsc{PRNGKey}(\mathrm{sk}_i)$
(\texttt{primitives/hash.go:19}), where the BLAKE3 hashing is
constant-time and the resulting $k_{\mathrm{sk}}$ is used only as a
seed for the per-session PRNG. The dependence between secret-derived
seed and observable PRNG output is bounded by BLAKE3 collision
resistance (PRF-secure for $Q_H \leq 2^{128}$).

\subsection{Nonce-uniqueness invariant}
\label{sec:security:nonce}

The per-session PRNG is seeded deterministically from
$\textsc{BLAKE3}(\textsc{WriteTo}(\mathrm{sk}_i))$, which means the
same $(\mathrm{sk}_i, \mathit{sid}, \mu)$ triple produces the same
$R_i$ sequence. This is safe iff $\mathit{sid}$ is unique per signing
session. In Lux Quasar deployment (LP-020 \cite{lp020}), $\mathit{sid}$
is the (chain id, block height) pair, whose monotonicity is enforced by
P-Chain consensus; this provides session-id uniqueness as a chain
invariant rather than a runtime obligation. Under
Theorem~\ref{thm:pulsar-suf-cma} a session-id collision would
manifest as a transcript-hash collision and reduce to BLAKE3
collision-resistance, but the chain rules out the collision before the
PRNG is reseeded.

\subsection{Identifiable abort posture}
\label{sec:security:identabort}

Pulsar identifies misbehaviour at two layers:
\begin{itemize}[nosep]
  \item \textbf{Round 1 MAC layer.} A failed MAC verification names
        the sender (the verifier can identify which $i$'s broadcast
        was tampered with). This is per-party identifiable abort by
        construction.
  \item \textbf{Round 2 share layer.} \textsc{Verify} can run per-share:
        $z_j$ verifies independently against
        $(D_j, \lambda_j, c, \tilde b)$ via the same $A z_j - b \cdot
        \lambda_j c$ identity restricted to share $j$. The first
        failing index identifies the corrupt $z_j$ and is recorded as
        slashing-evidence material on chain. The chain's safety and
        liveness do not depend on this attribution; per
        \S\ref{sec:lifecycle:rollback}, a failed activation
        triggers rollback rather than slashing.
\end{itemize}

\subsection{Composition with Quasar Horizon}
\label{sec:security:horizon}

Pulsar is one of three lanes in QuasarCert
\cite{quasarcertsoundness}. The composed soundness theorem
(Theorem~5 of \cite{quasarcertsoundness}) bounds the
adversary advantage by the minimum of three per-lane advantages
(BLS, Pulsar, ML-DSA-via-Groth16); under quantum adversary the BLS lane
is broken by Shor and the standalone-PQ predicate
$\mathsf{VerifyPQ} = \mathsf{RT.Verify} \land \mathsf{ZK.Verify}$
remains sound, with Pulsar's contribution bounded by
Theorem~\ref{thm:pulsar-suf-cma} above
(Theorem~8 of \cite{quasarcertsoundness}, ``post-quantum
safety''). Subject-binding
replay protection across epochs is per
Theorem~9 of \cite{quasarcertsoundness} (``subject-binding replay
protection''): every Pulsar
pulse hashes the certificate subject including
$(\mathsf{chain\_id}, \mathsf{epoch}, \mathsf{round}, \mathsf{KeyEraID},
\mathsf{Generation})$, so cross-epoch replay reduces to BLAKE3
collision resistance.