papers/lux-privacy-pool/sections/06-security-analysis.tex

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

\subsection{Soundness}

\begin{theorem}[Soundness]
No computationally bounded adversary can withdraw tokens without a corresponding valid deposit, except with probability $\mathsf{negl}(\lambda)$.
\end{theorem}

\begin{proof}
The Groth16 proof system is computationally sound under the $q$-power Knowledge of Exponent (KoE) assumption \cite{groth2016size}. The circuit enforces that the prover knows a leaf in the Merkle tree with root $R$. Since $R$ is the actual pool root and Poseidon is collision-resistant, the leaf must correspond to an actual deposit. The nullifier prevents reuse.
\end{proof}

\subsection{Zero-Knowledge}

\begin{theorem}[Privacy]
The withdrawal transaction reveals no information about the depositor beyond:
\begin{enumerate}
    \item The withdrawal amount $v$ (from the fixed denomination).
    \item Membership in association set $\mathcal{A}$ (from the ASP choice).
\end{enumerate}
In particular, the specific deposit corresponding to the withdrawal is computationally indistinguishable from any other deposit of the same denomination in $\mathcal{A}$.
\end{theorem}

\begin{proof}
Groth16 satisfies perfect zero-knowledge: the proof can be simulated without knowledge of the witness. The public inputs $(R, R_{\mathcal{A}}, \mathsf{nf}, \mathsf{recipient}, v)$ reveal only the pool root, association set, nullifier, recipient, and amount. The nullifier is a PRF output (Poseidon) and reveals no information about $\mathsf{sk}$ or $\mathsf{leafIndex}$. The recipient address is chosen by the withdrawer and is unlinkable to the depositor's address.
\end{proof}

\subsection{Double-Spend Prevention}

\begin{lemma}[No Double-Spend]
Each deposit can be withdrawn at most once.
\end{lemma}

\begin{proof}
Each deposit has a unique nullifier $\mathsf{nf} = H_{\text{null}}(\mathsf{sk}, \mathsf{leafIndex})$. The contract maintains a set of spent nullifiers. A second withdrawal attempt would produce the same $\mathsf{nf}$ (since $\mathsf{sk}$ and $\mathsf{leafIndex}$ are fixed), which the contract rejects.
\end{proof}

\subsection{Anonymity Set Size}

\begin{definition}[Effective Anonymity Set]
The effective anonymity set for a withdrawal from association set $\mathcal{A}$ at denomination $v$ is:
\begin{equation}
    k_{\text{eff}} = |\{i \in \mathcal{A} : v_i = v \text{ and } \mathsf{nf}_i \text{ not spent}\}|
\end{equation}
\end{definition}

\begin{proposition}[Privacy Level]
The probability of correctly linking a withdrawal to its deposit is at most $1/k_{\text{eff}}$ for a computationally bounded adversary without the depositor's secret key.
\end{proposition}

\begin{table}[H]
\centering
\caption{Expected anonymity set sizes by denomination and ASP type (at 100K total deposits).}
\label{tab:anonymity}
\begin{tabular}{lrrrrr}
\toprule
\textbf{ASP Type} & \textbf{0.1 LUX} & \textbf{1 LUX} & \textbf{10 LUX} & \textbf{100 LUX} & \textbf{1000 LUX} \\
\midrule
Permissive & 25,000 & 30,000 & 20,000 & 15,000 & 5,000 \\
Moderate & 22,000 & 27,000 & 18,000 & 13,000 & 4,500 \\
Strict & 7,000 & 9,000 & 6,000 & 4,000 & 1,500 \\
\bottomrule
\end{tabular}
\end{table}