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.
22 lines
869 B
TeX
22 lines
869 B
TeX
\section{Formal Verification}
|
|
|
|
\label{sec:formal}
|
|
%% =====================================================================
|
|
|
|
The core properties are mechanized in Lean~4 in the
|
|
\texttt{lux/proofs} repository:
|
|
|
|
\begin{itemize}[nosep]
|
|
\item \texttt{Crypto.FHE.TFHE}: correctness of encryption/decryption,
|
|
homomorphic gate correctness, noise growth bounds, bootstrapping
|
|
preservation.
|
|
\item \texttt{Crypto.Threshold.LSS}: Shamir sharing correctness,
|
|
privacy, linearity, composability.
|
|
\item \texttt{Crypto.Threshold.Composition}: uniform access structure
|
|
across TFHE threshold decryption, FROST, and CGGMP21.
|
|
\item \texttt{Crypto.ThresholdDecrypt}: combined proof that $t$
|
|
shares reconstruct correctly and $t{-}1$ shares reveal nothing.
|
|
\end{itemize}
|
|
|
|
%% =====================================================================
|