mirror of
https://github.com/luxfi/proofs.git
synced 2026-10-30 15:21:05 +00:00
zeekayandHanzo Dev
2dd030dd98
Each of these made the corpus unsound: from a false axiom every theorem in
it follows, so the 756 stated results meant nothing while they stood.
Crypto/Magnetar.lean carried two axioms of the shape
∀ (oracle : Nat → Nat), ∃ (x : Nat), oracle x ≠ x
which the identity function refutes, yielding `∃ x, x ≠ x`. Both were roots
of `lean_lib Crypto`, so both compiled. Neither had a user. Family
disjointness quantifies over adversaries and advantages; `Nat → Nat` cannot
state it, so it is prose until the advantage model exists.
Protocol/Handshake.lean defined the session KDF as integer addition and then
axiomatised that distinct transcripts give distinct keys. ⟨1,1,1⟩ and ⟨1,0,2⟩
both derive 3 with transcripts 1 ≠ 2. `deriveSessionKey` is now opaque, which
is what a hash is in a model, and collision resistance is the one assumed
property. `transcript_binding` followed from unfolding the addition; it now
follows from the assumption.
Consensus/Safety.lean `unique_threshold` counts `honestPreferring` over
`Finset.univ` — the whole validator set, not the k-sample — so it needs
`2 * alpha > n`. Legal counterexample without it: n = 1000, f = 100, k = 20,
alpha = 14, with 900 honest nodes split 450/450, satisfies every hypothesis
and concludes v1 = v2. The hypothesis is now stated and threaded through
`theorem safety`, which makes the real limitation visible in the type: with
alpha ≤ k ≤ n it forces sampling more than half the network every round. In
the sub-sampled regime the protocol runs, safety is probabilistic and no
theorem of this shape holds. Consensus.ThresholdProof already proves the
pigeonhole under exactly this hypothesis.
strict-e2e-pq cited ePrint 2024/1113 as "Corona: A Lattice-Based Threshold
Signature for Post-Quantum Consensus" with no authors. That paper is
Ringtail, by Boschini, Kaviani, Lai, Malavolta, Takahashi and Tibouchi.
Corona is our implementation of it. Restored their title and their names.
Verified with a local lake build over every library.
Co-authored-by: Hanzo Dev <[email protected]>
297 lines
12 KiB
TeX
297 lines
12 KiB
TeX
\documentclass[11pt,a4paper]{article}
|
|
\usepackage[utf8]{inputenc}
|
|
\usepackage[T1]{fontenc}
|
|
\usepackage{amsmath,amssymb,amsfonts,amsthm}
|
|
\usepackage{geometry}
|
|
\geometry{margin=1in}
|
|
\usepackage{hyperref}
|
|
\usepackage{listings}
|
|
\usepackage{xcolor}
|
|
\usepackage{enumitem}
|
|
\usepackage{booktabs}
|
|
|
|
\hypersetup{colorlinks=true,linkcolor=black,citecolor=blue,urlcolor=blue}
|
|
|
|
\lstset{
|
|
basicstyle=\ttfamily\small,
|
|
breaklines=true,
|
|
frame=single,
|
|
numbers=left,
|
|
numberstyle=\tiny\color{gray},
|
|
showstringspaces=false
|
|
}
|
|
|
|
\newtheorem{theorem}{Theorem}
|
|
\newtheorem{lemma}[theorem]{Lemma}
|
|
\newtheorem{definition}{Definition}
|
|
\newtheorem{proposition}[theorem]{Proposition}
|
|
\newtheorem{remark}{Remark}
|
|
|
|
\title{LUX\_STRICT\_E2E\_PQ Soundness:\\
|
|
Formal Statement of the End-to-End Post-Quantum Profile}
|
|
\author{Lux Industries, Inc.\\\texttt{[email protected]}}
|
|
\date{2026}
|
|
|
|
\begin{document}
|
|
\maketitle
|
|
|
|
\begin{abstract}
|
|
This note carries the formal soundness statement for the
|
|
\texttt{LUX\_STRICT\_E2E\_PQ} profile defined in
|
|
\texttt{luxfi/papers/lp-stricte2epq}. We state the four soundness claims (1)
|
|
ML-DSA-65 transaction authorisation, (2) SHA3-384 Merkle inclusion in the
|
|
Z-Chain registry, (3) collision-resistance of the Q-Chain
|
|
\texttt{ComputeRoundDigest}, and (4) Pulsar finality under Module-LWE. The
|
|
machine-checked counterparts live in Lean 4 (\texttt{StrictE2EPQ/}), TLA+
|
|
(\texttt{tla/StrictPQProfile.tla}), and Go property tests
|
|
(\texttt{property/strict\_pq\_test.go}).
|
|
\end{abstract}
|
|
|
|
\section{Profile pinning}
|
|
|
|
\begin{definition}[Locked profile]
|
|
\label{def:locked}
|
|
A \emph{locked profile} is a \texttt{ChainSecurityProfile} (the Go struct
|
|
at \texttt{luxfi/consensus/config/security\_profile.go:244}) such that:
|
|
\begin{enumerate}[leftmargin=2em,nosep]
|
|
\item Every enum field is non-zero (zero-value-invalid).
|
|
\item \texttt{Validate} accepts it.
|
|
\item \texttt{ComputeHash} returns a stable 48-byte digest under
|
|
customization \texttt{LUX\_CHAIN\_SECURITY\_V1} (cSHAKE256 / SHA3-384,
|
|
SP 800-185).
|
|
\end{enumerate}
|
|
\end{definition}
|
|
|
|
\begin{definition}[Strict-PQ profile]
|
|
\label{def:strict-pq}
|
|
A locked profile $P$ is \emph{strict-PQ} iff:
|
|
\begin{align*}
|
|
& P.\texttt{HashSuiteID} && = \texttt{SHA3-384/cSHAKE256}, \\
|
|
& P.\texttt{IdentitySchemeID} && = \texttt{ML-DSA-65}, \\
|
|
& P.\texttt{FinalitySchemeID} && = \texttt{Pulsar-65}, \\
|
|
& P.\texttt{HighValueSchemeID} && \in \{\texttt{Pulsar-65}, \texttt{Pulsar-87}\}, \\
|
|
& P.\texttt{ProofPolicyID} && = \texttt{ProofPolicy128bitPQ}, \\
|
|
& P.\texttt{AllowedProofBackends} && \subseteq \{\texttt{p3q}, \texttt{Plonky3-SHA3}\}, \\
|
|
& P.\texttt{MinSoundnessBits} && \ge 128, \\
|
|
& P.\texttt{MinHashOutputBits} && \ge 384, \\
|
|
& P.\texttt{RequireTransparent} && = \texttt{true}, \\
|
|
& P.\texttt{ForbidPairings} && = \texttt{true}, \\
|
|
& P.\texttt{ForbidKZG} && = \texttt{true}, \\
|
|
& P.\texttt{ForbidTrustedSetup} && = \texttt{true}, \\
|
|
& P.\texttt{ForbidClassicalSNARKs} && = \texttt{true}, \\
|
|
& P.\texttt{ForbidDevProofs} && = \texttt{true}, \\
|
|
& P.\texttt{ForbidFallbacks} && = \texttt{true}, \\
|
|
& P.\texttt{RequireTypedTxAuth} && = \texttt{true}, \\
|
|
& P.\texttt{WalletSchemeID} && = \texttt{ML-DSA-65}, \\
|
|
& P.\texttt{ContractAuthSchemeID} && = \texttt{ML-DSA-65}, \\
|
|
& P.\texttt{BridgeProfileID} && = \texttt{BridgeProfileStrictPQ}, \\
|
|
& P.\texttt{DRBGSchemeID} && = \texttt{Hash\_DRBG-SHA3-384}.
|
|
\end{align*}
|
|
\end{definition}
|
|
|
|
\begin{remark}
|
|
The strict-PQ profile is unique up to the choice of
|
|
\texttt{HighValueSchemeID} ($65$ or $87$). The production canonical at
|
|
\texttt{luxfi/consensus@12097034} pins
|
|
\texttt{ProfileLuxStrictPQ} with \texttt{HighValueSchemeID = Pulsar-87}
|
|
and golden digest \texttt{93efd103\ldots323bfcd0}.
|
|
\end{remark}
|
|
|
|
\section{Soundness claims}
|
|
|
|
\subsection{TX-AUTH-SOUND: transaction authorisation soundness}
|
|
|
|
\begin{theorem}[TX-AUTH-SOUND]
|
|
\label{thm:tx-auth-sound}
|
|
Let $P$ be a strict-PQ profile (Def.~\ref{def:strict-pq}). Let $E$ be a
|
|
\texttt{TxAuthEnvelope} accepted by \texttt{VerifyTxAuthEnvelope}$(P, E)$.
|
|
Then there exists a private key $\textsc{sk}$ such that the public key
|
|
$\textsc{pk}$ corresponding to $\textsc{sk}$ is:
|
|
\begin{enumerate}[leftmargin=2em,nosep]
|
|
\item Registered as \texttt{KeyStatusActive} in
|
|
\texttt{ZRegistryRoots.IdentityRoot} at the epoch when $E$ was
|
|
submitted.
|
|
\item Hashes to $E.\texttt{PublicKeyRef}$ under cSHAKE256.
|
|
\item Owned by $E.\texttt{AccountID}$ (per the Z-Chain account
|
|
binding).
|
|
\item $\textsc{sk}$ produced $E.\texttt{Signature}$ via the FIPS 204
|
|
\texttt{ML-DSA-65.Sign} algorithm applied to
|
|
$E.\texttt{SigningDigest}()$, under the FIPS 204 \S 5.2
|
|
\texttt{ctx} value \texttt{LUX\_ZCHAIN\_REGISTRY\_V1}.
|
|
\end{enumerate}
|
|
The reduction is to: (i) the EUF-CMA security of ML-DSA-65 under
|
|
Module-LWE \cite{fips204,dilithium}; (ii) collision-resistance of cSHAKE256
|
|
on the 17-field TupleHash256 transcript under customization
|
|
\texttt{LUX\_TX\_AUTH\_V1}; (iii) collision-resistance of cSHAKE256 on the
|
|
Z-Chain leaf and node customizations.
|
|
\end{theorem}
|
|
|
|
\begin{proof}[Proof sketch]
|
|
\texttt{VerifyTxAuthEnvelope} checks structural validity, profile
|
|
identity, suite, scheme, gate, Z-Chain binding, account / pubkey
|
|
binding, expiry, nonce, and finally signature. The signature step is
|
|
ML-DSA-65 verify against the resolved pubkey on the
|
|
\texttt{SigningDigest()}; by EUF-CMA, an accepting verifier implies
|
|
either a forgery (which contradicts the assumption that ML-DSA-65 is
|
|
EUF-CMA-secure) or the existence of $\textsc{sk}$.
|
|
|
|
Collision-resistance of cSHAKE256 on the transcript closes the
|
|
``two envelopes one digest'' attack: a verifier accepting $E$ under the
|
|
17-field transcript implies no $E' \ne E$ with
|
|
\texttt{SigningDigest}$(E') = \texttt{SigningDigest}(E)$.
|
|
|
|
The Z-Chain binding step rejects $E$ if $E.\texttt{ZIdentityRoot}$
|
|
disagrees with the consensus-bound \texttt{IdentityRoot}. The reduction
|
|
to Merkle collision-resistance is standard.
|
|
\end{proof}
|
|
|
|
\subsection{ZCHAIN-INCLUSION-SOUND: registry inclusion proof soundness}
|
|
|
|
\begin{theorem}[ZCHAIN-INCLUSION-SOUND]
|
|
\label{thm:zchain-inclusion}
|
|
Let $P$ be a strict-PQ profile. Let $\rho$ be a \texttt{MerkleProof}
|
|
accepted by \texttt{VerifyAuthPassed}$(P, \texttt{root}, \texttt{leaf},
|
|
\rho)$ (\texttt{luxfi/consensus/protocol/zchain/registry/auth\_proof.go:118}).
|
|
Then the \texttt{leaf} hash was committed in the Merkle tree
|
|
identified by \texttt{root} via the path $\rho$.
|
|
|
|
The reduction is to collision-resistance of cSHAKE256 on the leaf
|
|
customization \texttt{LUX\_MERKLE\_LEAF\_V1} and the node customization
|
|
\texttt{LUX\_MERKLE\_NODE\_V1}.
|
|
\end{theorem}
|
|
|
|
\begin{proof}[Proof sketch]
|
|
The verifier walks the proof reconstructing the root via the leaf
|
|
customization at the bottom and the node customization at each internal
|
|
level. Distinct leaf and node customizations prevent the
|
|
``second preimage on Merkle trees'' attack where a leaf hash is
|
|
reinterpreted as an internal-node hash. Reconstructed root equality to
|
|
\texttt{root} implies (under cSHAKE256 collision-resistance) that the
|
|
\texttt{leaf} was committed via $\rho$. Conversely, any verifier-accepting
|
|
proof either witnesses true inclusion or breaks cSHAKE256
|
|
collision-resistance.
|
|
\end{proof}
|
|
|
|
\subsection{ROUND-DIGEST-CR: Q-Chain digest collision-resistance}
|
|
|
|
\begin{theorem}[ROUND-DIGEST-CR]
|
|
\label{thm:round-digest-cr}
|
|
The function \texttt{ComputeRoundDigest} on \texttt{QBlock} is
|
|
collision-resistant: for two distinct \texttt{QBlock} values $q_1 \ne
|
|
q_2$, \texttt{ComputeRoundDigest}$(q_1) \ne$
|
|
\texttt{ComputeRoundDigest}$(q_2)$ with probability $\ge 1 - 2^{-192}$
|
|
against a polynomially-bounded quantum adversary.
|
|
|
|
The reduction is to collision-resistance of cSHAKE256 on the 23-axis
|
|
TupleHash256 transcript under customization \texttt{LUX\_QBLOCK\_V1}.
|
|
\end{theorem}
|
|
|
|
\begin{proof}[Proof sketch]
|
|
\texttt{ComputeRoundDigest} is TupleHash256 over the 23-axis canonical
|
|
byte serialisation under the customization. A collision in
|
|
\texttt{ComputeRoundDigest} produces a collision in TupleHash256 in the
|
|
$\textsc{cSHAKE256}$ domain. Quantum security of $\textsc{cSHAKE256}$ at
|
|
output length 48 bytes (384 bits) is Grover-bounded at $2^{-192}$.
|
|
\end{proof}
|
|
|
|
\subsection{PULSAR-SOUND: finality signature soundness}
|
|
|
|
\begin{theorem}[PULSAR-SOUND]
|
|
\label{thm:pulsar-sound}
|
|
Let $P$ be a strict-PQ profile. Let $\Sigma$ be a Pulsar-65 aggregate
|
|
signature accepted by \texttt{Pulsar.Verify}$(\textsc{gpk}, m, \Sigma)$
|
|
where \textsc{gpk} is the group public key for the committee bound in
|
|
$\texttt{QBlock.ValidatorSetRoot}$ and $m$ is
|
|
$\texttt{QBlock.ComputeRoundDigest}()$. Then either (i) at least 43 of
|
|
the 64 committee parties contributed an honest partial signature, or
|
|
(ii) the protocol identifies the misbehaving party via
|
|
\texttt{abort}\cite{lp073}.
|
|
|
|
The reduction is to the M-LWE assumption \cite{mlwe,regev2009} for
|
|
soundness, the rejection-sampling slack
|
|
$\eta_\varepsilon = 2.65$ for completeness, and BLAKE3-keyed MAC
|
|
unforgeability for Round 1 authentication.
|
|
\end{theorem}
|
|
|
|
\begin{proof}[Proof sketch]
|
|
Pulsar aggregates linearly: a verifier-accepting aggregate signature
|
|
reconstructs $\mathbf{A} z - \tilde{\mathbf{b}} c$ in $R_\nu$ under the
|
|
hint bound. By the two-round threshold ML-DSA argument
|
|
\cite{dttf2024,thresholdraccoon}, soundness reduces to M-LWE.
|
|
Identifiable abort \cite{lp073,boschini2024ringtail} closes the ``one bad
|
|
party blocks the round'' attack.
|
|
\end{proof}
|
|
|
|
\section{Conjunction: E2E PQ}
|
|
|
|
\begin{theorem}[E2E-PQ-COVERAGE]
|
|
\label{thm:e2e-coverage}
|
|
Let $P$ be a strict-PQ profile. Let $\tau$ be a transaction that
|
|
successfully closes a Q-Chain epoch under $P$. Then $\tau$ is bound, end
|
|
to end, to FIPS 203 / 204 / 205 primitives and the SHA3 family, via:
|
|
\begin{enumerate}[leftmargin=2em,nosep]
|
|
\item TX-AUTH-SOUND (Thm.~\ref{thm:tx-auth-sound}) for the
|
|
submission gate.
|
|
\item ZCHAIN-INCLUSION-SOUND (Thm.~\ref{thm:zchain-inclusion}) for
|
|
the registry lookup.
|
|
\item ROUND-DIGEST-CR (Thm.~\ref{thm:round-digest-cr}) for the
|
|
QBlock binding.
|
|
\item PULSAR-SOUND (Thm.~\ref{thm:pulsar-sound}) for the
|
|
finality cert.
|
|
\end{enumerate}
|
|
A Shor-capable adversary against the stack reduces to breaking one of:
|
|
ML-DSA-65 (EUF-CMA / M-LWE), Pulsar-65 (M-LWE), cSHAKE256
|
|
(collision-resistance), or the SHA3 family at $\ge 384$-bit output.
|
|
\end{theorem}
|
|
|
|
\section{Companion artefacts}
|
|
|
|
\begin{itemize}[leftmargin=2em,nosep]
|
|
\item \texttt{StrictE2EPQ/Profile.lean} carries the Lean 4 statement of
|
|
Definition~\ref{def:strict-pq} and the
|
|
\texttt{strict\_pq\_implies\_e2e\_pq} proof.
|
|
\item \texttt{StrictE2EPQ/Coverage.lean} carries the 14-path coverage
|
|
theorem (Section~\ref{thm:e2e-coverage}).
|
|
\item \texttt{tla/StrictPQProfile.tla} carries the TLA+ state machine.
|
|
\item \texttt{property/strict\_pq\_test.go} carries the Go property
|
|
tests against \texttt{luxfi/consensus}.
|
|
\end{itemize}
|
|
|
|
\bibliographystyle{plain}
|
|
\begin{thebibliography}{9}
|
|
\bibitem{fips204}
|
|
NIST. \emph{FIPS 204: Module-Lattice-Based Digital Signature Standard}, 2024.
|
|
|
|
\bibitem{dilithium}
|
|
Ducas et al. \emph{CRYSTALS-Dilithium: A Lattice-Based Digital Signature Scheme},
|
|
IACR TCHES, 2018.
|
|
|
|
\bibitem{mlwe}
|
|
Lyubashevsky, Peikert, Regev. \emph{On Ideal Lattices and Learning with Errors
|
|
over Rings}, JACM, 2013.
|
|
|
|
\bibitem{regev2009}
|
|
Regev. \emph{On Lattices, Learning with Errors, Random Linear Codes, and
|
|
Cryptography}, JACM, 2009.
|
|
|
|
\bibitem{dttf2024}
|
|
Anonymous. \emph{Two-Round Threshold Signature from Algebraic One-More
|
|
Learning with Errors}, EUROCRYPT 2024.
|
|
|
|
\bibitem{thresholdraccoon}
|
|
del Pino, Katsumata, Maller, Mouhartem, Prest, Servera. \emph{Threshold
|
|
Raccoon: Practical Threshold Signatures from Standard Lattice Assumptions},
|
|
EUROCRYPT 2024.
|
|
|
|
\bibitem{boschini2024ringtail}
|
|
C. Boschini, D. Kaviani, R. W. F. Lai, G. Malavolta, A. Takahashi and
|
|
M. Tibouchi. \emph{Ringtail: Practical Two-Round Threshold Signatures
|
|
from Learning with Errors}, IEEE S\&P 2025. Cryptology ePrint Archive,
|
|
Paper 2024/1113.
|
|
|
|
\bibitem{lp073}
|
|
Lux Core Team. \emph{LP-073: Pulsar Lattice-Based Threshold Signatures}, 2026.
|
|
\end{thebibliography}
|
|
|
|
\end{document}
|