Add Paper

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 |