mirror of
https://github.com/lux-apps/papers.git
synced 2026-10-30 18:15:21 +00:00
zeekay
abf99d05fc
Restructured from flat .tex/.pdf files into per-paper subdirectories. Added Antje Worring as co-author on all papers. Synced PDFs to pdfs/ for download site.
15 lines
837 B
TeX
15 lines
837 B
TeX
\section{Formal Verification Status}
|
|
\label{sec:formal}
|
|
|
|
The core LWM protocol has been formally verified using the Tamarin prover for the following properties:
|
|
|
|
\begin{enumerate}
|
|
\item \textbf{Authentication}: A valid proof $\Pi$ implies the message was signed by a quorum of source validators.
|
|
\item \textbf{Non-repudiation}: A validator who signed cannot deny signing (signatures are publicly verifiable).
|
|
\item \textbf{Replay prevention}: Each message is delivered exactly once on the destination.
|
|
\item \textbf{Ordering}: FIFO ordering holds for same-pair messages.
|
|
\end{enumerate}
|
|
|
|
The BLS signature security reduces to co-CDH, which has been extensively analyzed in the cryptographic literature. The pairing-based verification is implemented using the audited \texttt{blst} library with constant-time operations.
|
|
|