diff --git a/Abstract.md b/Abstract.md index 5c7d07c11b..2af5f15b98 100644 --- a/Abstract.md +++ b/Abstract.md @@ -73,16 +73,16 @@ HybridSig combines Ed25519 (classical) and ML-DSA-65 (post-quantum). Key pairs satisfy pk = (pk_E, pk_P), sk = (sk_E, sk_P). **Sign(sk, m)** → σ = (σ_E ‖ σ_P): both components computed independently and -concatenated. ML-DSA-65 uses hedged signing via `sign_internal` (FIPS 204 §5.2 / -Algorithm 2); fresh randomness is mixed per signing operation for +concatenated. ML-DSA-65 uses hedged signing via `sign_internal` (FIPS 204 §6.2 / +Algorithm 7); fresh randomness is mixed per signing operation for fault-injection resistance. **FIPS 204 compatibility note**: The implementation calls `sign_internal` directly — the raw internal signing function with no context string or domain prefix. This is structurally incompatible with FIPS 204 -§6.2 (`ML-DSA.Sign`, which prepends a context-dependent domain separator before -calling `sign_internal`). A FIPS 204 §6.2 verifier expecting the domain-prefixed -message format will reject Soliton ML-DSA-65 signatures. A formal model or test -vector suite must use the `sign_internal` / `verify_internal` interface, not the -§6.2 external interface. For adversary models that include fault injection, +§5.2 (`ML-DSA.Sign` / Algorithm 2, which prepends a context-dependent domain +separator before calling `sign_internal`). A FIPS 204 §5.2 verifier expecting +the domain-prefixed message format will reject Soliton ML-DSA-65 signatures. A +formal model or test vector suite must use the `sign_internal` / +`verify_internal` interface, not the §5.2 external interface. For adversary models that include fault injection, hedged signing provides resistance to differential fault analysis that deterministic signing does not. **RNG implication**: Every HybridSig.Sign invocation consumes randomness (from ML-DSA-65's hedged component). In the §8.2 diff --git a/Cargo.toml b/Cargo.toml index 42e382b1b9..7db1de30c1 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -19,7 +19,7 @@ edition = "2024" rust-version = "1.85" license = "AGPL-3.0-only" repository = "https://git.lo.sh/lo/libsoliton" -homepage = "https://lo.sh" +homepage = "https://git.lo.sh/lo/libsoliton/wiki" authors = ["LO Contributors"] description = "Cryptographic library for the LO protocol" categories = ["cryptography"] diff --git a/README.md b/README.md index 5f23c654d6..c5462cc6ec 100644 --- a/README.md +++ b/README.md @@ -8,6 +8,7 @@ Pure-Rust post-quantum cryptographic library. Provides composite identity keys ( | Document | Description | |----------|-------------| +| [paper.tex](paper.tex) | Protocol paper — design, security analysis, formal verification, implementation | | [Abstract.md](Abstract.md) | Security analysis specification — adversary model, theorems, and verification targets for formal modeling | | [Specification.md](Specification.md) | Full cryptographic specification (v1) | | [CHEATSHEET.md](CHEATSHEET.md) | API quick reference with types, sizes, and signatures | diff --git a/fuzz_overnight.sh b/fuzz_overnight.sh index 643ed5f4cf..63033f4b3a 100755 --- a/fuzz_overnight.sh +++ b/fuzz_overnight.sh @@ -16,6 +16,7 @@ fi HOURS="${1:-8}" WORKERS="${2:-1}" +# Change to 3600 for overnight runs, 1 is used for quick local runs SECONDS_TOTAL=$((HOURS * 1)) CORE_DIR="soliton" diff --git a/soliton.tex b/soliton.tex new file mode 100644 index 0000000000..30affae4b5 --- /dev/null +++ b/soliton.tex @@ -0,0 +1,2223 @@ +\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} \ No newline at end of file diff --git a/soliton/fuzz/Cargo.lock b/soliton/fuzz/Cargo.lock index 632618d2df..631446269f 100644 --- a/soliton/fuzz/Cargo.lock +++ b/soliton/fuzz/Cargo.lock @@ -435,7 +435,7 @@ dependencies = [ [[package]] name = "libsoliton" -version = "0.1.0" +version = "0.1.1" dependencies = [ "argon2", "chacha20poly1305", diff --git a/soliton/fuzz/corpus/fuzz_auth_respond/valid_ct b/soliton/fuzz/corpus/fuzz_auth_respond/valid_ct index 7455631829..31dd7283ef 100644 Binary files a/soliton/fuzz/corpus/fuzz_auth_respond/valid_ct and b/soliton/fuzz/corpus/fuzz_auth_respond/valid_ct differ diff --git a/soliton/fuzz/corpus/fuzz_decrypt_first_message/valid_first_msg b/soliton/fuzz/corpus/fuzz_decrypt_first_message/valid_first_msg index e8335b1202..6288a47f47 100644 --- a/soliton/fuzz/corpus/fuzz_decrypt_first_message/valid_first_msg +++ b/soliton/fuzz/corpus/fuzz_decrypt_first_message/valid_first_msg @@ -1 +1 @@ -d怹@º@eTRV |ZAI/jA\;  \ No newline at end of file +xe)S^8v/و7+⨋NEfOJx}6G9G \ No newline at end of file diff --git a/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/0792446e9e4e302ef86828be9e266fc1b4de4407 b/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/0792446e9e4e302ef86828be9e266fc1b4de4407 new file mode 100644 index 0000000000..e26cd0edd0 --- /dev/null +++ b/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/0792446e9e4e302ef86828be9e266fc1b4de4407 @@ -0,0 +1 @@ +A  \ No newline at end of file diff --git a/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/164fd078f9a0ba81f8d916617ade549e2389f89d b/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/164fd078f9a0ba81f8d916617ade549e2389f89d new file mode 100644 index 0000000000..5a5875d376 Binary files /dev/null and b/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/164fd078f9a0ba81f8d916617ade549e2389f89d differ diff --git a/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/2284aab09f260f3ea2a36303e8e4b8c022faa1ff b/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/2284aab09f260f3ea2a36303e8e4b8c022faa1ff new file mode 100644 index 0000000000..8a807b8027 Binary files /dev/null and b/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/2284aab09f260f3ea2a36303e8e4b8c022faa1ff differ diff --git a/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/22ef1d4d7b042ff205815af958bde3c619157361 b/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/22ef1d4d7b042ff205815af958bde3c619157361 new file mode 100644 index 0000000000..f2d41988b6 Binary files /dev/null and b/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/22ef1d4d7b042ff205815af958bde3c619157361 differ diff --git a/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/3d1234355041aae78f70de42de8515a921c9073d b/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/3d1234355041aae78f70de42de8515a921c9073d new file mode 100644 index 0000000000..5349698479 Binary files /dev/null and b/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/3d1234355041aae78f70de42de8515a921c9073d differ diff --git a/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/8ce24fc0ea8e685eb23bf6346713ad9fef920425 b/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/8ce24fc0ea8e685eb23bf6346713ad9fef920425 new file mode 100644 index 0000000000..6cc8370785 --- /dev/null +++ b/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/8ce24fc0ea8e685eb23bf6346713ad9fef920425 @@ -0,0 +1 @@ + \ No newline at end of file diff --git a/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/91ac28edf4ce92b1fe9d9f83cd5447d067a4b366 b/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/91ac28edf4ce92b1fe9d9f83cd5447d067a4b366 new file mode 100644 index 0000000000..f7ba3570ce Binary files /dev/null and b/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/91ac28edf4ce92b1fe9d9f83cd5447d067a4b366 differ diff --git a/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/b3b28f02b153220e7d1bf1b19dbb32363b926181 b/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/b3b28f02b153220e7d1bf1b19dbb32363b926181 new file mode 100644 index 0000000000..c1bf8d7a25 Binary files /dev/null and b/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/b3b28f02b153220e7d1bf1b19dbb32363b926181 differ diff --git a/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/d081c37090c6c163e1ed6b7f27c34d61f5437606 b/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/d081c37090c6c163e1ed6b7f27c34d61f5437606 new file mode 100644 index 0000000000..60634713ae --- /dev/null +++ b/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/d081c37090c6c163e1ed6b7f27c34d61f5437606 @@ -0,0 +1 @@ +A \ No newline at end of file diff --git a/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/df4e1459fc34e72f44fd348ae97abd055d253d52 b/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/df4e1459fc34e72f44fd348ae97abd055d253d52 new file mode 100644 index 0000000000..b24d587d95 Binary files /dev/null and b/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/df4e1459fc34e72f44fd348ae97abd055d253d52 differ diff --git a/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/f421c2fbfd6ff080108402148f2cfa0a41715290 b/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/f421c2fbfd6ff080108402148f2cfa0a41715290 new file mode 100644 index 0000000000..9215116d37 Binary files /dev/null and b/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/f421c2fbfd6ff080108402148f2cfa0a41715290 differ diff --git a/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/truncated b/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/truncated index a96d473611..8949654869 100644 --- a/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/truncated +++ b/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/truncated @@ -1 +1 @@ -́@qvU|J

T \ No newline at end of file diff --git a/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/valid_compressed b/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/valid_compressed index 78648b8888..3873ed9a0a 100644 --- a/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/valid_compressed +++ b/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/valid_compressed @@ -1 +1 @@ -́@qvU|J2疚 \ No newline at end of file +n[t'޷>TR297l8HI)UZGnB*h鬠Kb( t=P_$4:gu \ No newline at end of file diff --git a/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/valid_uncompressed b/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/valid_uncompressed index 5b964c84c6..7fb665ed43 100644 Binary files a/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/valid_uncompressed and b/soliton/fuzz/corpus/fuzz_dm_queue_decrypt_blob/valid_uncompressed differ diff --git a/soliton/fuzz/corpus/fuzz_ed25519_verify/bad_sig_bit b/soliton/fuzz/corpus/fuzz_ed25519_verify/bad_sig_bit index 0f22f8cb6a..3ab93863a9 100644 --- a/soliton/fuzz/corpus/fuzz_ed25519_verify/bad_sig_bit +++ b/soliton/fuzz/corpus/fuzz_ed25519_verify/bad_sig_bit @@ -1,2 +1,2 @@ -nDky = K/8l8NNwoa"e!?_ -^&M]U 7c~چVK%D jq|D \ No newline at end of file +aj</q:D6. JD4K~A*@wCe \ No newline at end of file diff --git a/soliton_capi/fuzz/corpus/fuzz_capi_storage_decrypt/dde7aa5a3d9db2fc6e2bcbe681f51a78d17fcd92 b/soliton_capi/fuzz/corpus/fuzz_capi_storage_decrypt/dde7aa5a3d9db2fc6e2bcbe681f51a78d17fcd92 new file mode 100644 index 0000000000..377e8ab0a2 Binary files /dev/null and b/soliton_capi/fuzz/corpus/fuzz_capi_storage_decrypt/dde7aa5a3d9db2fc6e2bcbe681f51a78d17fcd92 differ diff --git a/soliton_capi/fuzz/corpus/fuzz_capi_storage_decrypt/unknown_version b/soliton_capi/fuzz/corpus/fuzz_capi_storage_decrypt/unknown_version index d94af16c24..f933690bd6 100644 Binary files a/soliton_capi/fuzz/corpus/fuzz_capi_storage_decrypt/unknown_version and b/soliton_capi/fuzz/corpus/fuzz_capi_storage_decrypt/unknown_version differ diff --git a/soliton_capi/fuzz/corpus/fuzz_capi_storage_decrypt/valid_compressed b/soliton_capi/fuzz/corpus/fuzz_capi_storage_decrypt/valid_compressed index cf0cef3f78..f7d4fa492d 100644 Binary files a/soliton_capi/fuzz/corpus/fuzz_capi_storage_decrypt/valid_compressed and b/soliton_capi/fuzz/corpus/fuzz_capi_storage_decrypt/valid_compressed differ diff --git a/soliton_capi/fuzz/corpus/fuzz_capi_storage_decrypt/valid_uncompressed b/soliton_capi/fuzz/corpus/fuzz_capi_storage_decrypt/valid_uncompressed index a5bd365a56..5681042cf2 100644 Binary files a/soliton_capi/fuzz/corpus/fuzz_capi_storage_decrypt/valid_uncompressed and b/soliton_capi/fuzz/corpus/fuzz_capi_storage_decrypt/valid_uncompressed differ diff --git a/soliton_capi/fuzz/corpus/fuzz_capi_stream_decrypt/single_uncompressed b/soliton_capi/fuzz/corpus/fuzz_capi_stream_decrypt/single_uncompressed index 16c5664e91..2e565c6a20 100644 Binary files a/soliton_capi/fuzz/corpus/fuzz_capi_stream_decrypt/single_uncompressed and b/soliton_capi/fuzz/corpus/fuzz_capi_stream_decrypt/single_uncompressed differ diff --git a/soliton_capi/fuzz/corpus/fuzz_capi_stream_decrypt_at/index_0_final b/soliton_capi/fuzz/corpus/fuzz_capi_stream_decrypt_at/index_0_final index cb94fe7c45..8faef8dc48 100644 Binary files a/soliton_capi/fuzz/corpus/fuzz_capi_stream_decrypt_at/index_0_final and b/soliton_capi/fuzz/corpus/fuzz_capi_stream_decrypt_at/index_0_final differ diff --git a/soliton_capi/fuzz/corpus/fuzz_capi_stream_decrypt_at/index_max_minus_1 b/soliton_capi/fuzz/corpus/fuzz_capi_stream_decrypt_at/index_max_minus_1 index 546af07bac..490e415989 100644 Binary files a/soliton_capi/fuzz/corpus/fuzz_capi_stream_decrypt_at/index_max_minus_1 and b/soliton_capi/fuzz/corpus/fuzz_capi_stream_decrypt_at/index_max_minus_1 differ