\documentclass[11pt,a4paper]{article}

% --- Packages ---
% inputenc unnecessary with LaTeX 2018+ (UTF-8 is default)
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{enumitem}
\usepackage{booktabs}
\usepackage{array}
\usepackage{tabularx}
\usepackage{hyperref}
\usepackage{cleveref}
\usepackage{xcolor}
\usepackage{graphicx}
\usepackage{microtype}
\usepackage{float}
\usepackage[nottoc]{tocbibind}
\usepackage{xspace}
\usepackage{tikz}
\usetikzlibrary{positioning}

% --- Theorem environments ---
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{remark}{Remark}
\newtheorem*{claim}{Claim}  % unnumbered — does not consume theorem counter

\newenvironment{proofsketch}
  {\noindent\textit{Proof sketch.}\space}
  {\hfill$\lrcorner$\medskip}

% --- Shorthands ---
\newcommand{\ie}{i.e.,\xspace}
\newcommand{\eg}{e.g.,\xspace}
\newcommand{\cf}{cf.\xspace}
\newcommand{\etal}{et~al.\xspace}
\newcommand{\Adv}{\mathsf{Adv}}
\newcommand{\KDF}{\mathsf{KDF}}
\newcommand{\MAC}{\mathsf{MAC}}
\newcommand{\HKDF}{\mathsf{HKDF}}
\newcommand{\AEAD}{\mathsf{AEAD}}
\newcommand{\Enc}{\mathsf{Enc}}
\newcommand{\Dec}{\mathsf{Dec}}
\newcommand{\Encaps}{\mathsf{Encaps}}
\newcommand{\Decaps}{\mathsf{Decaps}}
\newcommand{\KeyGen}{\mathsf{KeyGen}}
\newcommand{\Sign}{\mathsf{Sign}}
\newcommand{\Verify}{\mathsf{Verify}}
\newcommand{\pk}{\mathit{pk}}
\newcommand{\sk}{\mathit{sk}}
\newcommand{\rk}{\mathit{rk}}
\newcommand{\ek}{\mathit{ek}}
\newcommand{\mk}{\mathit{mk}}
% \xmark removed — was unused

% --- Spacing fix for overfull hboxes ---
\emergencystretch=2em
\hypersetup{
    colorlinks=true,
    linkcolor=blue!60!black,
    citecolor=blue!60!black,
    urlcolor=blue!60!black,
}

% --- Title ---
\title{Soliton: A Formally Verified Post-Quantum Messaging Protocol\\with Hybrid Authentication}

