diff --git a/Paper.md b/Paper.md new file mode 100644 index 0000000..615da46 --- /dev/null +++ b/Paper.md @@ -0,0 +1,34 @@ +# Paper + +**Soliton: A Formally Verified Post-Quantum Messaging Protocol with Hybrid Authentication** + +Kamal Tufekcic. 2026. + +- [LaTeX source](https://git.lo.sh/lo/libsoliton/src/branch/master/paper.tex) + +## 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](Specification) | Full cryptographic specification (5000+ lines) | +| [Formal Analysis](Formal-Analysis) | Adversary model, 13 theorems, verification targets | +| [Formal Verification](Formal-Verification) | Tamarin + CryptoVerif model results | +| [Audit & Testing](Audit-and-Testing) | Test suite, fuzzing, benchmarks |