papers/lp-073-pulsar/sections/05a-formal-model.tex

%% ===================================================================
%% LP-134 canonical naming (2025-12-15):
%% Per LP-134 (Lux Chain Topology), T-Chain has been split into:
%%   M-Chain — MPC ceremonies for bridge custody of EXTERNAL wallets
%%             (CGGMP21, FROST, Pulsar-general)
%%   F-Chain — FHE compute + TFHE bootstrap-key generation (encrypted EVM)
%% T-Chain is REMOVED entirely; teleport is B-Chain (bridgevm, LP-6000). No teleportvm.
%% Where this paper says "M-Chain MPC" / "M-Chain threshold governance" /
%% "M-Chain TFHE" / "M-Chain custody", read as M-Chain (MPC) or F-Chain (FHE).
%% ===================================================================

\section{Formal Model}
\label{sec:formal-model}

This section formalises the validator-set model, adversary model,
corruption model, and lineage chain on top of which the security
theorems of \S\ref{sec:security} are stated. The model is shared with
\cite{quasarcertsoundness} App.~C and is reproduced here in the form
needed by Pulsar's lifecycle theorems.

\subsection{Validator set, key era, and persistent group key}
\label{sec:formal-model:validators}

\begin{definition}[Validator set at epoch $\tau$]
\label{def:val-tau}
The Lux P-Chain anchors a validator-set sequence
$(\mathcal{V}_\tau)_{\tau \geq 0}$ where $\mathcal{V}_\tau \subseteq
\mathcal{V}^*$ is the validator subset active at epoch $\tau$ with
stake distribution $\mathrm{stk}_\tau: \mathcal{V}_\tau \to \mathbb{N}$.
The total stake at epoch $\tau$ is
$S_\tau = \sum_{v \in \mathcal{V}_\tau} \mathrm{stk}_\tau(v)$. The
Byzantine bound is $f_\tau < S_\tau / 3$ (i.e., total stake controlled
by an adversary at epoch $\tau$ is strictly less than one third of
$S_\tau$); the threshold $t_\tau$ is the smallest integer with
$t_\tau \geq \lceil 2 S_\tau / 3 \rceil$. Membership in
$\mathcal{V}_\tau$ is determined by P-Chain governance and stake
delegation; transitions between $\mathcal{V}_\tau$ and
$\mathcal{V}_{\tau+1}$ are permitted at every epoch boundary.
\end{definition}

\begin{definition}[Key era]
\label{def:key-era}
A \emph{key era} $\mathsf{E}_\eta$ is the persistent state
\[
  \mathsf{E}_\eta
  = (\eta,\; \mathbf{A}_\eta,\; \tilde{\mathbf{b}}_\eta,\;
     \mathsf{GKH}_\eta,\; \mathrm{birth}(\eta),\; \mathrm{death}(\eta))
\]
where $\eta \in \mathbb{N}$ is the era identifier;
$(\mathbf{A}_\eta, \tilde{\mathbf{b}}_\eta)$ is the persistent group
public key with $\mathbf{A}_\eta \in R_q^{m_{\mathrm{pk}} \times
n_{\mathrm{vec}}}$, $\tilde{\mathbf{b}}_\eta \in R_\xi^{m_{\mathrm{pk}}}$;
$\mathsf{GKH}_\eta = \mathsf{BLAKE3}(\mathsf{WriteTo}(\mathbf{A}_\eta)
\,\|\, \mathsf{WriteTo}(\tilde{\mathbf{b}}_\eta))[:32]$ the canonical
GroupKey hash; and $\mathrm{birth}(\eta), \mathrm{death}(\eta)$ are the
P-Chain block heights at which $\mathsf{E}_\eta$ is anchored and
superseded. An era is \emph{live} during $[\mathrm{birth}(\eta),
\mathrm{death}(\eta))$. The triple $(\mathbf{A}_\eta,
\tilde{\mathbf{b}}_\eta, \mathsf{GKH}_\eta)$ is byte-immutable across
the era's lifetime; this is Lemma~12 of \cite{quasarcertsoundness}
(``GroupKey byte-identity across Refresh and Reshare'') and
Theorem~\ref{thm:pulsar-reshare} of LP-073 \S\ref{sec:security}.
\end{definition}

