papers/lux-warp-messaging/sections/04-security-analysis.tex

\section{Security Analysis}
\label{sec:security}

\subsection{Threat Model}

We consider a Byzantine adversary $\mathcal{A}$ controlling validators with total stake $W_{\mathcal{A}} < W/3$ on the source appchain. The adversary may:
\begin{enumerate}
    \item Produce arbitrary signatures with compromised keys.
    \item Delay, reorder, or drop relay messages (asynchronous network).
    \item Attempt rogue-key attacks during key registration.
    \item Collude across appchains (cross-chain adversary).
\end{enumerate}

\subsection{Rogue Key Prevention}

\begin{definition}[Proof of Possession (PoP)]
At registration, validator $v_i$ provides $\pi_i = \mathsf{sk}_i \cdot g_1 \in \mathbb{G}_1$. Verification: $e(\pi_i, g_2) = e(g_1, \mathsf{pk}_i)$.
\end{definition}

\begin{lemma}[\cite{ristenpart2007power}]
With PoP, same-message BLS aggregate signatures resist rogue-key attacks: no adversary can choose $\mathsf{pk}_{\mathcal{A}}$ to cancel honest contributions in the aggregate.
\end{lemma}

\subsection{Message Authenticity}

\begin{theorem}[Authenticity]\label{thm:auth}
Under co-CDH on BLS12-381 and $W_{\mathcal{A}} < W/3$, no PPT adversary can produce a valid proof $\Pi$ for a message $\mathcal{M}$ not finalized on the source appchain, except with probability $\mathsf{negl}(\lambda)$.
\end{theorem}

\begin{proof}
Suppose $\Pi = (\sigma_{\text{agg}}, \mathsf{bm})$ verifies for $\mathcal{M}$ not in any finalized block. Let $\mathcal{Q}$ be the signers indicated by $\mathsf{bm}$, with $W_q \geq 2W/3$. Since $W_{\mathcal{A}} < W/3$, there exists an honest validator $j \in \mathcal{Q}$ contributing weight $w_j > 0$.

By Algorithm~\ref{alg:signing}, honest $j$ never signed $\mathcal{M}$. For $\sigma_{\text{agg}}$ to verify under $\mathsf{apk} = \sum_{i \in \mathcal{Q}} \mathsf{pk}_i$, define $\sigma_j^* = \sigma_{\text{agg}} - \sum_{i \in \mathcal{Q} \setminus \{j\}} \sigma_i$. Then $\sigma_j^*$ is a valid BLS signature by $j$ on $d(\mathcal{M})$, constituting an existential forgery. This contradicts co-CDH security of BLS.
\end{proof}

\subsection{Liveness}

\begin{theorem}[Liveness]\label{thm:liveness}
If honest validators with total weight $\geq 2W/3$ are online and the network delivers messages within bounded delay $\Delta$, then every emitted warp message is relayed to the destination within $3\Delta + O(1)$ time.
\end{theorem}

\begin{proof}
Honest validators sign within one consensus round after finalization ($\leq \Delta$). Relayer collects signatures within $\Delta$ of broadcast. Submission to destination occurs within $\Delta$. Total: $3\Delta$ plus constant computation time for aggregation and verification.
\end{proof}

\subsection{Replay Protection}

Per-pair nonces (Algorithm~\ref{alg:verification}, line 8) prevent replay: each $(\mathsf{src}, \mathsf{dst})$ pair maintains a monotonic counter, and the destination rejects any message whose nonce does not match the expected next value.

\begin{lemma}[No Replay]
A message $\mathcal{M}$ with nonce $k$ accepted on the destination at nonce counter $k$ cannot be replayed, since the counter advances to $k+1$ upon acceptance.
\end{lemma}