papers/lux-bridge/sections/12-security-analysis.tex

\section{Security Analysis}

%% +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

\subsection{Threat Model}

\textbf{Adversary Capabilities}:
\begin{itemize}[leftmargin=1.1em]
  \item Can control up to $f < n/3$ validators (Byzantine fault tolerance)
  \item Can delay network messages by up to $\Delta t_{\text{max}}$ (network bound)
  \item Cannot break cryptographic assumptions:
  \begin{itemize}
    \item ECDLP on secp256k1 (128-bit, classical)
    \item co-CDH on BLS12-381 (128-bit, classical)
    \item LWE with $n = 630$, $q = 2^{32}$, $\sigma = 13744$ (128-bit, quantum)
    \item Paillier assumption (128-bit, for CGGMP21 MPC)
  \end{itemize}
\end{itemize}

\subsection{Security Properties}

\begin{theorem}[Bridge Safety]
If the source chain consensus is secure, fraud proof verification is sound, and the MPC threshold is not exceeded (fewer than $t$ nodes compromised), then no invalid cross-chain transfer can finalize.
\end{theorem}

\begin{proof}
Any invalid transfer requires one of:
\begin{enumerate}
  \item An invalid consensus proof, contradicting source chain safety under $f < n/3$ Byzantine assumption.
  \item An undetected fraud proof, contradicting ZK-SNARK soundness (Groth16 knowledge soundness in the generic group model \cite{groth2016size}).
  \item A forged MPC threshold signature, which requires either breaking ECDLP (probability $< 2^{-128}$) or corrupting $\geq t$ of $n$ signers (excluded by assumption).
  \item Bypass of rate limits, which is prevented by the C-01 daily mint limit invariant verified by Halmos symbolic execution.
\end{enumerate}
Since all four attack paths are blocked, no invalid transfer finalizes. \qed
\end{proof}

\begin{theorem}[Liveness]
If at least $2/3$ validators are honest and network delay $< \Delta t_{\text{max}}$, then all valid bridge transactions finalize within the timeout period.
\end{theorem}

\begin{proof}
Honest validators relay proofs within $\Delta t_{\text{max}}$. With $n - f \geq 2n/3$ honest nodes and $t = \lceil 2n/3 \rceil$, the MPC signing protocol completes (honest nodes exceed threshold). The liveness probability is $1 - 2^{-139.6}$ at $n = 100$, $p = 0.999$ (Theorem~\ref{thm:cggmp21-security}). If no fraud proof is submitted within the challenge period, the transaction finalizes. \qed
\end{proof}

\begin{theorem}[Conservation Invariant]
For any bridge token with native chain $A$:
\begin{equation}
\texttt{locked}_A = \sum_{B \neq A} \texttt{minted}_B
\end{equation}
This invariant is maintained across all bridge operations.
\end{theorem}

\begin{proof}
Proven by Halmos symbolic execution (\texttt{check\_bridge\_conservation} in \texttt{HalmosE2E.t.sol}). Each \texttt{bridgeMint(amount)} on chain $B$ is preceded by a verified \texttt{lock(amount)} on chain $A$, with nonce-based replay protection (C-03/C-04 fixes). The Halmos prover verifies that for all symbolic input values, the invariant holds after any sequence of lock/mint/burn/release operations. \qed
\end{proof}

\subsection{Comprehensive Security Summary}

\begin{table}[h]
\centering
\begin{tabular}{llr}
\toprule
\textbf{Attack Vector} & \textbf{Defense} & \textbf{Security Level} \\
\midrule
ECDSA key extraction & secp256k1 ECDLP & 128-bit \\
MPC forgery (CGGMP21) & $t$-of-$n$ threshold + Paillier & 128-bit \\
MPC forgery (FROST) & OMDL in ROM & 128-bit \\
Quantum attack on ECDSA/BLS & Corona (Phase 2+) & 128-bit PQ \\
MPC liveness failure & Binomial: $2^{-139.6}$ & 139.6-bit \\
Unlimited minting (C-01) & Daily mint limits & Halmos-verified \\
Admin key compromise (C-02) & Role separation & Halmos-verified \\
Nonce replay (C-03) & Monotonic counter & Halmos-verified \\
Withdrawal front-run (C-04) & Sequential per-user nonce & Halmos-verified \\
Light client forgery & ZK-SNARK soundness & 128-bit \\
BLS aggregate forgery & co-CDH & 128-bit \\
\bottomrule
\end{tabular}
\caption{Comprehensive security analysis of Lux Bridge}
\end{table}

%% +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++