\begin{definition}[Generation lineage within an era]
\label{def:gen-lineage}
Within $\mathsf{E}_\eta$, the chain records a strict-monotone
generation sequence
\[
  \mathcal{C}_\eta = \bigl(
    (g_0, V_0, t_0, r_0),\;
    (g_1, V_1, t_1, r_1),\;
    \ldots,\;
    (g_{k_\eta}, V_{k_\eta}, t_{k_\eta}, r_{k_\eta})
  \bigr)
\]
with $g_0 = 0$, $g_{i+1} = g_i + 1$ (strict-monotone bump on every
transition, including rollback). $V_i \subseteq \mathcal{V}_{\tau_i}$
is the active threshold committee at generation $i$, $t_i$ the
threshold, $r_i$ the RollbackFrom counter ($r_i = 0$ on forward;
$r_i = j > 0$ for a rollback to generation $j$). The lineage is
sealed at $\mathrm{death}(\eta)$ when a Reanchor produces
$\mathsf{E}_{\eta + 1}$.
\end{definition}

\subsection{KeyEraID lineage as a chain of tuples}
\label{sec:formal-model:lineage-chain}

The full lifecycle of Pulsar is a concatenation of per-era lineages:
\[
  \mathsf{LIN} = \bigl( \mathcal{C}_0, \mathcal{C}_1, \mathcal{C}_2,
                       \ldots \bigr).
\]
Every entry in every $\mathcal{C}_\eta$ is a tuple
$(\eta, g, V, t, r)$ committed on chain via the activation cert of
LP-073 \S\ref{sec:lifecycle:activation}. We treat $\mathsf{LIN}$ as a
labelled graph: nodes are tuples; edges are activations
(forward, $r = 0$) or rollbacks ($r > 0$). The Reanchor edge $\eta \to
\eta + 1$ is labelled with a fresh ceremony or DKG transcript and
carries the proof-of-knowledge that
$(\mathbf{A}_{\eta+1}, \tilde{\mathbf{b}}_{\eta+1})$ was sampled
honestly per LP-073 \S\ref{sec:lifecycle:dkg}. The Reanchor edge breaks
GroupKey continuity by definition: $\mathsf{GKH}_\eta \neq
\mathsf{GKH}_{\eta+1}$ except with probability $2^{-256}$
(BLAKE3 collision).

\begin{remark}[Multi-group lineage]
For grouped Pulsar deployments (\S\ref{sec:grouped}), the lineage chain
generalises to per-group lineages
$\mathsf{LIN}^{(j)}$, $j = 1, \ldots, G$, with each group running an
independent lifecycle. Group-level rotations do not affect other
groups; cross-group consistency is enforced only at the Horizon
certificate (\S\ref{sec:quasar}) where the $G$ Pulsar pulses are
combined into a Horizon-cert quorum.
\end{remark}

\subsection{Adversary models}
\label{sec:formal-model:adv}

We adopt the standard cryptographic adversary classes, refined for the
threshold-blockchain setting per Garay--Kiayias--Leonardos
\cite{garaybackbone}.

\begin{definition}[Honest-but-curious]
\label{def:hbc}
A party $v$ is \emph{honest-but-curious} (HBC) iff $v$ executes the
protocol exactly as specified but logs every received message,
intermediate computation, and outgoing message for offline analysis.
HBC parties do not deviate from the prescribed steps; they merely
attempt to extract as much information as possible from the protocol
transcript.
\end{definition}

\begin{definition}[Malicious]
\label{def:malicious}
A party $v$ is \emph{malicious} (or Byzantine) iff $v$ may deviate
arbitrarily from the protocol: omit messages, send malformed messages,
collude with other malicious parties, refuse to participate, or
participate with crafted inputs designed to bias the protocol output.
\end{definition}

