mirror of
https://github.com/lux-apps/papers.git
synced 2026-10-30 18:15:21 +00:00
zooqueen
a1f77cacc9
Ringtail (Boschini et al., ePrint 2024/1113) is third-party prior art; Lux's Corona (Ring-LWE = Module-LWE rank-1) builds on it; Pulsar is Module-LWE rank-k. Retired the conflated boschini2024corona/corona2024/coronago/... bib keys to the single canonical ringtail/corona/pulsar/magnetar keys, rewrote \cite + \bibitem by context, and fixed 'Pulsar (Ring-LWE)' mislabels (Corona where corona.metal/ single-ring/Ringtail-derived; Pulsar where Module-LWE rank-k/ML-DSA). Cryptographer-led.
47 lines
2.1 KiB
TeX
47 lines
2.1 KiB
TeX
\section{Formal Verification}
|
|
|
|
\label{sec:formal}
|
|
%% ============================================================================
|
|
|
|
The safety, liveness, replay-impossibility, and unforgeability theorems
|
|
are machine-checked in Lean~4. The protocol's resistance to network-level
|
|
attacks (replay, reflection, MITM) is verified in Tamarin.
|
|
|
|
\begin{table}[ht]
|
|
\centering
|
|
\small
|
|
\begin{tabular}{@{}lll@{}}
|
|
\toprule
|
|
\textbf{Property} & \textbf{Tool} & \textbf{File} \\
|
|
\midrule
|
|
Safety (Thm.~\ref{thm:safety}) & Lean~4 & \texttt{Quasar.lean} \\
|
|
Liveness (Thm.~\ref{thm:liveness}) & Lean~4 & \texttt{BFT.lean} \\
|
|
Replay impossibility (Thm.~\ref{thm:replay-impossible})
|
|
& Lean~4 & \texttt{Subject.lean} \\
|
|
BLS unforgeability & Lean~4 & \texttt{BLS.lean} \\
|
|
Corona EUF-CMA & Lean~4 & \texttt{Corona.lean} \\
|
|
ML-DSA-65 EUF-CMA & Lean~4 & \texttt{MLDSA.lean} \\
|
|
Groth16 knowledge-soundness & Lean~4 & \texttt{Groth16.lean} \\
|
|
QuasarCert unforgeability (Thm.~\ref{thm:unforgeability})
|
|
& Lean~4 & \texttt{Quasar.lean} \\
|
|
QuasarCert soundness (Thm.~\ref{thm:qcert-sound})
|
|
& Lean~4 & \texttt{QuasarCert.lean} \\
|
|
Protocol authentication & Tamarin & \texttt{QuasarConsensus.spthy} \\
|
|
Replay resistance (network) & Tamarin & \texttt{QuasarConsensus.spthy} \\
|
|
\bottomrule
|
|
\end{tabular}
|
|
\caption{Formal-verification artifacts shipped with the 25 December 2025
|
|
release. Lean~4 proofs compile against \texttt{[email protected]}; Tamarin
|
|
runs against version 1.8.0.}
|
|
\label{tab:formal}
|
|
\end{table}
|
|
|
|
The Lean development imports Module-LWE and ML-DSA assumptions as
|
|
axioms; QuasarCert soundness is then derived constructively. The
|
|
companion proof sketch~\cite{qcert-proof} (Appendices A--E) provides
|
|
the human-readable argument and the concrete-quantum security
|
|
parameters used to discharge the axioms numerically.
|
|
|
|
|
|
%% ============================================================================
|