papers/lux-threshold-mpc/sections/11-formal-security-proofs.tex

\section{Formal Security Proofs}

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

We state the main security theorems with full proof structure. Formal machine-checked
proofs in Lean 4 are available at
\texttt{github.com/luxfi/proofs/tree/main/lean/Crypto}.

\subsection{FROST Unforgeability (Full Proof)}

\begin{theorem}[FROST-UF]
\label{thm:frost-uf-full}
Let $\mathsf{FROST}$ be the $(t,n)$-threshold Schnorr signature scheme over group
$\mathbb{G}$ of order $q$. For any PPT adversary $\mathcal{A}$ making at most $q_s$
signing queries and $q_H$ random oracle queries, and corrupting at most $t-1$ parties:
\[
  \mathsf{Adv}^{\mathsf{uf}}_{\mathsf{FROST}}(\mathcal{A}) \leq
    \frac{q_H + q_s + 1}{q} + \sqrt{\frac{q_H}{q}} +
    \mathsf{Adv}^{\mathsf{dl}}_{\mathbb{G}}(\mathcal{B})
\]
where $\mathcal{B}$ is a DLP solver with runtime polynomial in the runtime of
$\mathcal{A}$.
\end{theorem}

\begin{proof}
We construct a sequence of games:

\textbf{Game 0.} Real FROST experiment with $t-1$ corrupted parties. $\mathcal{A}$
receives the public key $Y$, the corrupted shares $\{s_i\}_{i \in C}$, and access
to a signing oracle.

\textbf{Game 1.} Replace the random oracle $H_2$ with a programmable random oracle.
The reduction $\mathcal{R}$ programs responses to be consistent. This is a syntactic
change; $|\Pr[G_1] - \Pr[G_0]| = 0$.

\textbf{Game 2.} $\mathcal{R}$ receives DLP challenge $Y^* = x^* \cdot G$ and
embeds it as the honest party's public key share. Specifically, $\mathcal{R}$ sets
$Y_h = Y^* - \sum_{i \in C} \lambda_{i,S}^{-1} \cdot s_i \cdot G$ where $h$ is
the simulated honest party. $\mathcal{R}$ does not know $s_h$ but can simulate
signing by programming $H_2$ to produce challenges $c$ such that the honest party's
response $z_h$ can be computed from the random oracle output. This requires
$\mathcal{R}$ to know $c$ before committing to $R$, which is possible because
$\mathcal{R}$ programs $H_2$. $|\Pr[G_2] - \Pr[G_1]| \leq (q_H + q_s)/q$ due
to potential programming conflicts.

\textbf{Game 3 (Extraction).} When $\mathcal{A}$ outputs forgery $(m^*, (R^*, z^*))$
on an unqueried message, $\mathcal{R}$ applies the generalized forking
lemma~\cite{bellare2006}: rewind $\mathcal{A}$ with a different random oracle
response at the forgery point to obtain a second forgery $(m^*, (R^*, z^{*\prime}))$
with challenge $c' \neq c$. From $z^* - z^{*\prime} = (c - c') \cdot x^*$,
$\mathcal{R}$ recovers $x^* = (z^* - z^{*\prime}) / (c - c')$, solving DLP.

The forking probability is at least $(\epsilon - (q_H+1)/q)^2 / q_H$ where $\epsilon$
is $\mathcal{A}$'s advantage, giving the stated bound after rearrangement.
\end{proof}

\subsection{CGGMP21 Identifiable Abort}

\begin{theorem}[CGGMP21 Identifiable Abort]
\label{thm:cggmp-ia}
If the CGGMP21 signing protocol fails to produce a valid signature, the honest parties
can identify at least one malicious party with probability $\geq 1 - \mathsf{negl}(\lambda)$.
\end{theorem}

\begin{proof}
The identification mechanism works as follows. In the presigning phase, each party $i$
commits to its nonce share $k_i$ via $K_i = k_i \cdot G$ with a zero-knowledge proof
$\Pi_{\mathsf{enc}}$ of correct encryption. In the MtA sub-protocol, each party proves
correct computation via $\Pi_{\mathsf{aff-g}}$. In online signing, each party $i$
broadcasts $\sigma_i$ with a proof $\Pi_{\mathsf{log*}}$ that $\sigma_i$ is consistent
with its committed values $(k_i, \chi_i)$.

If $s = \sum_i \sigma_i$ does not yield a valid ECDSA signature, at least one $\sigma_i$
is inconsistent. The $\Pi_{\mathsf{log*}}$ proof for that party will fail verification,
identifying the malicious party. Soundness of $\Pi_{\mathsf{log*}}$ ensures that an
honest party's proof always verifies, so only a malicious party can be identified.

Formally: let $E$ be the event that signing fails. Conditioned on $E$, the probability
that all $\Pi_{\mathsf{log*}}$ proofs verify is bounded by the soundness error of
$\Pi_{\mathsf{log*}}$, which is $\mathsf{negl}(\lambda)$. Therefore, with probability
$\geq 1 - \mathsf{negl}(\lambda)$, at least one malicious party's proof fails.
\end{proof}

\subsection{Key Refresh Forward Security}

\begin{theorem}[Forward Security under Proactive Refresh]
\label{thm:forward}
With key refresh every $\Delta$ time units, an adversary who compromises $t-1$ shares
in any single epoch cannot forge signatures for other epochs, even if the adversary
later compromises $t-1$ different shares in a subsequent epoch.
\end{theorem}

\begin{proof}
Let $\{s_i^{(e)}\}$ and $\{s_i^{(e+1)}\}$ denote shares in epochs $e$ and $e+1$.
The adversary knows $\{s_i^{(e)}\}_{i \in C_e}$ and $\{s_j^{(e+1)}\}_{j \in C_{e+1}}$
with $|C_e| = |C_{e+1}| = t-1$.

Shares are related by $s_i^{(e+1)} = s_i^{(e)} + \sum_j g_j(i)$ where $g_j$ are
degree-$(t-1)$ polynomials with $g_j(0) = 0$. The adversary can compute
$s_i^{(e+1)} - s_i^{(e)} = \sum_j g_j(i)$ for indices in $C_e \cap C_{e+1}$.
However, $\sum_j g_j$ is a degree-$(t-1)$ polynomial with known zero constant term,
determined by $t-1$ coefficients. Even if $|C_e \cap C_{e+1}| = t-2$ (maximum overlap
given $|C_e| = |C_{e+1}| = t-1$ and $n \geq t+1$), the adversary obtains $t-2$ points
on a degree-$(t-1)$ polynomial plus the constraint $g(0) = 0$, giving $t-1$
constraints on $t-1$ unknowns. This determines $g$ uniquely, allowing the adversary
to convert shares across epochs.

However, this requires $C_e$ and $C_{e+1}$ to overlap in $t-2$ indices. If the signer
set has $n \geq 2t$, a mobile adversary corrupting $t-1$ parties per epoch with
$|C_e \cap C_{e+1}| \leq t-2$ still cannot reconstruct $s$: the adversary has at most
$t-1$ independent share values per epoch, which is information-theoretically
insufficient for a degree-$(t-1)$ polynomial.

The forward security guarantee holds provided the adversary does not corrupt the same
$t-1$ parties across two consecutive epochs and the honest parties' refresh polynomials
remain secret.
\end{proof}

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