\begin{definition}[Adversary classes]
\label{def:adv-classes}
We consider:
\begin{itemize}[nosep]
  \item $\mathcal{A}_C$: classical PPT, controls a corrupt set
        $F_\tau \subseteq \mathcal{V}_\tau$ at each epoch with
        $\mathrm{stk}_\tau(F_\tau) < t_\tau$, has access to all corrupt
        parties' state and signing oracles, polynomially bounded
        random-oracle queries.
  \item $\mathcal{A}_Q$: quantum PPT, same corrupt-set bound, full
        quantum random-oracle access (QROM), can run Shor and Grover
        in polynomial quantum time.
\end{itemize}
\end{definition}

\subsection{Static vs adaptive corruption}
\label{sec:formal-model:static-adaptive}

\begin{definition}[Static corruption {\cite{canetti2001uc}}]
The adversary $\mathcal{A}$ commits to the corrupt set
$F = \bigcup_\tau F_\tau$ before the protocol begins. Within an epoch,
$F_\tau$ is fixed at protocol start; new validators in
$\mathcal{V}_{\tau+1} \setminus \mathcal{V}_\tau$ are added to
$F_{\tau+1}$ only if $\mathcal{A}$ committed to them at the global
start.
\end{definition}

\begin{definition}[Adaptive corruption {\cite{canetti2001uc}}]
$\mathcal{A}$ may corrupt parties at any point during execution.
Upon corrupting $v$, $\mathcal{A}$ learns $v$'s current state (keys,
randomness, in-flight transcripts). The aggregate stake of corrupted
parties remains bounded by $t_\tau$ at every epoch $\tau$.
\end{definition}

\begin{definition}[Mildly adaptive (blockchain model)]
\label{def:mildly-adaptive}
$\mathcal{A}$ corrupts parties \emph{between rounds} but not within a
round. This is the canonical model for partially synchronous
blockchain consensus per \cite{garaybackbone} and matches the
assumption in LP-020 \cite{lp020}.
\end{definition}

\begin{definition}[Erasure / Fischlin hybrid]
\label{def:erasure}
A party $v$ \emph{erases} a value $x$ at time $\tau$ if any subsequent
state inspection at $\tau' > \tau$ does not reveal $x$. The
\emph{erasure model} assumes honest parties erase per-round
randomness immediately after the round completes; the
\emph{Fischlin hybrid} \cite{fischlin2005} replaces this with a
programmable random oracle that pays a $O(n \cdot Q_H)$ multiplicative
loss in the security reduction.
\end{definition}

\paragraph{Pulsar adopts both.} The Go canonical performs explicit
memory zeroing of $r^*, e^*, R_i, E_i$ after Round 2 completes
(\texttt{sign/sign.go} signing-finish blocks; \texttt{primitives/hash.go}
PRNG buffer scrub). HSM-backed signing on the Lux M-Chain (LP-020
\cite{lp020}~\S5) provides hardware-enforced erasure. By
Cor.~16 (``Adaptive soundness, erasure model'') of
\cite{quasarcertsoundness}, Theorem~\ref{thm:pulsar-suf-cma} extends to
mildly
adaptive corruption with no additional security loss.

\subsection{Soundness and liveness goals}
\label{sec:formal-model:goals}

We state the formal goals that Pulsar must satisfy as a permissionless-
consensus threshold-signature layer.

\begin{definition}[Soundness goal: SUF-CMA across eras]
\label{def:soundness}
For every era $\mathsf{E}_\eta$ and every adversary
$\mathcal{A} \in \{\mathcal{A}_C, \mathcal{A}_Q\}$ within
$(Q_S, Q_H, Q_M, T)$ budget,
\[
  \mathsf{Adv}^{\mathrm{tSUF-CMA}}_{\Pi_{\mathrm{Pulsar}}, \eta, \mathcal{A}}(\lambda)
  \;\leq\; \mathsf{negl}(\lambda)
\]
under MLWE/MSIS at the LP-073 \S2 parameters and the random-oracle /
PRF assumptions on BLAKE3.
\end{definition}

