Files
papers/lux-teleport-protocol/sections/07-security-analysis.tex
zeekay 4a753bb639 papers: reorganize into per-paper dirs, add Antje Worring as co-author
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.
2026-04-18 21:50:07 -07:00

61 lines
2.3 KiB
TeX

\section{Security Analysis}
\label{sec:security}
\subsection{Threat Model}
We consider adversaries who may:
\begin{enumerate}
\item Control $< 1/3$ of Lux validator stake.
\item Control relayer nodes (delay, censor, or forge relay messages).
\item Exploit vulnerabilities in light client contracts.
\item Attempt double-spend across chains.
\end{enumerate}
\subsection{Double-Spend Prevention}
\begin{theorem}[No Double-Spend]
An adversary cannot spend the same tokens on both the source and destination chains simultaneously, provided:
\begin{enumerate}
\item The source chain lock is verified before the destination mint.
\item Nonces prevent replay of lock proofs.
\item The source chain's consensus is safe ($< 1/3$ Byzantine).
\end{enumerate}
\end{theorem}
\begin{proof}
Suppose the adversary locks $n$ tokens on the source, obtains a mint of $n$ wrapped tokens on the destination, and then attempts to unlock the original $n$ tokens. The unlock requires either: (a) a burn proof from the destination (which the adversary has not produced, since they want to keep both), or (b) expiry of the HTLC timeout (which returns tokens but burns the destination mint). In neither case does the adversary hold $n$ tokens on both chains.
\end{proof}
\subsection{Light Client Trust Assumptions}
\begin{table}[H]
\centering
\caption{Trust assumptions for different transfer modes.}
\label{tab:trust}
\begin{tabular}{p{3.5cm}p{4cm}p{4cm}}
\toprule
\textbf{Mode} & \textbf{Trust Assumption} & \textbf{Attack Threshold} \\
\midrule
Intra-Lux (Warp) & $2/3$ source appchain stake & $> 1/3$ appchain stake \\
Lux $\to$ Ethereum (LC) & $2/3$ Lux stake + ETH LC & $> 1/3$ Lux stake \\
Ethereum $\to$ Lux (LC) & Sync committee honest & $> 1/3$ sync committee \\
SNARK-based & Co-CDH + SNARK soundness & Quantum or SNARK break \\
\bottomrule
\end{tabular}
\end{table}
\subsection{Bridge Invariants}
\begin{definition}[Conservation Invariant]
For any token $\mathsf{tok}$ with native chain $A$:
\begin{equation}
\text{locked}_A(\mathsf{tok}) = \sum_{B \neq A} \text{minted}_B(\mathsf{tok})
\end{equation}
Tokens locked on the native chain exactly equal wrapped tokens across all destination chains.
\end{definition}
\begin{lemma}[Conservation Under Normal Operation]
The conservation invariant holds after every successful transfer (lock-and-mint or burn-and-release).
\end{lemma}