mirror of
https://github.com/lux-apps/papers.git
synced 2026-10-30 18:15:21 +00:00
zeekayandHanzo Dev
70f6883235
A July commit removed eight papers on the premise "no license — DEX/non-custodial only". That premise is wrong: Lux operates an ATS, a broker-dealer, a transfer agent and a bank, and this material is resold at lux.financial. The merge that brought main in preserved the removal because the commit stated a reason, which is how a stale reason outlives the fact it rested on. Back, at the versions main carried — main never received the removal, so its copies are the later ones: the ATS architecture, the security-token standard, smart order routing, institutional custody, MPC custody, post-quantum securities, the SSB partnership and the CoinBridge brief. 83 files. Co-authored-by: Hanzo Dev <[email protected]>
22 lines
752 B
TeX
22 lines
752 B
TeX
\section{Formal Verification}
|
|
|
|
\label{sec:formal}
|
|
%% =====================================================================
|
|
|
|
The post-quantum precompiles are formally verified in the
|
|
\texttt{lux/proofs} repository:
|
|
|
|
\begin{itemize}[nosep]
|
|
\item \texttt{Crypto.MLDSA}: correctness and EUF-CMA security model.
|
|
\item \texttt{Crypto.MLKEM}: IND-CCA2 security model, decapsulation
|
|
correctness.
|
|
\item \texttt{Crypto.SLHDSA}: hash-based security reduction,
|
|
statelessness.
|
|
\item \texttt{Crypto.Hybrid}: best-of-both-worlds composition
|
|
theorem.
|
|
\item \texttt{Crypto.Pulsar}: lattice-based threshold signatures
|
|
for post-quantum MPC.
|
|
\end{itemize}
|
|
|
|
%% =====================================================================
|