\begin{definition}[Lifecycle soundness goal: lineage unforgeability]
\label{def:lineage-soundness}
For every adversary $\mathcal{A}$, the probability that $\mathcal{A}$
produces an alternate valid lineage $\mathsf{LIN}^\star \neq
\mathsf{LIN}$ at the same epoch sequence is bounded by
$\mathsf{Adv}^{\mathrm{tSUF-CMA}} + Q_H / 2^{256}$
(Theorem~\ref{thm:pulsar-lineage}).
\end{definition}

\begin{definition}[Liveness goal: progress under partial synchrony]
\label{def:liveness}
Under the partial-synchrony model of \cite{garaybackbone} with
GST $\Delta$, every epoch with $\mathrm{stk}(\mathcal{V}_\tau \setminus
F_\tau) \geq t_\tau$ produces at least one accepting Pulsar pulse
within wall-clock time $T_{\mathrm{Pulsar}} + \Delta$ where
$T_{\mathrm{Pulsar}}$ is the Round~1 + Round~2 + Combine wall-clock at
$|V_\tau| = K$ on the production hardware (LP-073
\S\ref{sec:implementation}, $\sim 200$~ms at $K = 5$ on Apple M2 Ultra,
under $1$~s at $K = 21$).
\end{definition}

\begin{definition}[Activation soundness]
\label{def:activation-soundness}
Every accepted lifecycle transition $\mathcal{C}_\eta[i] \to
\mathcal{C}_\eta[i+1]$ within an era satisfies the activation cert
soundness of Theorem~\ref{thm:pulsar-activation}: under unchanged
$(\mathbf{A}_\eta, \tilde{\mathbf{b}}_\eta)$, the new committee's
shares Lagrange-recombine to $\mathbf{s}_\eta$ except with
probability $\leq \mathsf{Adv}^{\mathrm{tSUF-CMA}}$.
\end{definition}

\begin{definition}[Rollback soundness]
\label{def:rollback-soundness}
Every accepted Rollback transition restores a state that was committed
on chain at a prior generation; the restored state's GroupKey hash
matches by Lemma~12 of \cite{quasarcertsoundness}
(``GroupKey byte-identity''), and the lineage audit of
Lemma~13 of \cite{quasarcertsoundness} (``Rollback-lineage forward
reconstruction'') reconstructs the canonical
forward path uniquely.
\end{definition}

The four goals (Definitions~\ref{def:soundness}--\ref{def:rollback-soundness})
together formalise the security target of LP-073: a permissionless-
consensus PQ threshold signature with verifiable lifecycle, per-era
SUF-CMA, and progress under partial synchrony with mildly adaptive
adversaries up to $f < n/3$ stake.

\subsection{What this model omits}
\label{sec:formal-model:omits}

Three model assumptions are made explicit so that downstream proofs
inherit them cleanly:

\begin{itemize}[nosep]
  \item \textbf{P-Chain consensus.} The validator-set sequence
        $(\mathcal{V}_\tau)$ is delivered to Pulsar by the P-Chain. We
        assume P-Chain consensus is sound and live; Pulsar inherits
        epoch-boundary commitments by reference (LP-020
        \cite{lp020}~\S6). A P-Chain-level safety violation that
        produced two conflicting $\mathcal{V}_\tau$ sequences would
        invalidate Pulsar's epoch-bound state, but this is
        out-of-scope: it is treated by Theorem~7.5 of LP-020 and is
        the responsibility of QuasarCert as a whole.
  \item \textbf{Network model.} We assume partially synchronous
        delivery with GST $\Delta$ post-stabilisation. Asynchronous
        adversaries can delay messages indefinitely pre-GST; this
        affects liveness only, not soundness, and is matched by every
        BFT consensus engine in production.
  \item \textbf{Setup ceremony.} Genesis of $\mathsf{E}_0$ is one of
        (a) foundation MPC ceremony with toxic-waste assumption
        confined to the first era, or (b) Pedersen DKG over $R_q$ per
        \S\ref{sec:lifecycle:dkg}. Subsequent Reanchors use the same
        two paths. Both paths are formalised in App.~D of
        \cite{quasarcertsoundness} (multi-party SRS ceremony, security
        per Bowe--Gabizon--Miers \cite{bowe2017}).
\end{itemize}