papers/lux-restaking/sections/11-formal-security-analysis.tex

\section{Formal Security Analysis}

\label{sec:security}
%%==========================================================================

\subsection{Security Properties}

We formally define and prove the following properties of LRP:

\begin{definition}[Safety]
LRP is \emph{safe} if no honest operator loses stake without having committed a
provable violation of a registered slashing condition.
\end{definition}

\begin{definition}[Liveness]
LRP is \emph{live} if all valid slash proofs submitted within the challenge window are
eventually executed.
\end{definition}

\begin{definition}[Stake Coverage]
LRP maintains \emph{stake coverage} if for every service $s$ and every time $t$,
$\Pi_t(s) \geq \text{MinSecurity}(s)$, unless fewer than \texttt{MinOperators}($s$) operators
exist in the system.
\end{definition}

\begin{theorem}[Safety of LRP]
Under the honest majority assumption for the veto committee and the correct implementation
of the Beacon consensus protocol, LRP is safe.
\end{theorem}

\begin{proof}[Proof Sketch]
Honest operators only sign valid blocks and perform valid state transitions by definition.
Slashing requires a proof $\pi$ that demonstrates an invalid operation. Since the veto
committee is honest-majority, at least 5-of-9 members must verify $\pi$ before approving
the slash. A false $\pi$ (accusing an honest operator) cannot pass verification by an
honest veto committee. Hence honest operators are not slashed.
\end{proof}

\begin{theorem}[Liveness of LRP]
Assuming network synchrony with message delay bound $\Delta$ and honest majority of
veto committee members, all valid slash proofs are finalized within
$T_{\text{veto}} + 2\Delta$.
\end{theorem}

\begin{proof}[Proof Sketch]
A valid slash proof is accepted by the slashing module $\Phi_s$ (by validity). The veto
committee, being honest majority, approves within $T_{\text{veto}}$. Network messages are
delivered within $\Delta$. The P-Chain finalizes within one consensus round, bounded by
$\Delta$ under Beacon.
\end{proof}

\subsection{Game-Theoretic Analysis}

We model the operator's decision to restake as a utility maximization problem:

\[
  \max_{\{\alpha_{v,s}\}_s} \sum_s \alpha_{v,s} \cdot w(v) \cdot r_s - \sum_s p_{v,s} \cdot \alpha_{v,s} \cdot w(v) \cdot \bar{f}_s,
\]

subject to $\sum_s \alpha_{v,s} \leq 1$, $\alpha_{v,s} \geq 0$.

This is a linear program in the $\alpha_{v,s}$. The optimal solution is to allocate all
capital to the service $s^* = \arg\max_s (r_s - p_{v,s} \cdot \bar{f}_s)$, unless the
diversification constraints of LRP require spreading across services. This confirms that
the mandatory diversification requirements serve a dual purpose: systemic risk reduction
and incentive compatibility.

%%==========================================================================