papers/lux-nist-mptc-submission/evaluation-report/security-analysis.tex

\documentclass[11pt,a4paper]{article}
\usepackage{../../shared/luxcover}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{graphicx}
\usepackage{hyperref}
\usepackage{booktabs}
\usepackage{enumitem}
\usepackage{xcolor}

\hypersetup{colorlinks=true,linkcolor=black,citecolor=blue,urlcolor=blue}

\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{remark}{Remark}

\title{Lux MPTC Security Analysis}
\author{
Lux Research\\
\textit{Lux Industries, Inc.}\\
\texttt{[email protected]}
}
\date{2026-03-03}

\begin{document}

\luxcoverpage

\section*{Abstract}

\noindent We present Lux, a hybrid post-quantum consensus architecture for DAG-native chains. Lux separates fast operational finality from durable post-quantum finality. Validators emit Photons over a Nebula DAG substrate; classical BLS aggregates form Beams for low-latency confirmation, while ML-DSA attestations and Pulsar lattice-threshold Pulses provide post-quantum finality over Nebula roots. Prism binds all certificate lanes to the same transcript, and Quasar reaches Horizon finality when the bound lanes verify.

\textbf{This document.} The security-analysis summary for the NIST MPTC submission. The full proofs live in the canonical proof bucket (\texttt{proofs/pulsar/}, \texttt{proofs/lss/}, \texttt{proofs/quasar/}, \texttt{proofs/definitions/}); this document summarizes the theorems and points at the bucket files. Lean / TLA+ / Tamarin mechanizations are also cited.

\section{Pulsar SUF-CMA}

\begin{theorem}[Pulsar SUF-CMA under MLWE/MSIS]
\label{thm:pulsar-suf-cma-sec}
Let $\mathcal{A}$ be a probabilistic polynomial-time adversary against Pulsar with at most $q_S$ signing queries and at most $t-1$ corrupted parties. Then
\[
  \mathrm{Adv}^{\mathsf{SUF\text{-}CMA}}_{\mathsf{Pulsar}}(\mathcal{A})
  \;\leq\; q_S \cdot \mathrm{Adv}^{\mathsf{MLWE}}_{q, \sigma_E}(\mathcal{B}_1)
  + \mathrm{Adv}^{\mathsf{MSIS}}_{q, [\mathbf{A}|-c\tilde{\mathbf{b}}], 2B}(\mathcal{B}_2)
  + \mathrm{negl}(\lambda).
\]
\end{theorem}

Full proof: \texttt{proofs/pulsar/unforgeability.tex}; concrete parameters in \texttt{quasar-cert-soundness.tex} App.~E give classical $\geq 2^{142}$ and quantum $\geq 2^{130}$ via BDGL sieving + Grover. Lean: \texttt{Crypto.Pulsar.corona\_pq\_unforgeability} \cite{leancrypto}.

\section{Reshare preserves master secret}