\author{Kamal Tufekcic\\[4pt]
\small Independent Researcher, Romania\\[2pt]
\small \texttt{kamal@lo.sh}\\[2pt]
\small \url{https://git.lo.sh/lo/libsoliton}}

\date{}

\begin{document}
\maketitle

% ============================================================================
% ABSTRACT
% ============================================================================
\begin{abstract}
I present Soliton, a two-party end-to-end encrypted communication protocol
providing hybrid classical/post-quantum security for messaging, voice and
video calls, and file transfer. The protocol comprises five sub-protocols ---
LO-KEX (asynchronous session establishment), LO-Ratchet (ongoing message
encryption), LO-Auth (server-side key possession proof), LO-Call (call key
derivation), and LO-Stream (streaming AEAD with random-access decryption) ---
built from X-Wing (X25519 + ML-KEM-768), hybrid Ed25519 + ML-DSA-65
signatures, HKDF-SHA3-256, and XChaCha20-Poly1305. The ratchet uses
counter-mode message key derivation ($\mk_i = \mathsf{PRF}(\ek, i)$),
enabling $O(1)$ out-of-order decryption without a skip cache. No existing
asynchronous two-party E2EE messaging protocol provides post-quantum
authentication alongside post-quantum key exchange and ratcheting ---
prior work (PQXDH, SPQR, PQ3) retains classical-only signatures.
I provide formal verification via 55~Tamarin lemmas across 8~symbolic
models and 7~CryptoVerif queries across 5~computational models, covering
13~security properties (12~theorems and 1~unverified claim) with
concrete security bounds. The reference implementation
is a pure Rust library requiring no C~toolchain, benchmarked on x86-64,
aarch64, and riscv64gc, with 574.6~billion fuzz executions across
36~targets yielding zero crashes. The full specification, formal models,
and implementation are published under AGPL-3.0 at
\url{https://git.lo.sh/lo/libsoliton} for independent review.
\end{abstract}

\smallskip\noindent\textbf{Keywords:}
post-quantum cryptography, secure messaging, KEM-based ratchet, hybrid
signatures, formal verification, X-Wing, ML-DSA-65

\tableofcontents
\newpage

% ============================================================================
% 1. INTRODUCTION
% ============================================================================
\section{Introduction}\label{sec:intro}

\subsection{Motivation}\label{sec:motivation}

The prospect of cryptographically relevant quantum computers poses an
existential threat to the confidentiality assumptions underlying every
deployed messaging protocol. The harvest-now-decrypt-later attack model ---
where an adversary records encrypted traffic today and decrypts it once
quantum hardware matures --- makes the post-quantum transition urgent for
any system handling sensitive communications, even if large-scale quantum
computers remain years away.

The messaging ecosystem has begun to respond. Signal introduced
PQXDH~\cite{signal-pqxdh} in 2023, adding an ML-KEM encapsulation to the
X3DH handshake while retaining the classical Diffie-Hellman double ratchet
for ongoing messages. Apple deployed PQ3~\cite{apple-pq3} in 2024 with
periodic KEM rekeying alongside per-message ECDH. Signal subsequently
introduced the Sparse Post-Quantum Ratchet
(SPQR)~\cite{signal-spqr}, based on the Triple Ratchet construction of
Dodis \etal~\cite{djkps25}, running an ML-KEM-based ratchet in parallel
with the existing
double ratchet. These are significant engineering achievements, but they
share a common gap: \textbf{none provide post-quantum authentication}. In
every deployed system, the signature scheme used to authenticate session
establishment remains classical --- Ed25519 or ECDSA --- and is therefore
vulnerable to quantum forgery. Signal has explicitly acknowledged this as an
open problem~\cite{signal-spqr}.

Soliton was not designed to fill this gap in the abstract. It was designed
because I needed it. I am building a messaging platform with stringent
privacy and security requirements, and I needed an end-to-end encryption
layer that met several practical constraints: no C~toolchain dependency
(to avoid cross-compilation complexity across target platforms), no
architectural lock-in (the library should be a ``byte pump'' --- plaintext
in, ciphertext out, with no opinions about transport, storage, or session
management), and hybrid post-quantum security at every layer, including
authentication. No existing library met all of these requirements.
\texttt{libsignal} is functionally coupled to Signal's architecture.
Academic PQ~messaging proposals exist~\cite{hks22, bfg20, acd19} but lack
production implementations. The available options were to compromise on
requirements or build something new.

The protocol design itself is a product of a single guiding principle:
\emph{keep it simple}. Where the standard double ratchet derives message
keys via an iterated HMAC chain (requiring a skip cache for out-of-order
decryption), Soliton uses counter-mode derivation
$\mk_i = \MAC(\ek, \texttt{0x01} \| \mathsf{BE32}(i))$,
enabling $O(1)$~random-access decryption with no additional state. Where
Signal runs two independent ratchets in parallel (classical DH and
post-quantum KEM) and combines their outputs, Soliton uses X-Wing --- a
hybrid KEM that inherently combines X25519 and ML-KEM-768 in every
operation --- as a single ratchet primitive, making the classical ratchet
redundant. Where Signal defers post-quantum authentication, Soliton signs
session initiations with a composite Ed25519 + ML-DSA-65 scheme from the
start. Each of these decisions reduces the protocol's complexity at the
cost of different trade-offs, discussed in \Cref{sec:rationale}.

\subsection{Contributions}\label{sec:contributions}

The primary contribution of this work is not any single protocol
component in isolation --- adding post-quantum signatures to a KEM-based
handshake is a natural instantiation choice, and the individual
sub-protocols build on well-established foundations. Rather, the
contribution is the \textbf{comprehensive, verified, and implemented
package}: a complete messaging protocol with hybrid PQ security at every
layer (including authentication), formal verification covering the full
protocol lifecycle, and a production-quality implementation. No prior
work combines all three.

Specifically:

\begin{enumerate}[leftmargin=*, itemsep=4pt]
\item \textbf{LO-KEX with hybrid PQ authentication}: An asynchronous
  KEM-based session establishment protocol using X-Wing, with hybrid
  Ed25519 + ML-DSA-65 authentication. No deployed or published
  asynchronous two-party E2EE messaging protocol provides post-quantum
  authentication: Signal's PQXDH~\cite{signal-pqxdh} and
  SPQR~\cite{signal-spqr} retain Ed25519-only signatures; Apple's
  PQ3~\cite{apple-pq3} uses ECDSA. Hashimoto \etal~\cite{hks22}
  provide a generic PQ~X3DH framework that could be instantiated with
  PQ signatures, but do not instantiate one, and provide neither an
  implementation nor formal verification of such an instantiation.

\item \textbf{LO-Ratchet}: A KEM-based double ratchet with counter-mode
  message key derivation ($\mk_i = \mathsf{PRF}(\ek, i)$), enabling
  $O(1)$ out-of-order decryption without a skip cache --- providing
  per-epoch forward secrecy and post-compromise security via X-Wing KEM
  ratchet steps.

\item \textbf{LO-Auth}: A KEM-based key possession proof for server-side
  authentication, compositionally secure with LO-KEX under shared
  identity keys.

\item \textbf{LO-Call}: Ephemeral KEM-based call key derivation for E2EE
  voice and video, with intra-call forward secrecy and independence from
  ratchet state.

\item \textbf{LO-Stream}: A streaming AEAD construction with both
  sequential and random-access interfaces, providing chunked encryption
  with ordering, truncation resistance, and cross-stream isolation
  guarantees.

\item \textbf{Formal verification}: 55~Tamarin lemmas across 8~symbolic
  models and 7~CryptoVerif queries across 5~computational models,
  covering 13~security properties with concrete security bounds. For comparison:
  the PQXDH verification~\cite{bjks24} covers the handshake only
  (${\sim}6$--8 properties); the PQ3 analysis~\cite{lsb25} covers
  handshake and ratcheting (${\sim}15$--30 lemmas); B\'eguinet
  \etal~\cite{bcrs24} cover a KEM-based Signal variant
  (${\sim}8$--10~properties). No prior work combines both Tamarin
  and CryptoVerif for a KEM-based messaging protocol covering
  handshake, ratcheting, authentication, calls, and streaming.

\item \textbf{Implementation}: A pure Rust library (\texttt{libsoliton})
  with C, Python, WASM, and Zig bindings, benchmarked across three
  architectures, with 574.6~billion fuzz executions across 36~targets
  yielding zero crashes.
\end{enumerate}

\paragraph{AI-assisted development.}
AI assistance (Anthropic's Claude) was used extensively throughout
protocol design, specification writing, and formal model development.
All formal verification results are machine-checkable and independently
reproducible --- the Tamarin and CryptoVerif models are published
alongside the paper. Model fidelity was validated through systematic
cross-referencing against both the specification and the Rust
implementation, including 10~expected-falsification tests confirming
the models correctly represent known attack paths. The paper itself
underwent multiple rounds of automated cross-validation (checking claims
against the specification, formal analysis document, implementation
source, and verification outputs) to identify factual discrepancies
before submission. Readers are encouraged to verify rather than trust.

\subsection{Paper organization}

\Cref{sec:prelim} introduces notation and primitive assumptions.
\Cref{sec:protocol} describes the five sub-protocols.
\Cref{sec:security-model} defines the adversary model and freshness
predicates. \Cref{sec:security} presents the 13~security theorems with
proof sketches and concrete bounds. \Cref{sec:verification} details the
Tamarin and CryptoVerif verification results.
\Cref{sec:implementation} covers the Rust implementation, benchmarks, and
testing. \Cref{sec:rationale} discusses key design decisions and their
trade-offs. \Cref{sec:related} surveys related work.
\Cref{sec:limitations} identifies verification gaps and open problems.
\Cref{sec:conclusion} concludes.

The full cryptographic specification (5000+ lines), formal analysis
document, and all Tamarin/CryptoVerif models are available in the project
repository~\cite{soliton-repo}. The specification targets independent
reimplementation; the formal analysis document targets formal methods
researchers. This paper presents the protocol design, security arguments,
and verification results at a level suitable for a cryptographic audience
without duplicating the companion documents.

% ============================================================================
% 2. PRELIMINARIES
% ============================================================================
\section{Preliminaries}\label{sec:prelim}

\subsection{Notation}\label{sec:notation}

I use the following conventions throughout. $\|$ denotes byte string
concatenation. $\mathsf{BE}n(x)$ denotes the big-endian encoding of the
unsigned integer~$x$ in exactly $n/8$~bytes (\eg $\mathsf{BE32}(x)$ is a
4-byte encoding). $|x|$ denotes the byte length of byte string~$x$.
$0^n$ denotes a string of $n$~zero bytes. $\{0,1\}^n$ denotes an
$n$-bit string; superscripts on zero-strings are byte counts while
superscripts on $\{0,1\}$ sets are bit counts. PPT denotes probabilistic
polynomial-time. $\mathsf{H}$ denotes SHA3-256.

Argument labels for $\MAC$ are always explicit:
$\MAC(\text{key}=k, \text{data}=d)$ uses $k$ as the HMAC key and $d$ as
the data, preventing transposition errors.

\subsection{Cryptographic primitives}\label{sec:primitives}

The protocol uses the following primitive suite, referred to as
\texttt{lo-crypto-v1}. No novel cryptographic assumptions are introduced;
the construction composes standard primitives under standard assumptions.

\subsubsection{X-Wing (hybrid KEM)}

X-Wing~\cite{xwing, xwing-ietf} combines X25519 and ML-KEM-768 via a
SHA3-256 combiner. Key pairs satisfy $\pk = (\pk_M, \pk_X)$,
$\sk = (\sk_M, \sk_X)$, where subscripts $M$ and $X$ denote the ML-KEM
and X25519 components respectively. (This tuple notation follows
draft-09's mathematical presentation order; the wire encoding is
X25519-first: $\pk = \pk_X \| \pk_M$.)

$\Encaps(\pk) \to (c, \mathit{ss})$: Generate an ephemeral X25519 key
pair, compute the ML-KEM encapsulation and the X25519 shared secret, then
combine via $\mathit{ss} = \mathsf{H}_3(\mathit{ss}_M \| \mathit{ss}_X \|
\mathit{ct}_X \| \pk_X \| \Lambda)$, where
$\Lambda = \texttt{0x5c2e2f2f5e5c}$ is a fixed domain label and
$\mathsf{H}_3$ denotes SHA3-256.

$\Decaps(\sk, c) \to \mathit{ss}$: Parse $c$, recompute both shared
secrets, and apply the identical combiner. Decapsulation uses ML-KEM's
implicit rejection (FIPS~203~\cite{fips203} \S7.3) --- a mismatched
ciphertext produces a pseudorandom shared secret rather than an error.

X-Wing is IND-CCA2 if at least one of X25519 (under the strong
Diffie-Hellman assumption) or ML-KEM-768 is IND-CCA2~\cite{xwing}.
ML-KEM-768 provides NIST security level~3 (128-bit post-quantum
security), matching the PQ~TLS~1.3 deployment trajectory; level~5
(ML-KEM-1024) would further increase the already-large key sizes for
marginal benefit. Key sizes: 1216-byte public key, 2432-byte secret key,
1120-byte ciphertext, 32-byte shared secret.

For symbolic analysis, X-Wing is treated as a single IND-CCA2 KEM. For
computational models, the black-box IND-CCA2 assumption is stronger than
opening the combiner; bounds are in terms of $P_{\text{kem}}$ rather than
component advantages.

\subsubsection{Hybrid signature scheme (HybridSig)}

HybridSig combines Ed25519~\cite{rfc8032} and ML-DSA-65~\cite{fips204}.

$\Sign(\sk, m) \to \sigma = (\sigma_E \| \sigma_P)$: Both components are
computed independently and concatenated. ML-DSA-65 uses hedged signing
via \texttt{sign\_internal} (FIPS~204 \S6.2) for fault-injection
resistance. This is structurally incompatible with FIPS~204 \S5.2's
external interface, which prepends a context-dependent domain separator;
a FIPS~204-compliant verifier will reject Soliton signatures.

$\Verify(\pk, m, \sigma) \to \{0,1\}$: Returns 1 iff both
$\mathsf{Ed25519.Verify}$ and $\mathsf{ML\text{-}DSA.Verify}$ return~1.
Both components are evaluated eagerly and the conjunction is
constant-time to prevent leaking which component failed.

HybridSig is EUF-CMA if at least one component is EUF-CMA. For symbolic
models, it is treated as a single EUF-CMA signature scheme.

\subsubsection{Key derivation and MAC}

$\MAC$ denotes HMAC-SHA3-256 throughout. All HKDF-based KDF functions
use a single HKDF invocation (Extract-then-Expand per RFC~5869
\cite{rfc5869}) with the specified output length, split sequentially at
32-byte boundaries:

\begin{itemize}[leftmargin=*, itemsep=2pt]
\item $\KDF_{\text{Root}}(\rk, \mathit{ss}) \to (\rk', \ek)$:
  $\HKDF(\text{salt}=\rk, \text{ikm}=\mathit{ss},
  \text{info}=\texttt{"lo-ratchet-v1"}, \text{len}=64)$.

\item $\KDF_{\text{MsgKey}}(\ek, \mathit{counter}) \to \mk$:
  $\mk = \MAC(\text{key}=\ek,
  \text{data}=\texttt{0x01} \| \mathsf{BE32}(\mathit{counter}))$.
  The epoch key $\ek$ does not advance per message.

\item $\KDF_{\text{KEX}}(\mathit{ikm}, \mathit{info}) \to (\rk, \ek)$:
  $\HKDF(\text{salt}=0^{32}, \mathit{ikm}, \mathit{info},
  \text{len}=64)$.

\item $\KDF_{\text{Call}}(\rk, \mathit{ss}_{\text{eph}},
  \mathit{call\_id}, \mathit{fp}_{\text{lo}},
  \mathit{fp}_{\text{hi}})$
  $\to (\mathit{key}_a, \mathit{key}_b,
  \mathit{ck}_{\text{call}})$: HKDF with
  $\text{salt}=\rk$,
  $\text{ikm}=\mathit{ss}_{\text{eph}} \| \mathit{call\_id}$,
  $\text{info}=\texttt{"lo-call-v1"} \| \mathit{fp}_{\text{lo}} \|
  \mathit{fp}_{\text{hi}}$, output 96~bytes.
\end{itemize}

The HMAC-SHA3-256 PRF property under arbitrary hash functions follows from
Bellare's analysis~\cite{bellare06}. The HKDF dual-PRF assumption and
extractor property follow from Krawczyk~\cite{krawczyk10}. Note:
Bellare's and Krawczyk's analyses target HMAC-SHA2 (Merkle-Damg\aa rd);
applicability to HMAC-SHA3-256 (sponge-based) follows from the generic
HMAC construction~\cite{bellare06}, whose PRF argument applies to any
hash function satisfying the underlying pseudorandomness assumptions.
SHA3-256 uses a sponge with an internal permutation (Keccak-$f$) rather
than a Merkle-Damg\aa rd compression function; the HMAC-over-sponge
construction is widely deployed and believed secure, but a
sponge-specific reduction (as opposed to the MD-specific analysis
in~\cite{bellare06}) remains an open problem. NIST's recommended
keyed MAC for SHA-3 is KMAC (SP~800-185), which operates natively on
the sponge; HMAC-SHA3-256 is used here because HKDF (RFC~5869) is
defined in terms of HMAC, and no HKDF-KMAC equivalent is standardized.

\subsubsection{Authenticated encryption}

$\AEAD.\Enc(k, n, m, \mathit{aad}) \to c$: XChaCha20-Poly1305 with a
128-bit tag appended to the ciphertext. Nonces for ratchet messages are
counter-derived: $n = 0^{20} \| \mathsf{BE32}(\mathit{counter})$ (24
bytes total). The session-init first message uses a uniformly random
192-bit nonce as defense-in-depth.

\subsection{Key hierarchy}\label{sec:key-hierarchy}

Soliton uses a four-tier key hierarchy (\Cref{fig:key-hierarchy}),
following the structure established by the Signal
Protocol~\cite{signal-x3dh} and adapted for KEM-based operations:

\begin{itemize}[leftmargin=*, itemsep=3pt]
\item \textbf{Identity Key (IK)}: Long-term composite key pair
  (3200~bytes public key):
  \[
  \pk_{\text{IK}} = \pk_{\text{IK}}[\text{XWing}] \;(1216) \;\|\;
  \pk_{\text{IK}}[\text{Ed25519}] \;(32) \;\|\;
  \pk_{\text{IK}}[\text{ML-DSA}] \;(1952)
  \]
  The X-Wing component is used for KEM operations; the Ed25519 and
  ML-DSA-65 components are used for signing. A single corruption of
  $\sk_{\text{IK}}$ yields both KEM decapsulation and signing
  capability.

\item \textbf{Signed Pre-Key (SPK)}: Medium-term X-Wing key pair, signed
  by the identity key:
  $\sigma_{\text{SPK}} = \Sign(\sk_{\text{IK}},
  \texttt{"lo-spk-sig-v1"} \| \pk_{\text{SPK}})$. Rotated
  approximately weekly.

\item \textbf{One-Time Pre-Key (OPK)}: Single-use X-Wing key pair.
  Deleted immediately after one decapsulation.

\item \textbf{Ephemeral Key (EK)}: Per-session X-Wing key pair generated
  by the initiator. Serves as the initiator's initial ratchet public key.
\end{itemize}

Session key material consists of a root key
$\rk \in \{0,1\}^{256}$, send and receive epoch keys
$\ek_s, \ek_r \in \{0,1\}^{256}$, and single-use message keys
$\mk \in \{0,1\}^{256}$. Epoch keys are replaced on each KEM ratchet
step; message keys are zeroized after use.

\begin{figure}[t]
\centering
\begin{tikzpicture}[
    >=stealth, font=\small,
    box/.style={draw, rounded corners=2pt, minimum height=1.5em,
                minimum width=2.4cm, font=\small},
    kdf/.style={draw, rounded corners=2pt, minimum height=1.3em,
                font=\scriptsize, fill=gray!10},
    arr/.style={->, thick},
    darr/.style={->, thick, dashed},
    lbl/.style={font=\scriptsize},
]

% --- Identity layer ---
\node[box] (IK) at (0, 0) {$\sk_\text{IK}$};
\node[lbl, above=0.1cm of IK] {Identity Key};

% Pre-keys + ephemeral — labels below boxes to avoid overlap with arrows
\node[box] (SPK) at (-3.2, -2.0) {$\sk_\text{SPK}$};
\node[lbl, below=0.1cm of SPK] {Signed Pre-Key};
\node[box] (OPK) at (0, -2.0) {$\sk_\text{OPK}$};
\node[lbl, below=0.1cm of OPK] {One-Time Pre-Key};
\node[box] (EK) at (3.2, -2.0) {$\sk_\text{EK}$};
\node[lbl, below=0.1cm of EK] {Ephemeral Key};

\draw[arr] (IK) -- node[above left, lbl] {signs} (SPK);
\draw[darr] (IK) -- (OPK);
\draw[darr] (IK) -- (EK);

% --- KEX ---
\node[kdf] (KDFKEX) at (0, -3.8)
    {$\textsf{KDF}_\text{KEX}(\mathit{ss}_\text{IK} \| \mathit{ss}_\text{SPK} [\| \mathit{ss}_\text{OPK}])$};
\draw[arr] (SPK) -- (KDFKEX);
\draw[arr] (OPK) -- (KDFKEX);
\draw[arr] (EK) -- (KDFKEX);

% KEX outputs
\node[box] (rk) at (-1.8, -5.2) {$\rk$};
\node[lbl, below=0.1cm of rk] {Root Key};
\node[box] (ek0) at (1.8, -5.2) {$\ek$};
\node[lbl, below=0.1cm of ek0] {Epoch Key};
\draw[arr] (KDFKEX) -- (rk);
\draw[arr] (KDFKEX) -- (ek0);

% --- Ratchet advancement (left branch) ---
\node[kdf] (KDFRoot) at (-1.8, -7.0)
    {$\textsf{KDF}_\text{Root}(\rk, \mathit{ss})$};
\draw[arr] (rk) -- (KDFRoot);

\node[box] (rkp) at (-3.5, -8.4) {$\rk'$};
\node[box] (ekp) at (-0.1, -8.4) {$\ek'$};
\draw[arr] (KDFRoot) -- (rkp);
\draw[arr] (KDFRoot) -- (ekp);

% Feedback loop: rk' → next KDF_Root
\draw[arr, dotted] (rkp.west) -- ++(-0.6, 0)
    |- node[left, lbl, pos=0.25] {next step} (KDFRoot.west);

% --- Message key derivation (right branch) ---
\node[kdf] (KDFMsg) at (1.8, -7.0)
    {$\textsf{KDF}_\text{MsgKey}(\ek, n)$};
\draw[arr] (ek0) -- (KDFMsg);
% ek' feeds KDF_MsgKey on subsequent epochs — route around mk
\draw[darr] (ekp.north) -- ++(0, 0.4) -| (KDFMsg.south west);

\node[box] (mk) at (1.8, -8.4) {$\mk$};
\node[lbl, below=0.1cm of mk] {Message Key};
\draw[arr] (KDFMsg) -- (mk);

\node[kdf] (AEAD) at (1.8, -9.8) {$\textsf{AEAD.Enc}(\mk, n, m)$};
\draw[arr] (mk) -- (AEAD);
\node[box] (ct) at (1.8, -10.8) {ciphertext};
\draw[arr] (AEAD) -- (ct);

% --- Call key derivation (left-bottom branch) ---
\node[kdf] (KDFCall) at (-3.5, -9.8)
    {$\textsf{KDF}_\text{Call}(\rk, \mathit{ss}_\text{eph})$};
\draw[darr] (rkp) -- (KDFCall);

\node[box] (ck) at (-3.5, -10.8) {$\mathit{key}_a, \mathit{key}_b, \mathit{ck}$};
\node[lbl, below=0.1cm of ck] {Call Keys};
\draw[arr] (KDFCall) -- (ck);

\end{tikzpicture}
\caption{Key derivation hierarchy. Solid arrows show derivation;
dashed arrows show KEM operations. The root key $\rk$ feeds both
$\textsf{KDF}_\text{Root}$ (ratchet advancement: $\rk' \to$ next step)
and $\textsf{KDF}_\text{Call}$ (call key derivation). Message keys are
counter-mode: $\mk_i = \textsf{MAC}(\ek, \texttt{0x01} \|
\textsf{BE32}(i))$, enabling $O(1)$ decryption without a skip cache.}
\label{fig:key-hierarchy}
\end{figure}

% ============================================================================
% 3. PROTOCOL DESCRIPTION
% ============================================================================
\section{Protocol description}\label{sec:protocol}

This section describes each sub-protocol at a level sufficient for
security analysis. The full wire formats, encoding details, and
implementation guidance are in the companion
specification~\cite{soliton-spec}.

\subsection{LO-KEX: Session establishment}\label{sec:kex}

LO-KEX (\Cref{fig:kex-flow}) establishes a shared session key between
an initiator~(Alice) and a responder~(Bob) via asynchronous KEM-based
key agreement. The design
follows the structure of X3DH~\cite{signal-x3dh} and
PQXDH~\cite{signal-pqxdh}, replacing Diffie-Hellman operations with
X-Wing encapsulations and adding hybrid post-quantum signatures for
initiator authentication.

\subsubsection{Pre-key bundle}

Bob publishes a bundle
$\mathit{Bundle}_B = (\mathit{cv}, \pk_{\text{IK}_B},
\pk_{\text{SPK}_B}, \mathit{id}_{\text{SPK}}, \sigma_{\text{SPK}}
[, \pk_{\text{OPK}_B}, \mathit{id}_{\text{OPK}}])$,
where $\sigma_{\text{SPK}} = \Sign(\sk_{\text{IK}_B},
\texttt{"lo-spk-sig-v1"} \| \pk_{\text{SPK}_B})$ and
$\mathit{cv} = \texttt{"lo-crypto-v1"}$. The signature binds the SPK to
Bob's identity but intentionally excludes $\mathit{id}_{\text{SPK}}$ and
$\mathit{cv}$ from the signed data --- an adversary controlling the
bundle relay can substitute these without invalidating the signature, but
this causes lookup failure rather than a security breach.

\subsubsection{Session initiation (Alice)}

\begin{enumerate}[leftmargin=*, itemsep=2pt]
\item \textbf{Verify bundle}: Check $\pk_{\text{IK}_B}$ matches the
  known reference, verify $\sigma_{\text{SPK}}$, check version
  compatibility, validate OPK co-presence.

\item \textbf{Generate ephemeral key}:
  $(\pk_{\text{EK}}, \sk_{\text{EK}}) \gets \KeyGen()$.

\item \textbf{Encapsulate}:
  \begin{align*}
    (c_{\text{IK}}, \mathit{ss}_{\text{IK}}) &\gets
      \Encaps(\pk_{\text{IK}_B}[\text{XWing}]) \\
    (c_{\text{SPK}}, \mathit{ss}_{\text{SPK}}) &\gets
      \Encaps(\pk_{\text{SPK}_B}) \\
    (c_{\text{OPK}}, \mathit{ss}_{\text{OPK}}) &\gets
      \Encaps(\pk_{\text{OPK}_B}) \quad\text{(if OPK present)}
  \end{align*}

\item \textbf{Derive session keys}:
  $\mathit{ikm} = \mathit{ss}_{\text{IK}} \|
  \mathit{ss}_{\text{SPK}} [\| \mathit{ss}_{\text{OPK}}]$;
  $(\rk, \ek) \gets \KDF_{\text{KEX}}(\mathit{ikm}, \mathit{info})$,
  where the $\mathit{info}$ string encodes a version label, both
  composite identity public keys, and the ephemeral public key with
  length prefixes to ensure injectivity.

\item \textbf{Construct and sign session init}: Construct
  $\mathit{SI}$ containing the crypto version, both identity
  fingerprints ($\mathit{fp} = \mathsf{H}(\pk_{\text{IK}})$),
  $\pk_{\text{EK}}$, all KEM ciphertexts, and key identifiers. Sign:
  \[
    \sigma_{\text{SI}} \gets \Sign(\sk_{\text{IK}_A},\;
    \texttt{"lo-kex-init-sig-v1"} \| \mathsf{Encode}(\mathit{SI}))
  \]

\item \textbf{Encrypt first message}:
  $\mk_0 \gets \KDF_{\text{MsgKey}}(\ek, 0)$;
  $n_0 \xleftarrow{\$} \{0,1\}^{192}$;
  \begin{align*}
  \mathit{aad}_0 &= \texttt{"lo-dm-v1"} \| \mathit{fp}_{\text{IK}_A}
    \| \mathit{fp}_{\text{IK}_B} \| \mathsf{Encode}(\mathit{SI}) \\
  c_0 &= \AEAD.\Enc(\mk_0, n_0, m_0, \mathit{aad}_0)
  \end{align*}
  Transmit $(\mathit{SI}, \sigma_{\text{SI}}, n_0 \| c_0)$.
\end{enumerate}

\subsubsection{Session reception (Bob)}

Bob resolves Alice's identity from $\mathit{fp}_{\text{IK}_A}$, validates
fingerprints and version, verifies $\sigma_{\text{SI}}$ \emph{before} any
KEM operations (so a forged signature is rejected without performing
decapsulation), then decapsulates to recover the shared secrets and
derives the same $(\rk, \ek)$. Successful decryption of $c_0$ completes
session establishment and provides Bob with key confirmation of Alice
(Alice holds $\mk_0$, therefore $\ek$, therefore the correct session
key). Alice obtains key confirmation of Bob only when Bob's first
ratchet reply decrypts successfully.

If an OPK was used, $\sk_{\text{OPK}}$ is deleted atomically ---
concurrent session inits referencing the same OPK are resolved by at
most one succeeding.

\begin{figure}[t]
\centering
\begin{tikzpicture}[
    >=stealth, font=\small,
    party/.style={font=\small\bfseries},
    msg/.style={->, thick},
    note/.style={font=\scriptsize, text width=4.2cm, align=left},
]
% Party labels
\node[party] (A) at (0, 0) {Alice (initiator)};
\node[party] (B) at (7, 0) {Bob (responder)};

% Lifelines
\draw[thick] (0, -0.3) -- (0, -10.5);
\draw[thick] (7, -0.3) -- (7, -10.5);

% Bundle fetch
\draw[msg] (0, -0.8) -- node[above, font=\scriptsize] {fetch bundle} (7, -0.8);
\draw[msg, dashed] (7, -1.3) -- node[above, font=\scriptsize]
    {$(\mathit{cv},\, \mathit{pk}_{\text{IK}_B},\,
    \mathit{pk}_{\text{SPK}_B},\, \sigma_{\text{SPK}}
    [,\, \mathit{pk}_{\text{OPK}_B}])$} (0, -1.3);

% Alice processing
\node[note, anchor=east] at (-0.2, -2.1) {verify $\sigma_{\text{SPK}}$};
\node[note, anchor=east] at (-0.2, -2.7) {$(\mathit{pk}_{\text{EK}}, \mathit{sk}_{\text{EK}}) \gets \textsf{KeyGen}()$};
\node[note, anchor=east] at (-0.2, -3.5)
    {$\textsf{Encaps} \to (c_{\text{IK}}, c_{\text{SPK}} [, c_{\text{OPK}}])$};
\node[note, anchor=east] at (-0.2, -4.3)
    {$(\mathit{rk}, \mathit{ek}) \gets \textsf{KDF}_{\text{KEX}}(\mathit{ikm}, \mathit{info})$};
\node[note, anchor=east] at (-0.2, -4.9)
    {$\sigma_{\text{SI}} \gets \textsf{Sign}(\mathit{sk}_{\text{IK}_A},\, \textsf{SI})$};
\node[note, anchor=east] at (-0.2, -5.5)
    {$c_0 \gets \textsf{AEAD.Enc}(\mathit{mk}_0,\, m_0)$};

% Session init message
\draw[msg] (0, -6.2) -- node[above, font=\scriptsize]
    {$(\textsf{SI},\; \sigma_{\text{SI}},\; n_0 \| c_0)$} (7, -6.2);

% Bob processing
\node[note, anchor=west] at (7.2, -6.9) {verify $\sigma_{\text{SI}}$};
\node[note, anchor=west] at (7.2, -7.5)
    {$\textsf{Decaps} \to (\mathit{ss}_{\text{IK}}, \mathit{ss}_{\text{SPK}} [, \mathit{ss}_{\text{OPK}}])$};
\node[note, anchor=west] at (7.2, -8.1)
    {delete $\mathit{sk}_{\text{OPK}}$ (if used)};
\node[note, anchor=west] at (7.2, -8.7)
    {$(\mathit{rk}, \mathit{ek}) \gets \textsf{KDF}_{\text{KEX}}(\mathit{ikm}, \mathit{info})$};
\node[note, anchor=west] at (7.2, -9.3)
    {$m_0 \gets \textsf{AEAD.Dec}(\mathit{mk}_0,\, c_0)$};

% Session established
\draw[dashed, thick, gray] (-0.5, -10) -- (7.5, -10);
\node[font=\scriptsize\itshape, gray] at (3.5, -10.3) {session established --- ratchet begins};
\end{tikzpicture}
\caption{LO-KEX session establishment. Alice verifies Bob's bundle,
encapsulates to three public keys (IK, SPK, OPK), derives session keys
via $\textsf{KDF}_{\text{KEX}}$, signs the session init, and encrypts the
first message. Bob verifies Alice's signature before any KEM operation,
then decapsulates and derives the same session key. OPK fields are
optional (brackets).}
\label{fig:kex-flow}
\end{figure}

\subsection{LO-Ratchet: Ongoing message encryption}\label{sec:ratchet}

LO-Ratchet provides forward secrecy and post-compromise security for
ongoing message exchange. It adapts the double ratchet
algorithm~\cite{signal-doubleratchet, acd19} with two key modifications:
KEM ratchet steps replace DH ratchet steps, and counter-mode key
derivation replaces chain-mode key derivation.

\subsubsection{Ratchet state}

Each party maintains a ratchet state~$\Sigma$ containing:
$\rk$~(root key), $\ek_s, \ek_r$~(send/receive epoch keys),
$(\pk_s, \sk_s)$~(send ratchet keypair), $\pk_r$~(peer's ratchet
public key), $\mathit{prev\_ek_r}$~(retained prior epoch key),
$s, r$~(send/receive counters),
$\mathit{pending} \in \{\top, \bot\}$~(KEM ratchet step due on next
send), $\mathit{recv\_seen}$~(duplicate detection set),
$\mathit{local\_fp}, \mathit{remote\_fp}$~(identity fingerprints),
and $\mathit{epoch}$~(anti-rollback counter).

\subsubsection{Counter-mode message key derivation}

Message keys are derived as
$\mk = \KDF_{\text{MsgKey}}(\ek, \mathit{counter}) =
\MAC(\text{key}=\ek,
\text{data}=\texttt{0x01} \| \mathsf{BE32}(\mathit{counter}))$.
The epoch key is static within an epoch; all messages in the same epoch
share a single $\ek$. This provides $O(1)$~random-access decryption ---
any message counter yields its message key directly, with no iterated
hashing and no skip cache. The trade-off is that forward secrecy is
per-epoch (per KEM ratchet step), not per-message; see
\Cref{sec:rationale} for the design rationale.

\subsubsection{KEM ratchet step}

A KEM ratchet step occurs when a party sends a message after receiving
one (direction change), triggered by $\mathit{pending} = \top$. The
sender:

\begin{enumerate}[leftmargin=*, itemsep=2pt]
\item Generates a fresh X-Wing keypair
  $(\pk_s', \sk_s') \gets \KeyGen()$.
\item Encapsulates to the peer's ratchet public key:
  $(c_{\text{ratchet}}, \mathit{ss}) \gets \Encaps(\pk_r)$.
\item Advances the root key:
  $(\rk', \ek_s') \gets \KDF_{\text{Root}}(\rk, \mathit{ss})$.
\item Updates state: $\rk \gets \rk'$, $\ek_s \gets \ek_s'$,
  $(\pk_s, \sk_s) \gets (\pk_s', \sk_s')$, $s \gets 0$,
  $\mathit{pending} \gets \bot$.
\end{enumerate}

The message header includes $\pk_s$ and $c_{\text{ratchet}}$, allowing
the receiver to perform the symmetric decapsulation and key derivation.

\subsubsection{Forward secrecy and \texorpdfstring{$\mathit{prev\_ek_r}$}{prev\_ek\_r} retention}

Forward secrecy is per-epoch with a \textbf{two-step delay on the receive
side} (\Cref{fig:ratchet-flow}). When a KEM ratchet step replaces a
party's receive epoch key, the
old $\ek_r$ moves into $\mathit{prev\_ek_r}$ to allow decryption of
delayed messages from the immediately prior epoch. A corruption of
$\Sigma$ after a single KEM ratchet step therefore reveals
$\mathit{prev\_ek_r}$ and all message keys from the prior receive epoch.
Full receive-side forward secrecy requires two KEM ratchet steps: the
first moves $\ek_r$ into $\mathit{prev\_ek_r}$, the second overwrites
$\mathit{prev\_ek_r}$ (the old value is zeroized). On the send side,
forward secrecy applies after a single step ($\ek_s$ is overwritten
directly with no retention).

\begin{figure}[t]
\centering
\begin{tikzpicture}[
    >=stealth, font=\small,
    party/.style={font=\small\bfseries},
    msg/.style={->, thick},
    note/.style={font=\scriptsize, text width=4.2cm, align=left},
    epoch/.style={font=\scriptsize\itshape, gray},
]
% Party labels
\node[party] (A) at (0, 0) {Alice};
\node[party] (B) at (7, 0) {Bob};

% Lifelines
\draw[thick] (0, -0.3) -- (0, -12.4);
\draw[thick] (7, -0.3) -- (7, -12.4);

% Epoch 0: Alice sends (same epoch, no KEM step)
\node[epoch] at (3.5, -0.7) {Epoch 0 (from KEX)};

\draw[msg] (0, -1.4) -- node[above, font=\scriptsize]
    {$H_1 = (\mathit{pk}_{\text{EK}},\, \bot,\, 1,\, 0),\ c_1$} (7, -1.4);
\node[note, anchor=east] at (-0.2, -1.4) {$\mk_1 = \textsf{KDF\_MsgKey}(\ek_s, 1)$};

\draw[msg] (0, -2.1) -- node[above, font=\scriptsize]
    {$H_2 = (\mathit{pk}_{\text{EK}},\, \bot,\, 2,\, 0),\ c_2$} (7, -2.1);

% Bob receives, sets pending = true
\node[note, anchor=west] at (7.2, -2.8) {decrypt: $\mathit{pk}_{\text{EK}} = \mathit{pk}_r$};
\node[note, anchor=west] at (7.2, -3.3) {$\to$ CurrentEpoch, pending $\gets \top$};

% Direction change: Bob sends → KEM ratchet step
\node[epoch] at (3.5, -3.9) {Direction change $\to$ Epoch 1};

\node[note, anchor=west] at (7.2, -4.6)
    {pending $= \top \to$ KEM ratchet:};
\node[note, anchor=west] at (7.2, -5.2)
    {$(\mathit{pk}_B, \mathit{sk}_B) \gets \textsf{KeyGen}()$};
\node[note, anchor=west] at (7.2, -5.8)
    {$(c_r, \mathit{ss}) \gets \textsf{Encaps}(\mathit{pk}_{\text{EK}})$};
\node[note, anchor=west] at (7.2, -6.4)
    {$(\rk', \ek_s') \gets \textsf{KDF\_Root}(\rk, \mathit{ss})$};
\node[note, anchor=west] at (7.2, -7.0)
    {$\mathit{pn}, s \gets 0$, pending $\gets \bot$};

\draw[msg] (7, -7.6) -- node[above, font=\scriptsize]
    {$H_3 = (\mathit{pk}_B,\, c_r,\, 0,\, 0),\ c_3$} (0, -7.6);

% Alice receives → NewEpoch
\node[note, anchor=east] at (-0.2, -8.3)
    {$\mathit{pk}_B \neq \mathit{pk}_r \to$ NewEpoch};
\node[note, anchor=east] at (-0.2, -8.9)
    {$\mathit{ss} \gets \textsf{Decaps}(\mathit{sk}_{\text{EK}}, c_r)$};
\node[note, anchor=east] at (-0.2, -9.5)
    {$(\rk', \ek_r') \gets \textsf{KDF\_Root}(\rk, \mathit{ss})$};
\node[note, anchor=east] at (-0.2, -10.1)
    {$\mathit{prev\_ek_r} \gets \ek_r$, $\mathit{pk}_r \gets \mathit{pk}_B$};
\node[note, anchor=east] at (-0.2, -10.7)
    {pending $\gets \top$ (next send $\to$ KEM step)};

% Epoch 2 preview
\node[epoch] at (3.5, -11.4) {Alice's next send $\to$ Epoch 2 (KEM ratchet)};
\node[note, anchor=east] at (-0.2, -11.9)
    {$\textsf{Encaps}(\mathit{pk}_B) \to$ new $\rk'', \ek_s''$};

\end{tikzpicture}
\caption{Ratchet direction change. Alice sends two messages in Epoch~0
(no KEM step). Bob's first reply triggers a KEM ratchet step
(pending~$= \top$): fresh keypair, encapsulate to Alice's $\mathit{pk}_s$,
derive new root and epoch keys. Alice receives the new-epoch message,
decapsulates, rotates $\mathit{prev\_ek_r}$, and sets pending~$= \top$
for her next send. Each direction change advances the epoch and
introduces fresh KEM randomness.}
\label{fig:ratchet-flow}
\end{figure}

\subsubsection{Anti-reflection}

Reflected messages --- where an adversary replays a message from $A
\to B$ back to~$A$ as if it were from $B \to A$ --- are defeated by
directional AAD construction:
\[
\mathit{aad} = \texttt{"lo-dm-v1"} \| \mathit{fp}_{\text{sender}} \|
\mathit{fp}_{\text{recipient}} \| \mathsf{Encode}(H)
\]
Since $\mathit{fp}_{\text{sender}} \neq \mathit{fp}_{\text{recipient}}$
(enforced at construction, invariant~(h)), the reversed fingerprint
ordering produces a different AAD and AEAD verification fails.

\subsection{LO-Auth: Key possession proof}\label{sec:auth}

LO-Auth provides server-side authentication of a client's identity key
ownership. The server encapsulates to the client's
$\pk_{\text{IK}}[\text{XWing}]$:
$(c, \mathit{ss}) \gets \Encaps(\pk_{\text{IK}}[\text{XWing}])$.
The client decapsulates and returns
$\mathit{proof} = \MAC(\text{key}=\mathit{ss},
\text{data}=\texttt{"lo-auth-v1"})$.
Challenge single-use is enforced server-side. Under IND-CCA2 and PRF
assumptions, a client who produces a valid proof for a fresh challenge
possesses $\sk_{\text{IK}}[\text{XWing}]$.

In the composed setting with LO-KEX, LO-Auth sessions provide the
adversary with an interactive decapsulation oracle on the identity key
--- each challenge constitutes one additional CCA2 query. The security
loss is additive in the number of LO-Auth sessions.

\subsection{LO-Call: Voice/video call encryption}\label{sec:call}

LO-Call derives call-specific encryption keys with ephemeral forward
secrecy, independent of the ratchet's KEM ratchet cycle. For a call
with identifier $\mathit{call\_id}$:

\begin{enumerate}[leftmargin=*, itemsep=2pt]
\item Generate ephemeral X-Wing keypair
  $(\pk_{\text{eph}}, \sk_{\text{eph}}) \gets \KeyGen()$.
  Send $(\mathit{call\_id}, \pk_{\text{eph}})$ to the peer via a
  ratchet-encrypted signaling message.
\item Peer encapsulates to the ephemeral public key:
  $(c_{\text{eph}}, \mathit{ss}_{\text{eph}}) \gets
  \Encaps(\pk_{\text{eph}})$.
  Sends $c_{\text{eph}}$ back via a ratchet-encrypted message.
  Initiator decapsulates:
  $\mathit{ss}_{\text{eph}} \gets \Decaps(\sk_{\text{eph}},
  c_{\text{eph}})$.
\item Both parties derive call keys:
  $(\mathit{key}_a, \mathit{key}_b, \mathit{ck}_{\text{call}}) \gets
  \KDF_{\text{Call}}(\rk, \mathit{ss}_{\text{eph}}, \mathit{call\_id},
  \mathit{fp}_{\text{lo}}, \mathit{fp}_{\text{hi}})$.
\end{enumerate}

Intra-call rekeying advances the call chain via
$\KDF_{\text{CallChain}}(\mathit{ck}_{\text{call}})$, producing fresh
send/receive keys and a new chain key; the old chain key is zeroized.
Call keys are independent of ratchet state: the ephemeral keypair and
$\mathit{ss}_{\text{eph}}$ are generated within call setup and zeroized
after HKDF, so $\mathsf{Corrupt}(\text{RatchetState})$ does not reveal
$\mathit{ss}_{\text{eph}}$ (recovering it from $c_{\text{eph}}$ requires
breaking X-Wing).

\subsection{LO-Stream: Streaming AEAD}\label{sec:stream}

LO-Stream provides chunked authenticated encryption for bulk data (file
transfer, media) with both sequential and random-access interfaces. Each
stream uses a caller-provided 32-byte key and a random 192-bit base
nonce.

\subsubsection{Nonce derivation}

Per-chunk nonces are derived by XOR-ing a mask into the base nonce
(\Cref{fig:stream-nonce}):
\begin{align*}
  \mathit{mask} &= \mathsf{BE64}(\mathit{chunk\_index}) \|
    \mathit{tag\_byte} \| 0^{15} \\
  \mathit{chunk\_nonce} &= \mathit{base\_nonce} \oplus \mathit{mask}
\end{align*}
where $\mathit{tag\_byte} \in \{\texttt{0x00}, \texttt{0x01}\}$
indicates non-final or final chunk. Distinct
$(\mathit{chunk\_index}, \mathit{tag\_byte})$ pairs produce distinct
masks, and XOR with a constant is a bijection, so nonce injectivity
within a single stream is unconditional.

\begin{figure}[t]
\centering
\begin{tikzpicture}[font=\small]
  % Mask row
  \node[font=\scriptsize\bfseries] at (-1.5, 1.2) {mask};
  \draw (0, 0.8) rectangle (4, 1.6);
  \node at (2, 1.2) {\scriptsize chunk\_index (8\,B, BE64)};
  \draw (4, 0.8) rectangle (5, 1.6);
  \node at (4.5, 1.2) {\scriptsize tag};
  \draw (5, 0.8) rectangle (9.5, 1.6);
  \node at (7.25, 1.2) {\scriptsize $0\!\times\!00 \times 15$ (padding)};

  % Byte markers
  \node[font=\tiny, gray] at (0, 0.6) {0};
  \node[font=\tiny, gray] at (4, 0.6) {8};
  \node[font=\tiny, gray] at (5, 0.6) {9};
  \node[font=\tiny, gray] at (9.5, 0.6) {24};

  % XOR symbol
  \node[font=\large] at (4.75, 0.2) {$\oplus$};

  % Base nonce row
  \node[font=\scriptsize\bfseries] at (-1.5, -0.4) {base\_nonce};
  \draw (0, -0.8) rectangle (9.5, 0);
  \node at (4.75, -0.4) {\scriptsize random 24 bytes (public, per-stream)};

  % Equals
  \node[font=\large] at (4.75, -1.2) {$=$};

  % Result row
  \node[font=\scriptsize\bfseries] at (-1.5, -2.0) {chunk\_nonce};
  \draw[thick] (0, -2.4) rectangle (9.5, -1.6);
  \node at (4.75, -2.0) {\scriptsize 24-byte XChaCha20-Poly1305 nonce};
\end{tikzpicture}
\caption{Streaming AEAD nonce derivation (\cref{sec:stream}). The 24-byte mask
encodes the chunk index (8 bytes), finality tag (1 byte:
\texttt{0x00}~non-final, \texttt{0x01}~final), and 15 zero-padding
bytes. XOR with the per-stream random base nonce yields a unique
chunk nonce. Only 9 bytes vary within a stream; the 15 fixed bytes
are load-bearing for cross-stream isolation (birthday bound
$\sim(\sum M_i)^2 / 2^{193}$).}
\label{fig:stream-nonce}
\end{figure}

\subsubsection{Dual interfaces}

\textbf{Sequential} ($\mathsf{encrypt\_chunk}$ /
$\mathsf{decrypt\_chunk}$): Stateful --- advances an internal
$\mathit{next\_index}$, enforces ordering by construction (the
decryptor derives the chunk index from its own counter, not from the
wire format), and tracks finalization.

\textbf{Random-access} ($\mathsf{encrypt\_chunk\_at}$ /
$\mathsf{decrypt\_chunk\_at}$): Stateless --- takes an explicit index,
reads only persistent state (key, base nonce), provides no ordering or
truncation guarantees. Ordering and truncation resistance are caller
obligations in this mode.

The sequential and random-access decryption interfaces can coexist on
the same stream. The state partition --- linear state
($\mathit{next\_index}$, $\mathit{finalized}$) for sequential,
persistent state (key, base nonce) for random-access --- ensures the
random-access oracle cannot interfere with sequential ordering
properties.

\subsubsection{AAD construction}

Each chunk's AAD binds the chunk to its stream, position, finality, and
application context:
\begin{multline*}
\mathit{aad} = \texttt{"lo-stream-v1"} \| \mathit{version} \|
\mathit{flags} \| \mathit{base\_nonce} \| {} \\
\mathsf{BE64}(\mathit{chunk\_index}) \| \mathit{tag\_byte} \|
\mathit{caller\_aad}
\end{multline*}
The base nonce in the AAD is load-bearing for cross-stream isolation:
different base nonces guarantee distinct AADs at every position,
making any cross-stream ciphertext an unconditional INT-CTXT forgery.


% ============================================================================
% 4. SECURITY MODEL
% ============================================================================
\section{Security model}\label{sec:security-model}

\subsection{Adversary model}\label{sec:adversary}

I adopt a Dolev-Yao network adversary who controls all communication
channels: the adversary can intercept, drop, delay, replay, modify, and
inject messages between any two parties. In addition, the adversary has access
to corruption oracles that model partial compromise, following the
approach of Cohn-Gordon \etal~\cite{cgcd20} and Alwen
\etal~\cite{acd19}.

\subsubsection{Corruption oracles}

The adversary may issue the following queries adaptively:

\begin{itemize}[leftmargin=*, itemsep=3pt]
\item $\mathsf{Corrupt}(\text{IK}, P)$: Reveals the full composite
  identity secret key of party~$P$.

\item $\mathsf{Corrupt}(\text{SPK}, P, \mathit{id})$ /
  $\mathsf{Corrupt}(\text{OPK}, P, \mathit{id})$: Reveals the
  secret key for the specified pre-key.

\item $\mathsf{Corrupt}(\text{RatchetState}, P, t)$: Reveals the full
  ratchet state~$\Sigma$ at time~$t$, including $\rk$, both epoch keys,
  the send ratchet secret key, $\mathit{prev\_ek_r}$, and all counters.

\item $\mathsf{Corrupt}(\text{CallKeys}, P, \mathit{call\_id})$:
  Reveals call keys for a specific call.

\item $\mathsf{Corrupt}(\text{StreamKey}, P, \mathit{stream\_id})$:
  Reveals the stream key for a specific streaming AEAD instance.

\item $\mathsf{Corrupt}(\text{RNG}, P, t)$: Reveals all randomness
  generated by party~$P$ at time~$t$.
\end{itemize}

Corruption queries are temporally parameterized where relevant,
enabling fine-grained modeling of partial compromise.

\subsection{Freshness predicates}\label{sec:freshness}

Each theorem's security claim is conditional on a freshness predicate
defining the adversary class for which the claim holds.

\subsubsection{LO-KEX freshness}

A session key is fresh if the adversary has not obtained all of
$\{\sk_{\text{IK}_B}[\text{XWing}], \sk_{\text{SPK}_B},
\sk_{\text{OPK}_B}\}$ (OPK-present case), has not issued
$\mathsf{Corrupt}(\text{RNG}, A, t)$ at the session establishment
epoch, and has not issued $\mathsf{Corrupt}(\text{RatchetState}, P, t)$
at or after the establishment epoch for either party (which would
directly reveal $\rk$ and $\ek$). The OPK-absent case has a weaker
corruption threshold: $\sk_{\text{IK}_B}[\text{XWing}]$ and
$\sk_{\text{SPK}_B}$ together suffice to derive the session key.

\subsubsection{LO-Ratchet freshness (F1--F4)}

A message key at epoch~$e$ is fresh if all of the following hold:

\begin{itemize}[leftmargin=*, itemsep=2pt]
\item[\textbf{F1.}] No $\mathsf{Corrupt}(\text{RatchetState}, P, t)$
  covers epoch~$e$ (epoch key not directly revealed).

\item[\textbf{F2.}] If $\mathsf{Corrupt}(\text{RatchetState}, P, t_c)$
  was issued for any $t_c$ before the target epoch, then at least one
  KEM ratchet step between $t_c$ and the target epoch --- the
  \emph{recovery step}~$t_r$ --- executed with uncompromised
  encapsulator randomness (no
  $\mathsf{Corrupt}(\text{RNG}, \text{encapsulator}, t)$ at that step).
  Absent any prior corruption, F2 is vacuously satisfied.

\item[\textbf{F3.}] The decapsulator's ratchet state was uncompromised
  at $t_r$ and all preceding steps between $t_c$ and $t_r$: no
  $\mathsf{Corrupt}(\text{RatchetState},$ $\text{decapsulator}, t)$
  covers those positions.

\item[\textbf{F4.}] The decapsulator's ratchet keypair encapsulated to
  at $t_r$ was generated without
  $\mathsf{Corrupt}(\text{RNG},$ $\text{decapsulator},
  t_{\text{keygen}})$ at its generation epoch --- otherwise the
  adversary holds $\sk_s$ and can compute the KEM shared secret from
  the public ciphertext.
\end{itemize}

All four conditions are conjunctive. In the absence of any
$\mathsf{Corrupt}(\text{RatchetState})$ before the target epoch, F2--F4
are vacuously satisfied and freshness reduces to F1 alone. F1--F4 are
syntactic (query-based) predicates, not semantic (knowledge-based) ---
the gap is bridged by the IND-CCA2 reduction embedding its challenge at
the recovery step~\cite{acd19}.

\subsubsection{Other freshness conditions}

LO-Auth requires no $\mathsf{Corrupt}(\text{IK})$ on the client and
no $\mathsf{Corrupt}(\text{RNG})$ at the challenge epoch.
LO-Call requires $\rk$ freshness, uncompromised ephemeral RNG, and no
$\mathsf{Corrupt}(\text{CallKeys})$.
LO-Stream requires no $\mathsf{Corrupt}(\text{StreamKey})$ and no
$\mathsf{Corrupt}(\text{RNG})$ at base nonce generation. Stream keys
are independent of ratchet state by construction.

\subsection{Assumptions}\label{sec:assumptions}

All primitive operations are total except $\Verify$ and $\AEAD.\Dec$.
$\Decaps$ is total due to ML-KEM's implicit rejection. The following
security properties are assumed: X-Wing IND-CCA2~\cite{xwing},
HybridSig EUF-CMA, HMAC-SHA3-256 PRF~\cite{bellare06}, HKDF dual-PRF
and extractor~\cite{krawczyk10}, XChaCha20-Poly1305 IND-CPA + INT-CTXT.
No novel assumptions are introduced.

XChaCha20-Poly1305 does \textbf{not} provide key commitment. This is
not a concern: epoch identification selects a single key before
decryption, and streaming AEAD uses a single caller-provided key.

\subsection{Out of scope}\label{sec:out-of-scope}

\textbf{Deniability}: Not claimed. KEM ciphertexts and signatures are
attributable~\cite{fiedler-janson24}. \textbf{Group messaging}:
Strictly two-party. \textbf{Traffic analysis}: Message sizes, timing,
and epoch structure are observable. \textbf{Endpoint security}: Not
modeled. \textbf{Side channels}: Generally out of scope, except that
constant-time signature verification is a normative requirement.


% ============================================================================
% 5. SECURITY ANALYSIS
% ============================================================================
\section{Security analysis}\label{sec:security}

This section presents the 13 security theorems. Full game definitions
and detailed proof sketches are in the companion formal
analysis~\cite{soliton-analysis}; I present theorem statements,
reduction targets, and key proof ideas.

\subsection{Session establishment (Theorems 1--2)}

\begin{theorem}[LO-KEX Session Key Secrecy]\label{thm:kex-secrecy}
For sessions established between $A$ and $B$, if the session key is
fresh, no PPT adversary can distinguish it from uniform with
non-negligible advantage. Reduces to X-Wing IND-CCA2 + HKDF extractor.
In the composed setting with LO-Auth, each authentication session adds
one CCA2 oracle query; the loss is additive.
\end{theorem}

\begin{theorem}[LO-KEX Mutual Authentication]\label{thm:kex-auth}
\leavevmode
\begin{enumerate}[label=(\alph*), leftmargin=*, itemsep=2pt]
\item \emph{Recipient authentication}: If $A$ completes LO-KEX with
  $B$'s verified bundle and obtains a fresh session key, then $B$
  possesses $\sk_{\text{IK}_B}$. Binding is implicit (KEM
  decapsulability) and explicit ($\mathit{fp}_{\text{IK}_B}$ in
  $\sigma_{\text{SI}}$). Reduces to X-Wing IND-CCA2 + HybridSig
  EUF-CMA.

\item \emph{Initiator authentication}: Verification of
  $\sigma_{\text{SI}}$ proves $A$ possesses $\sk_{\text{IK}_A}$.
  Reduces to HybridSig EUF-CMA.

\end{enumerate}
\end{theorem}

\begin{claim}[Key Confirmation]\label{claim:key-confirm}
Key confirmation is asymmetric and deferred to the ratchet layer
(not mechanically verified; see \cref{sec:limitations}):
\begin{enumerate}[label=(\alph*), start=3, leftmargin=*, itemsep=2pt]
\item \emph{$A \to B$}: $A$ obtains key confirmation of~$B$ only when
  $B$'s first ratchet reply decrypts successfully --- requiring a
  round trip. Reduces to XChaCha20-Poly1305 INT-CTXT + Theorem~1.
\item \emph{$B \to A$}: $B$ obtains key confirmation of~$A$ immediately
  upon decrypting the first message (successful AEAD decryption proves
  $A$ holds $\mk_0$, therefore $\ek$, therefore the same session key).
  Reduces to XChaCha20-Poly1305 INT-CTXT + Theorem~1.
\end{enumerate}
This asymmetry is inherent to asynchronous establishment.
\end{claim}

\subsection{Ratchet security (Theorems 3--5)}

\begin{theorem}[Message Secrecy]\label{thm:msg-secrecy}
If the message key is fresh (F1--F4), no PPT adversary can distinguish
the plaintext from random.
\end{theorem}

\begin{proofsketch}
The reduction proceeds in three stages. First, the IND-CCA2 challenger
for X-Wing is embedded at the KEM ratchet step establishing the target
epoch; the resulting shared secret is replaced with a uniformly random
value (cost: $P_{\text{kem}}$). Second, the HKDF extractor property
ensures that $\KDF_{\text{Root}}(\rk, \mathit{ss})$ with random
$\mathit{ss}$ produces outputs $(\rk', \ek)$ indistinguishable from
uniform (cost: $P_{\text{prf}}$). Third, the epoch key $\ek$ is used as
a PRF key in $\KDF_{\text{MsgKey}}$; the PRF guarantee yields a message
key $\mk$ indistinguishable from random (cost: $P_{\text{prf}}$), under
which the AEAD ciphertext is IND-CPA secure. Nonce uniqueness ---
depending on fork prevention, $\mathit{min\_epoch}$ integrity, counter
exhaustion guards, and counter retirement at session init --- ensures
the AEAD reduction is sound.
\end{proofsketch}

\begin{theorem}[Forward Secrecy]\label{thm:fs}
Per-epoch, with a two-step receive-side delay:
\begin{enumerate}[label=(\alph*), leftmargin=*, itemsep=2pt]
\item \emph{Send-side}: One KEM ratchet step suffices ($\ek_s$
  overwritten directly).
\item \emph{Receive-side}: One step is insufficient
  ($\mathit{prev\_ek_r}$ retains the old key); two steps suffice
  ($\mathit{prev\_ek_r}$ overwritten).
\end{enumerate}
Reduces to HKDF one-wayness + X-Wing IND-CCA2.
\end{theorem}

\begin{theorem}[Post-Compromise Security]\label{thm:pcs}
After $\mathsf{Corrupt}(\text{RatchetState}, P, t_c)$, if F1--F4 hold
for a recovery step $t_r > t_c$, message keys after~$t_r$ are fresh.
\end{theorem}

\begin{proofsketch}
After corruption at $t_c$, the adversary can forward-derive ratchet
state through epochs where it holds the decapsulator's secret key
$\sk_s$ (obtained from the corrupted state or from a KEM step it can
invert). This derivation chain terminates at the first step~$t_r$ where
$\sk_s$ was generated with uncompromised RNG (F4): the adversary cannot
compute $\mathit{ss}' = \Decaps(\sk_{s_{t_r}}, c_{\text{ratchet}})$
because $\sk_{s_{t_r}}$ is unknown. The IND-CCA2 reduction embeds its
challenge at this step, replacing $\mathit{ss}'$ with a uniformly random
value. From $\KDF_{\text{Root}}(\rk, \mathit{ss}')$, the output
$(\rk', \ek)$ is indistinguishable from uniform by the HKDF extractor
property. Recovery requires two direction changes in the worst case:
the first fails because the adversary holds the compromised party's
$\sk_s$; the second succeeds because the compromised party generates a
fresh keypair and encapsulates to the peer's post-compromise public key.
F4 prevents chain-injection attacks where the adversary substitutes
controlled public keys to extend compromise indefinitely.
\end{proofsketch}

\subsection{Authentication and domain separation (Theorems 6--7)}

\begin{theorem}[Auth Key Possession]\label{thm:auth}
Under active attack (Dolev-Yao channel), where the adversary may modify
or replay challenges, interleave LO-Auth sessions with LO-KEX sessions
(obtaining additional $\Decaps$ oracle queries on
$\sk_{\text{IK}}[\text{XWing}]$), and relay challenges across sessions:
if $\mathsf{auth\_verify}(\mathit{expected\_token}, \mathit{proof})$
returns true for a fresh challenge, the client possesses
$\sk_{\text{IK}}[\text{XWing}]$. Reduces to X-Wing IND-CCA2 +
HMAC-SHA3-256 PRF.
\end{theorem}

\begin{theorem}[Domain Separation]\label{thm:domain-sep}
No output from one protocol component is valid in another. Follows from
disjoint labels and non-overlapping AAD prefixes. An Encode disjointness
sub-lemma establishes a minimum 1196-byte gap between session-init and
ratchet-message encodings.
\end{theorem}

\subsection{Call security (Theorems 8--11)}

\begin{theorem}[Call Key Secrecy]\label{thm:call-secrecy}
Fresh call keys are indistinguishable from random. Reduces to X-Wing
IND-CCA2 + HKDF extractor.
\end{theorem}

\begin{theorem}[Intra-Call Forward Secrecy]\label{thm:call-fs}
Call chain advance is one-way. Reduces to HMAC-SHA3-256 PRF.
\end{theorem}

\begin{theorem}[Call/Ratchet Independence]\label{thm:call-ratchet}
$\mathsf{Corrupt}(\text{CallKeys})$ does not violate ratchet secrecy;
$\mathsf{Corrupt}(\text{RatchetState})$ after call derivation does not
reveal call keys.
\end{theorem}

\begin{proofsketch}
The ephemeral keypair $(\pk_{\text{eph}}, \sk_{\text{eph}})$ and shared
secret $\mathit{ss}_{\text{eph}}$ are generated within call setup and
zeroized after HKDF --- they are not part of the ratchet state~$\Sigma$.
Therefore $\mathsf{Corrupt}(\text{RatchetState})$ does not yield
$\mathit{ss}_{\text{eph}}$; recovering it from the public
$c_{\text{eph}}$ requires breaking X-Wing IND-CCA2. The dual-use of
$\rk$ as HKDF salt in both $\KDF_{\text{Root}}$ (ratchet) and
$\KDF_{\text{Call}}$ (call) is safe via a hybrid argument: under the
dual-PRF assumption, $\HKDF$-Extract produces a pseudorandom PRK, and
$\HKDF$-Expand keyed by PRK with distinct info strings
(\texttt{"lo-ratchet-v1"} vs \texttt{"lo-call-v1"}) produces
independent outputs by the PRF guarantee. Security loss is additive
(one PRF advantage term per HKDF invocation sharing the same salt).
\end{proofsketch}

\begin{theorem}[Concurrent Call Independence]\label{thm:concurrent}
Calls with distinct $\mathit{call\_id}$ values under the same~$\rk$
have jointly independent keys. Security loss is additive.
\end{theorem}

\subsection{Anti-reflection and streaming (Theorems 12--13)}

\begin{theorem}[Anti-Reflection]\label{thm:anti-reflect}
Reflected messages fail AEAD verification. Reduces to INT-CTXT under
invariant~(h).
\end{theorem}

\begin{theorem}[Streaming AEAD Chunk Security]\label{thm:stream}
For a stream with fresh key and fresh base nonce:
\begin{enumerate}[label=\textbf{P\arabic*.}, leftmargin=*, itemsep=2pt]
\item \textbf{Confidentiality} (IND-CPA): Per-chunk indistinguishability.
  Aggregate advantage $Q \times \Adv_{\text{IND-CPA}}$, giving
  ${\approx}128 - \log_2(Q)$ effective bits.
\item \textbf{Integrity} (INT-CTXT): No forgery. No $Q$-factor loss.
\item \textbf{Ordering}: Mismatched sequential position causes nonce
  mismatch and AEAD failure.
\item \textbf{No false finalization}: $\mathit{tag\_byte}$ in both
  nonce and AAD prevents finality confusion.
\item \textbf{Cross-stream isolation}: Different $\mathit{base\_nonce}$
  guarantees different AADs unconditionally.
\end{enumerate}
\end{theorem}

\noindent\textbf{Non-goal}: No forward secrecy claim.
$\mathsf{Corrupt}(\text{StreamKey})$ retroactively compromises all
chunks.

\subsection{Concrete security bounds}\label{sec:bounds}

The CryptoVerif models yield the following bounds (simplified; full
expressions in \Cref{app:cryptoverif}):

\begin{center}
\small
\begin{tabular}{@{} l l @{}}
\toprule
\textbf{Theorem} & \textbf{Bound} \\
\midrule
1 (KEX Secrecy) & $2P_{\text{prf}} + 2P_{\text{kem}}^{\text{ik}}
  + 2P_{\text{kem}}^{\text{spk}} + 2P_{\text{kem}}^{\text{opk}}
  + \text{coll.}$ \\
2b (Initiator Auth) & $P_{\text{sig}}$ \\
3 (Message Secrecy) & $2P_{\text{prf}}$ \\
6 (Auth) & $N_s \cdot P_{\text{mac}} + P_{\text{kem}}$ \\
13 P1 (IND-CPA) & $2P_{\text{ctxt}} + 2P_{\text{cpa}}(t, N_{\text{enc}})$ \\
13 P2 (INT-CTXT) & $P_{\text{ctxt}}$ \\
\bottomrule
\end{tabular}
\end{center}

\noindent Theorem~3's $2P_{\text{prf}}$ assumes a fresh epoch key
(\emph{epoch key freshness assumption}): $\ek$ is indistinguishable from
uniform, which follows from Theorem~1 at session establishment and from
the KDF\_Root output independence lemma at each subsequent KEM ratchet
step (HKDF-Expand with a pseudorandom PRK produces independent 32-byte
blocks under the PRF assumption). The multi-epoch bound is additive:
each epoch contributes one $2P_{\text{prf}}$ term, and epoch keys are
pairwise independent by the cross-epoch key independence corollary.
This composition is not mechanically end-to-end verified.
Theorem~13 P2 has no $Q$-factor (direct reduction). For multi-stream
nonce uniqueness: probability $\geq 1 - (\sum M_i)^2 / 2^{193}$.

\subsection{Composition argument}\label{sec:composition}

A full mechanized composition theorem (showing all 13~security properties hold
simultaneously under compound corruption) remains open
(\Cref{sec:limitations}). However, composed security follows from the
individual theorems via three structural properties.

First, \textbf{domain separation} (Theorem~\ref{thm:domain-sep}):
disjoint HKDF info strings and AAD prefixes ensure that no output from
one sub-protocol is valid in another. An adversary who obtains, for
example, a call chain key cannot use it to forge a ratchet message ---
the HMAC domain bytes are disjoint (\texttt{0x01} for ratchet,
\texttt{0x04}--\texttt{0x06} for calls), and the primary separation is
by key: $\KDF_{\text{MsgKey}}$ and $\KDF_{\text{CallChain}}$ operate on
independent HMAC keys.

Second, \textbf{independent key material}: each sub-protocol derives its
keys from independent sources. Call keys depend on an ephemeral KEM
shared secret $\mathit{ss}_{\text{eph}}$ that is not part of~$\Sigma$
(Theorem~\ref{thm:call-ratchet}). Stream keys are caller-provided and
independent of ratchet state by construction. The LO-Auth token depends
on a fresh KEM challenge, not on ratchet material. Cross-component
corruption therefore does not create transitive compromise paths beyond
those already captured by the individual freshness predicates.

Third, \textbf{additive security loss}: the pairwise composition results
(KEX$\to$Ratchet via the $\KDF_{\text{Root}}$ output independence lemma;
Ratchet$\to$Call via Theorem~\ref{thm:call-ratchet}'s dual-PRF argument)
show that the combined security loss is additive across protocol layers,
not multiplicative. The remaining gap --- verifying that compound
corruption schedules spanning all three layers do not create interference
between these pairwise arguments --- is explicitly identified as an open
research direction.


% ============================================================================
% 6. FORMAL VERIFICATION
% ============================================================================
\section{Formal verification}\label{sec:verification}

All models are machine-checkable and published in the project
repository~\cite{soliton-repo}. Independent verification is encouraged.

\subsection{Symbolic verification (Tamarin)}\label{sec:tamarin}

Eight Tamarin models verify 55~lemmas covering Theorems~1--2, 4--6,
8--13. All complete in under 90~seconds total with under 2~GB peak RAM,
achieved through bounded unrolling (3--4 steps) and unique fact names.

\begin{table}[H]
\centering
\caption{Tamarin model summary. \emph{f} = falsified (expected).}
\label{tab:tamarin-summary}
\small
\begin{tabular}{@{} l c c l @{}}
\toprule
\textbf{Model} & \textbf{Lemmas} & \textbf{Theorems} &
  \textbf{Key results} \\
\midrule
LO\_KEX & 9 & 1, 2a, 2b &
  Session key secrecy, authentication \\
LO\_Ratchet & 9 & 4, 5 &
  FS (structural); recv\_fs\_1step \emph{f} \\
LO\_Ratchet\_PCS & 5 & 5 &
  KEM-level PCS recovery \\
LO\_Auth & 7 & 6 &
  Key possession correspondence \\
LO\_Call & 6 & 8--11 &
  Call key secrecy, independence \\
LO\_AntiReflection & 2 & 12 &
  AAD direction binding \\
LO\_Stream & 7 & 13 P2--P5 &
  Integrity, ordering, isolation \\
LO\_NegativeTests & 10 & --- &
  10 expected attack paths confirmed \\
\bottomrule
\end{tabular}
\end{table}

\paragraph{Negative tests.}
Ten lemmas confirm known attack paths (IK corruption forges auth,
zero-step corruption reveals epoch key, etc.). All produce expected
results. If any were to flip, it would indicate a modeling error.

\paragraph{Scope.}
X-Wing is a black-box IND-CCA2 KEM. Chains bounded to 3--4 steps. KEX
models OPK-present only. Theorem~7 is vacuously true (string constants
are structurally distinct). Theorem~3 is computational (CryptoVerif).

\subsection{Computational verification (CryptoVerif)}\label{sec:cryptoverif}

Five models prove concrete bounds for Theorems~1, 2b, 3, 6, and
13~(P1+P2), completing in under 5~seconds total.

\begin{table}[H]
\centering
\caption{CryptoVerif model summary.}
\label{tab:cv-summary}
\small
\begin{tabular}{@{} l l l @{}}
\toprule
\textbf{Model} & \textbf{Theorem} & \textbf{What is proved} \\
\midrule
LO\_KEX\_Secrecy & 1 & $\rk$ indistinguishable from random \\
LO\_KEX & 2b & $\sigma_{\text{SI}}$ authentication (EUF-CMA) \\
LO\_Ratchet\_MsgSecrecy & 3 & $\mk$ indistinguishable from random \\
LO\_Auth & 6 & Correspondence + injective \\
LO\_Stream\_Secrecy & 13 P1+P2 & Bit secrecy + INT-CTXT \\
\bottomrule
\end{tabular}
\end{table}

\paragraph{Scope.}
No corruption oracles (Tamarin covers these). X-Wing as monolithic
IND-CCA2. Simplified KDF info binding. Single-epoch assumption for
Theorem~3. No Theorem~2c/2d. Streaming model adapted from CryptoVerif's
TLS~1.3 Record Protocol example.

\subsection{Coverage analysis}\label{sec:coverage}

\begin{table}[H]
\centering
\caption{Theorem coverage by verification tool.}
\label{tab:coverage}
\small
\begin{tabular}{@{} c l c c @{}}
\toprule
\textbf{Thm} & \textbf{Property} & \textbf{Tamarin} & \textbf{CV} \\
\midrule
1 & KEX Key Secrecy & \checkmark & \checkmark \\
2a & Recipient Auth & \checkmark & --- \\
2b & Initiator Auth & \checkmark & \checkmark \\
2c/d & Key Confirmation & --- & --- \\
3 & Message Secrecy & --- & \checkmark \\
4 & Forward Secrecy & \checkmark & --- \\
5 & PCS & \checkmark & --- \\
6 & Auth Key Possession & \checkmark & \checkmark \\
7 & Domain Separation & (vacuous) & --- \\
8 & Call Key Secrecy & \checkmark & --- \\
9 & Intra-Call FS & \checkmark & --- \\
10 & Call/Ratchet Indep. & \checkmark & --- \\
11 & Concurrent Calls & \checkmark & --- \\
12 & Anti-Reflection & \checkmark & --- \\
13 & Streaming AEAD & \checkmark\,(P2--5) & \checkmark\,(P1+2) \\
\bottomrule
\end{tabular}
\end{table}

\subsection{Reproducibility}\label{sec:reproducibility}

All models verified with Tamarin~1.12.0 (Maude~3.5.1) and
CryptoVerif~2.12:

\begin{verbatim}
../verify.sh tamarin          # all 8 Tamarin models
CV_LIB=/path/to/pq ../verify.sh cryptoverif  # all 5 CV models
\end{verbatim}


% ============================================================================
% 7. IMPLEMENTATION
% ============================================================================
\section{Implementation}\label{sec:implementation}

\subsection{Architecture}

The reference implementation, \texttt{libsoliton}, is a pure Rust
library with no C~toolchain dependency. Binding layers are provided for
C~ABI (\texttt{cbindgen}), Python (PyO3), WASM (wasm-bindgen), and Zig
(\texttt{@cImport}). Sensitive key material is protected via
\texttt{ZeroizeOnDrop}. Fork prevention is enforced by destructive
serialization, and an anti-rollback counter prevents state replay.

\subsection{Performance}\label{sec:performance}

\begin{table}[H]
\centering
\caption{Representative benchmarks (\texttt{cargo +nightly bench}).}
\label{tab:bench}
\small
\begin{tabular}{@{} l r r r @{}}
\toprule
\textbf{Operation} &
  \textbf{x86-64} & \textbf{aarch64} & \textbf{riscv64} \\
  & \small{Zen\,4, 5.1\,GHz} &
  \small{A76, 2.4\,GHz} &
  \small{U74, 1.5\,GHz} \\
\midrule
Ratchet encrypt (same epoch) & 4.3\,$\mu$s & 7.2\,$\mu$s & 47.6\,$\mu$s \\
Ratchet decrypt (same epoch) & 6.2\,$\mu$s & 10.1\,$\mu$s & 67.5\,$\mu$s \\
Encrypt (direction change) & 182\,$\mu$s & 651\,$\mu$s & 2.46\,ms \\
Decrypt (direction change) & 127\,$\mu$s & 473\,$\mu$s & 1.76\,ms \\
Session initiate & 1.41\,ms & 3.95\,ms & 17.1\,ms \\
Session receive & 585\,$\mu$s & 1.88\,ms & 7.70\,ms \\
Hybrid sign & 988\,$\mu$s & 2.85\,ms & 10.6\,ms \\
Hybrid verify & 254\,$\mu$s & 794\,$\mu$s & 3.31\,ms \\
Stream encrypt 1\,MiB & 537\,$\mu$s & 3.96\,ms & 31.0\,ms \\
Stream 4\,MiB (parallel, 4 cores) & 867\,$\mu$s & 5.35\,ms & 33.0\,ms \\
\bottomrule
\end{tabular}
\end{table}

\noindent Per-message latency is 4.3\,$\mu$s on desktop (same epoch).
Direction changes are ${\sim}40\times$ slower due to X-Wing keygen +
encapsulation. Streaming AEAD achieves 1.95\,GB/s sequential and
4.61\,GB/s parallel on desktop. ML-DSA-65 and SHA3-256 lack SIMD in
current RustCrypto crates; these numbers will improve.

\subsection{Testing and fuzzing}\label{sec:testing}

956~tests across all binding layers (488~core unit, 61~integration,
287~CAPI, 49~Python, 35~Zig, 36~WASM), plus 36~fuzz targets with a
165,540-entry corpus (883\,MB). A 24-hour campaign on a 32-vCPU server
executed 574.6~billion iterations with zero crashes, timeouts, or OOM
events. The 31~active targets achieve 172--12,714 libFuzzer edge
coverage features per target (median ${\sim}1{,}100$); the
state-machine fuzzer covers 12,714~features across full cryptographic
sessions with up to 200~actions per execution. 455~tests run under MIRI
for undefined-behavior detection. 27~KAT vectors
cross-validate against the specification~\cite{soliton-spec}.

\subsection{License}

\texttt{libsoliton} is released under AGPL-3.0-only. Applications using
the library in a network service must release their source code. Users
should evaluate this constraint before adoption.


% ============================================================================
% 8. DESIGN RATIONALE
% ============================================================================
\section{Design rationale}\label{sec:rationale}

\subsection{Counter-mode vs.\ chain-mode key derivation}

The standard double ratchet derives message keys by iterating a
symmetric ratchet: $\mathit{ck}_{i+1}, \mk_i = \KDF(\mathit{ck}_i)$.
Decrypting message~$n$ requires $n$~iterations or a skip cache.
Soliton uses $\mk_i = \MAC(\ek, \texttt{0x01} \| \mathsf{BE32}(i))$
--- $O(1)$ derivation with no skip cache. The trade-off: forward
secrecy drops from per-message to per-epoch. This is acceptable because
$\ek$ and $\rk$ share the same memory and compromise granularity ---
an adversary who reads $\ek$ can also read $\rk$, which is strictly
more damaging. Per-message chain advancement provides limited practical benefit
under this deployment assumption, where the chain key shares a trust
domain with the root key.

\subsection{Unified X-Wing vs.\ parallel ratchets}

Signal's SPQR~\cite{signal-spqr} (based on~\cite{djkps25}) runs two independent ratchets
and combines their outputs, providing a compositional guarantee: if
either is secure, the combined output is secure. Soliton uses a single
X-Wing ratchet that inherently combines X25519 and ML-KEM-768. The
trade-off: if X-Wing's combiner had a subtle flaw causing component
interference, both would fail together. I consider this acceptable given
X-Wing's published analysis~\cite{xwing} and the simplicity benefit ---
one ratchet state, one KEM operation per direction change, one code
path.

A consequence of KEM-based ratcheting (whether unified or parallel) is
\textbf{single-sided freshness}: only the encapsulator contributes
fresh randomness to the KEM shared secret, whereas a DH ratchet step
has both parties contributing symmetrically. This means post-compromise
recovery requires two direction changes in the worst case
(Theorem~\ref{thm:pcs}), compared to one for DH ratchets. This is an
inherent property of all KEM-based ratchet designs~\cite{acd19}, not
specific to Soliton.

\subsection{Post-quantum authentication}

All deployed PQ messaging retains classical-only authentication. A
quantum adversary breaking the signature scheme can forge session
initiations. Soliton's hybrid scheme ensures authentication survives if
either component is secure.

\paragraph{Why \texttt{sign\_internal}, not the FIPS~204 public API.}
Soliton uses \texttt{sign\_internal} (FIPS~204 \S6.2) rather than the
external \texttt{ML-DSA.Sign} wrapper (\S5.2) for two reasons.
First, \texttt{sign\_internal} accepts the \texttt{rnd} parameter
directly, enabling hedged signing with 32~bytes of fresh
\texttt{getrandom} entropy per call --- providing fault-injection
resistance that deterministic signing lacks. Second, the \S5.2
public API unconditionally prepends a \texttt{0x00} domain separator
byte and context string \emph{even when the context is empty}:
$\texttt{Sign}(\sk, \texttt{""}, m)$ signs
$\texttt{0x00} \| \texttt{0x00} \| m$, not~$m$. Passing an empty
context is therefore \emph{not} equivalent to calling
\texttt{sign\_internal} --- it changes the signed message. Since
Soliton handles domain separation at the protocol level (unique
per-context labels in every signed payload), the \S5.2 wrapper's
domain separator is redundant and would require all reimplementers
to match the exact wrapping behavior.

\paragraph{FIPS-mode deployment.}
This choice makes Soliton ML-DSA-65 signatures incompatible with
standalone FIPS~204-conformant verifiers (and vice versa).
Deployments subject to FIPS~140 or FIPS~204 compliance requirements
cannot use Soliton signatures in their current form. If a future
NIST policy restricts access to \texttt{sign\_internal}, migrating
to the \S5.2 interface requires a protocol version bump
(\texttt{lo-crypto-v2}), updated test vectors, and adjusting the
signed payload to account for the prepended domain separator ---
but no structural redesign.

\subsection{Deniability trade-off}

Soliton's session-init signature $\sigma_{\text{SI}}$ is transferable
proof that Alice initiated the session --- a deliberate departure from
Signal's X3DH, which achieves deniability through DH-based key
agreement (no signatures on session initiation).  KEM-based protocols
inherently struggle with deniability: the encapsulator produces a
unique ciphertext that constitutes a cryptographic receipt, and the
hybrid signature makes this explicit.  Fiedler and
Janson~\cite{fiedler-janson24} characterize this as a fundamental
tension in KEM-based handshakes.

For Soliton's target deployment (a private communications platform
where users authenticate via identity keys stored on their devices),
transferable authentication is acceptable --- and arguably desirable,
as it simplifies the trust model.  Deniability would require either a
designated-verifier signature scheme (adding complexity and a new
cryptographic assumption) or ring-signature--based constructions
(substantial overhead with PQ ring signatures).  Neither is pursued in
v1; the trade-off is explicit.


% ============================================================================
% 9. RELATED WORK
% ============================================================================
\section{Related work}\label{sec:related}

\Cref{tab:comparison} compares Soliton with deployed PQ messaging
protocols across key dimensions. Per-message overhead reflects the
ratchet header transmitted with each message; session establishment
overhead reflects the initial handshake.

\begin{table}[!htbp]
\centering
\caption{Comparison with deployed post-quantum messaging protocols.}
\label{tab:comparison}
\small
\setlength{\tabcolsep}{3.5pt}
\begin{tabular}{@{} l c c c c @{}}
\toprule
& \textbf{Soliton} & \textbf{Signal} & \textbf{Signal} & \textbf{Apple} \\
& & \textbf{PQXDH} & \textbf{SPQR} & \textbf{PQ3} \\
\midrule
PQ key exchange & \checkmark & \checkmark & \checkmark & \checkmark \\
PQ ratchet & \checkmark & --- & \checkmark & Periodic \\
PQ authentication & \checkmark & --- & --- & --- \\
Ratchet type & KEM & DH & DH+KEM & ECDH+KEM \\
\midrule
Header (no KEM step) & 1225\,B & 33\,B & 33\,B & 33\,B \\
Header (KEM step) & 2347\,B & 33\,B & ${\sim}75$\,B & 1125\,B \\
Session init & 4669\,B & ${\sim}4$\,KB & ${\sim}4$\,KB & --- \\
\midrule
Formal verif.\ tool(s) & Tam.+CV & PV+CV & --- & Tamarin \\
Formal verif.\ scope & Full & KEX & --- & KEX+Ratchet \\
Theorems/lemmas & 13/55 & ${\sim}$8 & --- & ${\sim}$15--30 \\
\midrule
Deniability & --- & ---$^{\dagger}$ & ---$^{\dagger}$ & --- \\
Per-message FS & Per-epoch & Per-msg & Per-msg & Per-msg \\
\bottomrule
\end{tabular}

\smallskip
{\scriptsize $^{\dagger}$PQXDH and SPQR lose X3DH's full deniability
guarantees~\cite{fiedler-janson24} (KEM ciphertexts are attributable),
but retain weaker deniability than Soliton: they do not place explicit
signatures on session initiation. Soliton's $\sigma_{\text{SI}}$ is
transferable proof of initiation.}
\end{table}

\noindent Soliton's per-message overhead (1225--2347~bytes) is
substantially larger than Signal's (33~bytes) due to the 1216-byte
X-Wing public key transmitted in every ratchet header. This is the
fundamental bandwidth cost of a KEM-based ratchet: unlike DH, where the
public key is 32~bytes, X-Wing public keys are 38$\times$ larger. SPQR
amortizes this via erasure-coded chunking of ML-KEM keys across
messages, achieving ${\sim}75$-byte per-message overhead at the cost of
requiring multiple messages for a complete KEM ratchet step. Soliton
does not amortize; each direction change is self-contained in a single
message. In practice, the 1225-byte overhead is modest relative to
typical network traffic --- modern web requests routinely transmit
tens of kilobytes of metadata per interaction, and mobile messaging
payloads (including media thumbnails, typing indicators, and delivery
receipts) dwarf the ratchet header. The overhead is significant
primarily for extremely constrained links or high-frequency
machine-to-machine messaging, neither of which is the target
deployment. The Auerbach \etal VulM framework~\cite{adjks25} provides
a rigorous methodology for quantifying these trade-offs under
realistic messaging patterns; applying it to Soliton is future work.

\subsection{Post-quantum key exchange for messaging}

Signal introduced PQXDH~\cite{signal-pqxdh} in 2023, adding ML-KEM to
X3DH while retaining classical DH. Bhargavan
\etal~\cite{bjks24} provided formal verification (USENIX Security 2024).
Fiedler and Janson~\cite{fiedler-janson24} showed PQXDH loses X3DH's
deniability guarantees. Hashimoto \etal~\cite{hks22} gave the first
efficient generic PQ~X3DH construction. Brendel \etal~\cite{bfg20}
introduced split KEMs. Apple deployed PQ3~\cite{apple-pq3} with periodic
KEM rekeying; Linker \etal~\cite{lsb25} provided a Tamarin analysis
(USENIX Security 2025).

\subsection{KEM-based ratcheting}

Alwen \etal~\cite{acd19} decomposed the double ratchet into CKA,
FS-AEAD, and PRF-PRNGs, showing CKA from any KEM (EUROCRYPT 2019).
Signal's SPQR~\cite{djkps25} introduced Katana, a novel RKEM with
${\sim}40\%$ size savings (EUROCRYPT 2025). Auerbach
\etal~\cite{adjks25} introduced the VulM metric for comparing PQ
ratchet protocols (USENIX Security 2025). Cremers
\etal~\cite{cmn25} proved PCS impossibility results (IEEE S\&P 2025).

\subsection{X-Wing and hybrid KEMs}

Barbosa \etal~\cite{xwing} proved X-Wing IND-CCA2 (IACR CiC 2024). The
IETF draft progressed to draft-10~\cite{xwing-ietf}. Follow-up work
examined broader applicability~\cite{starfighters25},
anonymity~\cite{bp26}, and public context
requirements~\cite{kls26}.

\subsection{Formal verification of messaging protocols}

Cohn-Gordon \etal~\cite{cgcd20} established the foundational Signal
analysis. Blanchet and Jacomme~\cite{bj24} proved post-quantum soundness
of CryptoVerif (CSF 2024). B\'eguinet \etal~\cite{bcrs24} gave the
first symbolic proof of a KEM-based Signal variant. Soliton's
55~Tamarin lemmas and 7~CryptoVerif queries across 13~models represent
among the most extensive formal verification efforts applied to a
KEM-based messaging protocol in the published literature (\Cref{tab:comparison}). The combination of
symbolic and computational verification for a full protocol (handshake
through streaming) is new.

\subsection{Streaming AEAD}

STREAM~\cite{hrrv15} (CRYPTO 2015) is the theoretical foundation. Hoang
and Shen~\cite{hs20} extended to random-access decryption for Google
Tink (CCS 2020). Fabrega \etal~\cite{floe25} introduced FLOE with
formal random-access encryption and commitment security (RWC 2026).
LO-Stream's dual-interface design in a messaging context appears novel.

\subsection{Group messaging and other protocols}

The Messaging Layer Security (MLS) protocol~\cite{rfc9420} addresses
group messaging with tree-based key agreement. Post-quantum MLS
ciphersuites using X-Wing have been implemented in
OpenMLS. Matrix's Megolm protocol provides group
encryption for the Matrix ecosystem but has no PQ features at the E2EE
layer. Zoom added ML-KEM for initial key encapsulation in 2024 but
provides no ongoing PQ ratcheting. Soliton is strictly two-party and
does not address group messaging.


% ============================================================================
% 10. LIMITATIONS AND OPEN PROBLEMS
% ============================================================================
\section{Limitations and open problems}\label{sec:limitations}

Transparency about what has \emph{not} been proved is as important as
stating what has. The formal models and this paper were authored by the
protocol designer, assisted by AI (\Cref{sec:contributions}), and have
not undergone independent peer review. All results are
machine-checkable; independent verification is actively invited.

\subsection{Verification gaps}

\textbf{No full composition theorem.} Individual theorems and pairwise
compositions are established, but simultaneous correctness under
compound corruption spanning all protocol layers remains open.

\textbf{No Theorem~2c/2d mechanization.} Key confirmation requires a
combined KEX+Ratchet model.

\textbf{Single-epoch assumption.} CryptoVerif's Theorem~3 assumes a
fresh epoch key (\emph{epoch key freshness assumption}). Multi-epoch
security follows from the additive composition of per-epoch bounds under
the KDF\_Root output independence lemma and cross-epoch key independence
corollary (see \cref{sec:bounds}), but this chain is not
mechanically end-to-end verified.

\textbf{X-Wing as black box.} Opening the combiner would yield tighter
bounds.

\textbf{Bounded chains.} Tamarin bounds steps to 3--4. Unbounded
verification is feasible~\cite{lsb25} but resource-intensive.

\subsection{Protocol limitations}

\textbf{No deniability} --- KEM ciphertexts and $\sigma_{\text{SI}}$ are
attributable~\cite{fiedler-janson24}.
\textbf{OPK-absent security regression} --- without OPK, session
establishment forward secrecy depends solely on SPK rotation; corruption
of $\sk_{\text{IK}_B}$ and $\sk_{\text{SPK}_B}$ together suffices to
derive the session key. Deployments without a pre-key server should
treat OPK unavailability as a materially weaker security configuration.
\textbf{No group messaging} --- strictly two-party.
\textbf{Per-epoch FS only} --- counter-mode trades per-message FS for
$O(1)$ access. An epoch lasts until a direction change; in one-sided
conversations, a single epoch may span many messages over an extended
period, all derivable from the same~$\ek$.
\textbf{X-Wing not standardized} --- still an IETF draft.
\textbf{Metadata exposure} --- headers reveal epoch transitions and
message counts.

\subsection{Open research directions}

The formal analysis document~\cite{soliton-analysis} identifies specific
targets: full composition under compound corruption, OPK atomicity,
SPK rotation lifecycle, counter-mode vs.\ chain-mode formal comparison,
and bandwidth analysis via the VulM framework~\cite{adjks25}.
Applicability of Katana-style amortization~\cite{djkps25} to X-Wing is
open: Katana requires a Randomizable KEM (RKEM) interface that allows
ciphertext splitting across messages, and X-Wing's combiner structure
(X25519~+~ML-KEM-768 fed into SHA3-256) is not obviously compatible
with the RKEM abstraction.


% ============================================================================
% 11. CONCLUSION
% ============================================================================
\section{Conclusion}\label{sec:conclusion}

I have presented Soliton, an end-to-end encrypted messaging protocol
providing hybrid classical/post-quantum security across key exchange,
ratcheting, authentication, call encryption, and streaming AEAD. No
existing asynchronous two-party E2EE messaging protocol provides
post-quantum authentication --- PQXDH, SPQR, and PQ3 all retain
classical-only signatures. Soliton's 55~Tamarin lemmas and
7~CryptoVerif queries across 13~models represent the most extensive
published formal verification of a KEM-based messaging protocol,
and the first to combine both symbolic and computational verification
for a full protocol lifecycle.

The protocol makes deliberate trade-offs --- per-epoch forward secrecy,
unified X-Wing ratcheting, no deniability --- each motivated by
simplicity and practical deployability. These trade-offs and their
security implications are documented, and the open problems they create
are explicitly identified.

The full specification, formal analysis, Tamarin and CryptoVerif models,
and Rust implementation are published at
\url{https://git.lo.sh/lo/libsoliton} under AGPL-3.0. Everything
claimed in this paper is machine-checkable. I invite independent
verification, critique, and analysis.


% ============================================================================
% APPENDICES
% ============================================================================
\clearpage
\appendix

\section{Tamarin lemma results}\label{app:tamarin}

\begin{table}[!htbp]
\centering
\caption{Complete Tamarin results (Tamarin 1.12.0, Maude 3.5.1).
  \textbf{Bold} = falsified (expected).}
\label{tab:tamarin-full}
\small
\setlength{\tabcolsep}{4pt}
\begin{tabular}{@{} l l c r @{}}
\toprule
\textbf{Model} & \textbf{Lemma} & \textbf{Result} & \textbf{Steps} \\
\midrule
LO\_KEX & KEX\_Exists & verified & 27 \\
 & Thm1\_Session\_Key\_Secrecy\_A & verified & 70 \\
 & Thm1\_Session\_Key\_Secrecy\_B & verified & 136 \\
 & Thm1\_EK\_Secrecy\_A & verified & 70 \\
 & Thm1\_EK\_Secrecy\_B & verified & 136 \\
 & Thm2a\_Recipient\_Binding & verified & 2 \\
 & Thm2b\_Initiator\_Auth & verified & 10 \\
 & OPK\_Single\_Use & verified & 24 \\
 & Key\_Uniqueness & verified & 2 \\
\midrule
LO\_Ratchet & send\_sanity & verified & 7 \\
 & send\_fs & verified & 2818 \\
 & send\_corrupt\_terminates & verified & 193 \\
 & send\_pcs & verified & 2 \\
 & recv\_sanity & verified & 6 \\
 & recv\_fs\_1step & \textbf{falsified} & 11 \\
 & recv\_fs\_2step & verified & 9132 \\
 & recv\_corrupt\_terminates & verified & 273 \\
 & recv\_pcs & verified & 107 \\
\midrule
LO\_Ratchet\_PCS & pcs\_sanity & verified & 3 \\
 & pcs\_no\_recovery\_after\_recv & \textbf{falsified} & 9 \\
 & pcs\_recovery\_after\_send & verified & 7 \\
 & pcs\_recovery\_sustained & verified & 15 \\
 & pcs\_f4\_violated & verified & 7 \\
\midrule
LO\_Auth & Auth\_Exists & verified & 5 \\
 & Auth\_Ordering & verified & 2 \\
 & Auth\_Single\_Use & verified & 8 \\
 & Auth\_No\_Accept\_After\_Timeout & verified & 3 \\
 & Auth\_Unique\_Challenge & verified & 2 \\
 & Thm6\_Key\_Possession & verified & 11 \\
 & Thm6\_No\_Oracle & verified & 11 \\
\midrule
LO\_Call & Call\_Exists & verified & 6 \\
 & Call\_Key\_Agreement & verified & 56 \\
 & Thm8\_Call\_Key\_Secrecy & verified & 24 \\
 & Thm9\_Intra\_Call\_FS & verified & 193 \\
 & Thm10\_Call\_Ratchet\_Ind & verified & 3 \\
 & Thm11\_Concurrent\_Ind & verified & 52 \\
\midrule
LO\_AntiRefl. & Reflection\_Sanity & verified & 8 \\
 & Thm12\_Anti\_Reflection & verified & 5 \\
\midrule
LO\_Stream & Stream\_Sanity & verified & 11 \\
 & Stream\_Sanity\_Finalize & verified & 7 \\
 & Thm13\_P2\_Integrity & verified & 28 \\
 & Thm13\_P3\_Ordering & verified & 18 \\
 & Thm13\_P4\_No\_False\_Final & verified & 17 \\
 & Thm13\_P5\_Cross\_Stream & verified & 55 \\
 & Thm13\_Key\_Secrecy & verified & 3 \\
\midrule
LO\_NegativeTests & neg\_auth\_ik\_corrupt & \textbf{falsified} & 8 \\
 & neg\_auth\_rng\_corrupt & \textbf{falsified} & 10 \\
 & neg\_ratchet\_no\_fs\_0step & \textbf{falsified} & 8 \\
 & neg\_ratchet\_recv\_1step & \textbf{falsified} & 10 \\
 & neg\_call\_rk\_plus\_rng & \textbf{falsified} & 9 \\
 & neg\_stream\_key\_corrupt & \textbf{falsified} & 5 \\
 & neg\_reflect\_self\_session & \textbf{falsified} & 7 \\
 & neg\_kex\_no\_opk & \textbf{falsified} & 11 \\
 & neg\_ratchet\_duplicate & \textbf{falsified} & 7 \\
 & neg\_call\_self\_session & verified\textsuperscript{*} & 3 \\
\bottomrule
\end{tabular}

\smallskip
{\scriptsize $^*$\texttt{neg\_call\_self\_session} is an
\texttt{exists-trace} lemma (not all-traces): it confirms that
self-sessions are \emph{reachable} when the $\mathit{local\_fp} \neq
\mathit{remote\_fp}$ guard is absent, demonstrating the guard is
necessary. ``Verified'' is the expected outcome.}
\end{table}


\section{CryptoVerif query results}\label{app:cryptoverif}

\begin{table}[!htbp]
\centering
\caption{CryptoVerif results (CryptoVerif 2.12).}
\label{tab:cv-full}
\small
\begin{tabular}{@{} l l l @{}}
\toprule
\textbf{Model} & \textbf{Query} & \textbf{Bound} \\
\midrule
LO\_KEX\_Secrecy
  & $\mathsf{secret}\ \rk_A$ \texttt{[cv\_onesession]}
  & $2P_{\text{prf}} {+} 2P_{\text{kem}}^{\text{ik}} {+}
    2P_{\text{kem}}^{\text{spk}} {+} 2P_{\text{kem}}^{\text{opk}} {+}
    \text{coll.}$ \\
LO\_KEX
  & $\mathsf{event}(\text{Bob\_Accept}) {\Rightarrow}
    \mathsf{event}(\text{Alice\_Init})$
  & $P_{\text{sig}}$ \\
LO\_Ratchet\_MsgSecrecy
  & $\mathsf{secret}\ \mathit{test\_mk}$
    \texttt{[cv\_onesession]}
  & $2P_{\text{prf}}$ \\
LO\_Auth
  & $\mathsf{event}(\text{ServerAccepts}) {\Rightarrow}
    \mathsf{event}(\text{ClientResponds})$
  & $N_s {\cdot} P_{\text{mac}} {+} P_{\text{kem}}$ \\
LO\_Auth
  & $\mathsf{inj\text{-}event}(\text{ServerAccepts}) {\Rightarrow}
    \mathsf{inj\text{-}event}(\text{ClientResponds})$
  & $N_s {\cdot} P_{\text{mac}} {+} P_{\text{kem}}$ \\
LO\_Stream\_Secrecy
  & $\mathsf{secret}\ b_0$ \texttt{[cv\_bit]}
  & $2P_{\text{ctxt}} {+} 2P_{\text{cpa}}(t, N_{\text{enc}})$ \\
  & $\mathsf{inj\text{-}event} {\Rightarrow}
    \mathsf{inj\text{-}event}$
  & $P_{\text{ctxt}}$ \\
\bottomrule
\end{tabular}
\end{table}


\section{Wire sizes}\label{app:sizes}

\begin{table}[!htbp]
\centering
\caption{Key and ciphertext sizes (bytes).}
\label{tab:sizes}
\small
\begin{tabular}{@{} l r l @{}}
\toprule
\textbf{Object} & \textbf{Size} & \textbf{Components} \\
\midrule
Identity public key & 3200 & X-Wing (1216) + Ed25519 (32) + ML-DSA (1952) \\
Identity secret key & 2496 & X-Wing (2432) + Ed25519 (32) + ML-DSA seed (32) \\
Identity fingerprint & 32 & SHA3-256 of public key \\
X-Wing public key & 1216 & ML-KEM-768 (1184) + X25519 (32) \\
X-Wing ciphertext & 1120 & ML-KEM-768 (1088) + X25519 (32) \\
Hybrid signature & 3373 & Ed25519 (64) + ML-DSA-65 (3309) \\
\midrule
Ratchet header (no KEM step) & 1225 & $\pk_s$ + flag + counters \\
Ratchet header (with KEM step) & 2347 & + length prefix + $c_{\text{ratchet}}$ \\
Session init (no OPK) & 3543 & version + fps + $\pk_{\text{EK}}$ + 2 ciphertexts \\
Session init (with OPK) & 4669 & + 1 ciphertext \\
\midrule
Stream header & 26 & version (1) + flags (1) + base\_nonce (24) \\
Stream chunk overhead & 17 & tag\_byte (1) + Poly1305 tag (16) \\
\bottomrule
\end{tabular}
\end{table}


% ============================================================================
% REFERENCES (placeholder for BibTeX)
% ============================================================================
\begingroup
\raggedright
\begin{thebibliography}{99}

\bibitem{acd19} J.~Alwen, S.~Coretti, Y.~Dodis. ``The Double Ratchet:
Security Notions, Proofs, and Modularization for the Signal Protocol.''
EUROCRYPT~2019.

\bibitem{apple-pq3} Apple Security Research. ``iMessage with PQ3.''
\url{https://security.apple.com/blog/imessage-pq3/}, 2024.

\bibitem{bellare06} M.~Bellare. ``New Proofs for NMAC and HMAC: Security
without Collision-Resistance.'' CRYPTO~2006.


\bibitem{bfg20} J.~Brendel, M.~Fischlin, F.~G\"unther, C.~Janson,
D.~Stebila. ``Towards Post-Quantum Security for Signal's X3DH
Handshake.'' SAC~2020.

\bibitem{bjks24} K.~Bhargavan, C.~Jacomme, F.~Kiefer, R.~Schmidt.
``Formal Verification of the PQXDH Post-Quantum Key Agreement Protocol.''
USENIX Security~2024.

\bibitem{bj24} B.~Blanchet, C.~Jacomme. ``Post-Quantum Sound CryptoVerif
and Verification of Hybrid TLS and SSH Key-Exchanges.'' CSF~2024.

\bibitem{cgcd20} K.~Cohn-Gordon, C.~Cremers, B.~Dowling, L.~Garratt,
D.~Stebila. ``A Formal Security Analysis of the Signal Messaging
Protocol.'' J.~Cryptology, 2020.

\bibitem{djkps25} Y.~Dodis, D.~Jost, S.~Katsumata, T.~Prest,
R.~Schmidt. ``Triple Ratchet: A Bandwidth Efficient Hybrid-Secure Signal
Protocol.'' EUROCRYPT~2025. IACR ePrint 2025/078.

\bibitem{adjks25} B.~Auerbach, Y.~Dodis, D.~Jost, S.~Katsumata,
R.~Schmidt. ``How to Compare Bandwidth Constrained Two-Party Secure
Messaging Protocols.'' USENIX Security~2025.

\bibitem{fips203} NIST. ``Module-Lattice-Based Key-Encapsulation
Mechanism Standard.'' FIPS~203, 2024.

\bibitem{fips204} NIST. ``Module-Lattice-Based Digital Signature
Standard.'' FIPS~204, 2024.

\bibitem{hks22} K.~Hashimoto, S.~Katsumata, K.~Kwiatkowski, T.~Prest.
``An Efficient and Generic Construction for Signal's Handshake (X3DH):
Post-Quantum, State Leakage Secure, and Deniable.'' J.~Cryptology, 2022.

\bibitem{hrrv15} V.T.~Hoang, R.~Reyhanitabar, P.~Rogaway, D.~Viz\'ar.
``Online Authenticated-Encryption and its Nonce-Reuse
Misuse-Resistance.'' CRYPTO~2015.

\bibitem{krawczyk10} H.~Krawczyk. ``Cryptographic Extraction and Key
Derivation: The HKDF Scheme.'' CRYPTO~2010.

\bibitem{lsb25} F.~Linker, R.~Sasse, D.~Basin. ``A Formal Analysis of
Apple's iMessage PQ3 Protocol.'' USENIX Security~2025.

\bibitem{rfc5869} H.~Krawczyk, P.~Eronen. ``HMAC-based
Extract-and-Expand Key Derivation Function (HKDF).'' RFC~5869, 2010.


\bibitem{rfc8032} S.~Josefsson, I.~Liusvaara. ``Edwards-Curve Digital
Signature Algorithm (EdDSA).'' RFC~8032, 2017.

\bibitem{signal-doubleratchet} Signal Foundation. ``The Double Ratchet
Algorithm.'' \url{https://signal.org/docs/specifications/doubleratchet/}.

\bibitem{signal-pqxdh} E.~Kret. ``Quantum Resistance and the Signal
Protocol.'' Signal Blog, 2023.
\url{https://signal.org/blog/pqxdh/}.

\bibitem{signal-spqr} Signal Foundation. ``Signal Protocol and
Post-Quantum Ratchets.'' Signal Blog, 2025.
\url{https://signal.org/blog/spqr/}.

\bibitem{signal-x3dh} Signal Foundation. ``The X3DH Key Agreement
Protocol.'' \url{https://signal.org/docs/specifications/x3dh/}.

\bibitem{soliton-repo} K.~Tufekcic. ``libsoliton.''
\url{https://git.lo.sh/lo/libsoliton}.

\bibitem{soliton-spec} K.~Tufekcic. ``Soliton Cryptographic
Specification.''
\url{https://git.lo.sh/lo/libsoliton/wiki/Specification}.

\bibitem{soliton-analysis} K.~Tufekcic. ``Soliton Formal Analysis.''
\url{https://git.lo.sh/lo/libsoliton/wiki/Formal-Analysis}.

\bibitem{xwing} M.~Barbosa \etal ``X-Wing: The Hybrid KEM You've Been
Looking For.'' IACR Commun.\ Cryptol., 2024.

\bibitem{xwing-ietf} D.~Connolly \etal
``draft-connolly-cfrg-xwing-kem-10.'' IETF CFRG, 2026.

\bibitem{fiedler-janson24} R.~Fiedler, C.~Janson. ``A Deniability
Analysis of Signal's Initial Handshake PQXDH.'' PoPETs, 2024. IACR
ePrint 2024/741.


\bibitem{cmn25} C.~Cremers, N.~Medinger, A.~Naska. ``Impossibility
Results for Post-Compromise Security in Real-World Communication
Systems.'' IEEE S\&P, 2025. IACR ePrint 2024/1886.

\bibitem{starfighters25} D.~Connolly, A.~H\"ovelmanns, A.~H\"ulsing,
S.~Kousidis, J.~Meijers. ``Starfighters --- On the General
Applicability of X-Wing.'' IACR ePrint 2025/1397.

\bibitem{bp26} S.~Bao, Y.~Pan. ``Anonymity of X-Wing and its
Variants.'' IACR ePrint 2026/396.

\bibitem{kls26} M.~Kang, J.~Lee, K.~Son. ``On the Necessity of Public
Contexts in Hybrid KEMs: A Case Study of X-Wing.'' IACR ePrint
2026/140.

\bibitem{bcrs24} L.~B\'eguinet, C.~Chevalier, T.~Ricosset, E.~Senet.
``Formal Verification of a Post-quantum Signal Protocol with Tamarin.''
VECoS~2023, LNCS~14368, 2024.

\bibitem{hs20} V.T.~Hoang, Y.~Shen. ``Security of Streaming Encryption
in Google's Tink Library.'' CCS, 2020. IACR ePrint 2020/1019.

\bibitem{floe25} T.~Fabrega, J.~Len, T.~Ristenpart, A.~Rubin.
``Random-Access AEAD for Fast Lightweight Online Encryption.'' IACR
ePrint 2025/2275.

\bibitem{rfc9420} R.~Barnes, B.~Beurdouche, R.~Robert, J.~Millican,
E.~Omara, K.~Cohn-Gordon. ``The Messaging Layer Security (MLS)
Protocol.'' RFC~9420, 2023.

\end{thebibliography}
\endgroup

\end{document}