Paper

Soliton: A Formally Verified Post-Quantum Messaging Protocol with Hybrid Authentication

Kamal Tufekcic. 2026.

• LaTeX source

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.

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, with 574.6 billion fuzz executions across 36 targets yielding zero crashes.

Companion Documents

Document	Description
Specification	Full cryptographic specification (5000+ lines)
Formal Analysis	Adversary model, 13 theorems, verification targets
Formal Verification	Tamarin + CryptoVerif model results
Audit & Testing	Test suite, fuzzing, benchmarks