\begin{theorem}[Reshare preserves master secret]
The new shares $\{\mathsf{Share}'_j = G(\beta_j)\}$ are valid $(t_{\mathrm{new}}, |V_{\mathrm{new}}|)$-Shamir shares of the same master secret $\mathbf{s}$, where $G(X) = \sum_{i \in Q} \lambda^Q_i \cdot g_i(X)$. Persistent group public key $(\mathbf{A}, \tilde{\mathbf{b}})$ unchanged.
\end{theorem}

Full proof: \texttt{proofs/pulsar/reshare-preservation.tex}. Lean: \texttt{Crypto.Threshold.Reshare.reshare\_same\_secret}, \texttt{reshare\_preserves\_public\_key}.

\section{Activation circuit-breaker safety}

\begin{theorem}[Activation cert is necessary and sufficient for safe transition]
A successful activation cert verify under unchanged GroupKey implies (i) the new shares recombine to the same master secret, (ii) the new committee can produce verifying signatures, (iii) the KeyEraID is unchanged. Conversely, failure of (i), (ii), or (iii) implies activation cert verify fails with overwhelming probability.
\end{theorem}

Full proof: \texttt{proofs/pulsar/activation-safety.tex}; companion-cited as Theorem 14 (\texttt{thm:activation-soundness}) of \cite{quasarcertsoundness}.

\begin{lemma}[Failure-mode containment]
If activation cert verify fails, the chain remains at the prior state. The candidate state is discarded; the LSS RollbackManager retains the prior snapshot. This is a structural property of the chain's state-machine acceptance rule, not a cryptographic assumption.
\end{lemma}

Reference: \texttt{proofs/pulsar/activation-safety.tex} Lemma \texttt{lem:activation-fail-safe}.

\section{Hash-suite separation}

\begin{theorem}[Cross-suite signatures do not collide]
A Pulsar signature under one hash suite (Pulsar-SHA3 or Pulsar-BLAKE3) does not verify under the other, with overwhelming probability over the verifier's hash function.
\end{theorem}

Full proof: \texttt{proofs/pulsar/hash-suite-separation.tex}. The HashSuiteID is bound into every transcript via TupleHash personalization; cross-suite forgery would require a collision on the personalized TupleHash.

\section{LSS lifecycle invariants}

\begin{lemma}[Generation monotonicity]
$g$ increases monotonically by exactly $1$ per $\mathsf{DynamicReshare}$ or $\mathsf{Refresh}$. On $\mathsf{Rollback}$, $g \mapsto g_{\mathrm{current}} + 1$ with $\mathsf{rb} = g_{\mathrm{current}}$.
\end{lemma}

\begin{lemma}[KeyEraID stability]
$\eta$ is unchanged by $\mathsf{Refresh}$, $\mathsf{Reshare}$, or $\mathsf{Rollback}$. Increments only on $\mathsf{Reanchor}$.
\end{lemma}

\begin{lemma}[GroupKey byte-identity]
GroupKey pointer is byte-identical across every $\mathsf{Refresh}$ and $\mathsf{Reshare}$ within an era.
\end{lemma}

\begin{lemma}[Rollback lineage reconstructibility]
The forward lineage of the chain is reconstructible from the snapshot history.
\end{lemma}

Full proofs: \texttt{proofs/lss/lifecycle-safety.tex}.

\section{Rollback safety}

\begin{theorem}[Rollback never crosses an era boundary]
$\mathsf{Rollback}(g_{\mathrm{target}})$ succeeds iff $g_{\mathrm{target}}$ is in the current era's snapshot history. Rollback to a snapshot with $\eta_{\mathrm{snapshot}} \neq \eta_{\mathrm{current}}$ is refused.
\end{theorem}

\begin{theorem}[Rollback preserves liveness under failed activation]
If $\mathsf{state}_{g+1}$'s activation cert fails verification and the chain calls $\mathsf{Rollback}(g)$, the chain continues to produce signatures under $\mathsf{state}_g$'s shares.
\end{theorem}

Full proofs: \texttt{proofs/lss/rollback-safety.tex}.

\section{Quasar Horizon soundness (consensus composition)}

\begin{theorem}[Horizon-final implies all lanes verify the same transcript]
A Prism-accepted Horizon certificate cannot exist for two distinct $\mathsf{NebulaRoot}$s at the same $(\mathsf{epoch}, \mathsf{round})$ except with negligible probability under (i) BLS12-381 co-CDH, (ii) MLWE/MSIS, and (iii) FIPS 204 ML-DSA EUF-CMA. The lanes are independent; quantum break of one does not break the others.
\end{theorem}

Full proof: \texttt{proofs/quasar/horizon-soundness.tex}; companion-cited from \cite{quasarcertsoundness} Theorem 7.5 (classical soundness), Theorem 7.6 (parallel-lane liveness), Theorem 7.7 (PQ safety). Lean: \texttt{Consensus/Quasar.lean}: \texttt{triple\_requires\_all}, \texttt{quantum\_safe\_triple}, \texttt{independent\_pq\_from\_classical}, \texttt{cert\_intersection}, \texttt{unique\_per\_round}.

\section{L2 co-validation security inheritance}

\begin{theorem}[L2 inherits from primary]
An L2's safety bound is at least the minimum of the primary's safety bound and the L2's own validator-set safety bound. Forging conflicting L2 finality requires (i) compromising enough of the L2's validators, AND (ii) either compromising the primary's validators or breaking transcript binding.
\end{theorem}

Full proof: \texttt{proofs/quasar/l1-l2-covalidation.tex}.

\section{Warp 2.0 envelope unforgeability}

\begin{theorem}[Warp 2.0 envelope unforgeability]
A successful $\mathsf{VerifyWithOptions}$ implies any forgery on the same $(\mathsf{sourceChainID}, \mathsf{sourceNebulaRoot}, \mathsf{sourceKeyEraID}, \mathsf{sourceGeneration})$ tuple with a different $\mathsf{payload}$ requires breaking either co-CDH (Beam) or MLWE/MSIS (Pulse).
\end{theorem}

Full proof: \texttt{proofs/quasar/warp-pq-soundness.tex}.

\section{Lane independence under quantum advice}

\begin{lemma}[Lane independence]
A polynomial-time adversary $\mathcal{A}$ with quantum oracle access to BLS12-381's discrete log gains no MLWE/MSIS-relevant computational advantage; the Pulse lane remains unforgeable. Symmetrically, an MLWE-oracle-equipped $\mathcal{A}$ enjoys no advantage against BLS.
\end{lemma}

Full argument: \texttt{proofs/pq-finality-no-bls.tex}; \cite{pqfinalitynobls}.

\section{Honest classification of the Groth16 wrapper}

\begin{remark}[Groth16 wrapper does not contribute PQ security]
The Z-Chain Groth16 rollup proof of ML-DSA cert-set verification is a \emph{classical succinct proof of post-quantum signature verification}. Pairing-based SNARKs over BLS12-381 break under Shor. Horizon's PQ soundness flows from ML-DSA signatures and Pulsar Pulse alone; the Groth16 proof is a compatibility / compression artifact.
\end{remark}

Reference: Remark \texttt{rem:groth16-wrapper} of \texttt{proofs/quasar/horizon-soundness.tex}; Remark \texttt{rem:groth16-not-pq} of \texttt{proofs/definitions/finality-definitions.tex}; LP-105 \cite{lp105} \S"Proof-lane classification".

The classification is enforced in code: \texttt{warp/pulsar/IsPQRootOfTrust} returns false for Groth16-wrapped lanes (\texttt{warp/pulsar/groth16\_classification\_test.go}).

\section{Mechanization summary}

\begin{tabular}{@{}p{0.40\textwidth}p{0.55\textwidth}@{}}
  \toprule
  \textbf{Theorem} & \textbf{Mechanization} \\
  \midrule
  Pulsar SUF-CMA & Lean: \texttt{Crypto.Pulsar.corona\_pq\_unforgeability} \\
  Reshare preserves master secret & Lean: \texttt{Crypto.Threshold.Reshare.reshare\_same\_secret} \\
  GroupKey byte-identity & Lean: \texttt{Crypto.Threshold.Reshare.reshare\_preserves\_public\_key} \\
  Triple consensus composition & Lean: \texttt{Consensus/Quasar.lean} \\
  BFT safety / liveness / finality & Lean: \texttt{Consensus/\{Safety,Liveness,Finality,BFT\}.lean} \\
  Quasar protocol model & TLA+: \texttt{tla/Quasar.tla} (model-checked) \\
  Quasar protocol handshake & Tamarin: \texttt{tamarin/QuasarConsensus.spthy} \\
  FROST threshold (Lens) & Tamarin: \texttt{tamarin/FROSTThreshold.spthy} \\
  PQ encryption (Lumen) & Tamarin: \texttt{tamarin/pq\_encryption.spthy} \\
  Property-based testing & Go: \texttt{proofs/property/} \\
  \bottomrule
\end{tabular}

The mechanizations are not exhaustive (e.g., a UC treatment is open work); they cover the most security-critical theorems. The full proof bucket at \texttt{github.com/luxfi/proofs/} is the source of truth.

\section{Adversary model}

The adversary is computationally bounded with possibly quantum-aided lower-bound queries. It adaptively corrupts up to $f$ validators with $f < n/3$. It controls the network (delay, drop, reorder) but not the chain's state-machine acceptance rule. Its quantum and classical oracles are independent: a quantum DL oracle gives no MLWE/MSIS advantage, and vice versa.

\section{Side-channel posture}

Constant-time review documented separately in the side-channel-considerations document of this submission. Summary: the lattice math (Pulsar) and curve math (Lens) have been reviewed; GPU paths are research, not production; the lattigo deserializer hardening (Section "Fuzz-Discovered Vulnerability" of \cite{luxwarpv2}) is in production.

\section{Audit status}

The Lux research audit (\cite{quasarcertsoundness} App. + \texttt{papers/AUDIT.pdf}) covers the consensus engine and threshold-cryptography stack. The audit cites the proof bucket; mechanizations and the production-stack tests are the audit-supporting evidence. The audit is internal to Lux; an external third-party audit is in the production-research roadmap.

\bibliographystyle{plain}
\bibliography{../references}

\end{document}