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.
42 lines
1.6 KiB
TeX
42 lines
1.6 KiB
TeX
\section{Formal Verification}
|
|
\label{sec:verification}
|
|
%% ===================================================================
|
|
|
|
All critical protocols in the trust kernel have corresponding Lean~4 mechanized
|
|
proofs. The proof modules are organized as follows:
|
|
|
|
\begin{table}[h]
|
|
\centering
|
|
\caption{Lean~4 proof modules for trust kernel properties.}
|
|
\label{tab:proofs}
|
|
\begin{tabular}{lp{7cm}}
|
|
\toprule
|
|
\textbf{Module} & \textbf{Property} \\
|
|
\midrule
|
|
\texttt{Consensus/BFT} & Safety and liveness under $f < n/3$ Byzantine
|
|
validators \\
|
|
\texttt{Crypto/FROST} & Unforgeability of FROST threshold Schnorr
|
|
signatures \\
|
|
\texttt{Crypto/Threshold/CGGMP21} & Threshold ECDSA composition security
|
|
and identifiable abort correctness \\
|
|
\texttt{Trust/Authority} & Trust delegation chain integrity: no capability
|
|
escalation, revocation finality \\
|
|
\bottomrule
|
|
\end{tabular}
|
|
\end{table}
|
|
|
|
\begin{remark}
|
|
The Lean~4 proofs verify the \emph{protocol logic}, not the implementation.
|
|
Implementation correctness is established through the type-safe Go and Rust
|
|
codebases (\texttt{luxfi/frost}, \texttt{luxfi/threshold}, \texttt{luxfi/lattice})
|
|
with property-based testing against the Lean~4 reference specifications.
|
|
\end{remark}
|
|
|
|
The proof of trust delegation integrity (Theorem~\ref{thm:signing-auth}) is
|
|
mechanized in \texttt{Trust/Authority.lean} as follows: the proof establishes
|
|
that the authorization graph is acyclic, that revocation propagates to all
|
|
downstream delegations, and that no delegation chain can exceed the
|
|
capabilities of its root authority.
|
|
|
|
%% ===================================================================
|