mirror of
https://github.com/lux-apps/papers.git
synced 2026-10-30 18:15:21 +00:00
zeekay
4a753bb639
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.
22 lines
883 B
TeX
22 lines
883 B
TeX
\section{Formal Verification}
|
|
|
|
\label{sec:formal}
|
|
%% =====================================================================
|
|
|
|
The core properties are mechanized in Lean~4:
|
|
|
|
\begin{itemize}[nosep]
|
|
\item \texttt{Crypto.Threshold.CGGMP21}: keygen correctness,
|
|
identifiable abort, presignature one-time use, offline/online
|
|
separation, key never reconstructed.
|
|
\item \texttt{Crypto.FROST}: correctness, unforgeability, robustness,
|
|
majority threshold safety, share refresh.
|
|
\item \texttt{Crypto.Threshold.Reshare}: public key preservation,
|
|
old share invalidation, threshold maintenance, no key
|
|
reconstruction, Byzantine safety.
|
|
\item \texttt{Crypto.NonCustodial}: 2-of-3 non-custodial guarantee,
|
|
liveness (any 2 can sign), single-party impotence.
|
|
\end{itemize}
|
|
|
|
%% =====================================================================
|