papers/lux-trust-kernel/sections/09-security-model.tex

%% ===================================================================
%% LP-134 canonical naming (2025-12-15):
%% Per LP-134 (Lux Chain Topology), T-Chain has been split into:
%%   M-Chain — MPC ceremonies for bridge custody of EXTERNAL wallets
%%             (CGGMP21, FROST, Pulsar-general)
%%   F-Chain — FHE compute + TFHE bootstrap-key generation (encrypted EVM)
%% T-Chain is REMOVED entirely; teleport is B-Chain (bridgevm, LP-6000). No teleportvm.
%% Where this paper says "F-Chain MPC" / "F-Chain threshold governance" /
%% "F-Chain TFHE" / "F-Chain custody", read as M-Chain (MPC) or F-Chain (FHE).
%% ===================================================================

\section{Security Model}
\label{sec:security}
%% ===================================================================

\subsection{Trust Assumptions}

The trust kernel's security rests on the following assumptions:

\begin{enumerate}
    \item \textbf{BFT consensus}: each chain (K, T, M, I) is secured by a
          validator set $V$ with $|V| = n$ and the adversary controls at most
          $f < n/3$ validators. Under this assumption, the chain provides
          safety (no conflicting receipts) and liveness (receipts are eventually
          finalized).
    \item \textbf{Threshold honesty}: for $t$-of-$n$ protocols, at least $t$
          participants are honest. This is strictly weaker than the BFT
          assumption when $t \leq \lfloor n/3 \rfloor + 1$.
    \item \textbf{Cryptographic hardness}: ML-KEM is IND-CCA2 secure under the
          Module-LWE assumption; ML-DSA is EUF-CMA secure under Module-LWE and
          Module-SIS; TFHE is IND-CPA secure under LWE; FROST is EUF-CMA
          secure in the random oracle model under the discrete logarithm
          assumption; CGGMP21 is EUF-CMA secure under the strong RSA and DDH
          assumptions.
    \item \textbf{Capsule integrity}: each capsule correctly implements its
          local encryption and anchoring protocols. A compromised capsule can
          leak its own data but cannot forge receipts or compromise other
          capsules through the trust kernel.
\end{enumerate}

\subsection{BFT Threshold Analysis}

\begin{theorem}[Trust Kernel Safety]\label{thm:safety}
If fewer than $n/3$ validators on each chain are Byzantine, then for any
two receipts $\mathcal{R}_1, \mathcal{R}_2$ with the same
$(\mathsf{chain}, \mathsf{block}, \mathsf{txHash})$, it holds that
$\mathcal{R}_1 = \mathcal{R}_2$.
\end{theorem}

\begin{proof}
This follows directly from the BFT safety property of the underlying consensus
protocol. Two conflicting receipts at the same position would require two
conflicting blocks at the same height, which the BFT consensus prevents
when $f < n/3$. See the mechanized proof in \texttt{Consensus/BFT.lean}
(Section~\ref{sec:verification}).
\end{proof}

\subsection{Post-Quantum Migration Path}

The trust kernel is designed for incremental PQ migration:

\begin{enumerate}
    \item \textbf{Phase 1 (current)}: ML-KEM for key wrapping on K-Chain;
          classical signatures (Ed25519, secp256k1) for transaction signing.
          All wrapped key material is PQ-safe at rest.
    \item \textbf{Phase 2}: ML-DSA for transaction signatures on K-Chain and
          I-Chain. F-Chain and M-Chain retain classical signatures for
          threshold protocol compatibility.
    \item \textbf{Phase 3}: Pulsar (lattice-based threshold signatures)
          replaces FROST on M-Chain, providing full PQ security for threshold
          operations.
\end{enumerate}

Each phase is activated by a governance vote on the F-Chain. The K-Chain's
rotation policy (Definition~\ref{def:rotation}) includes the
$\mathsf{successor\_alg}$ field, enabling per-key migration.

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