diff --git a/API-Reference.md b/API-Reference.md index 9eaeffb59a..80d12e2a3c 100644 --- a/API-Reference.md +++ b/API-Reference.md @@ -99,7 +99,7 @@ Quick reference for the soliton v1 API. For the full cryptographic specification libsoliton = { path = "../soliton" } # Published form (once on crates.io — use one or the other, not both): -# libsoliton = "0.1.1" +# libsoliton = "0.1.0" ``` **Minimum toolchain: Rust 1.93 (edition 2024).** The `unsafe extern "C" {}` block syntax added in edition 2024 is required; older toolchains produce cryptic parse errors. Run `rustup update stable` to get a recent toolchain. @@ -2022,7 +2022,7 @@ pub fn aead_decrypt(key: &[u8; 32], nonce: &[u8; 24], ### C API ```c -// Returns the library version string — the Cargo crate semver (e.g., "0.1.1"), +// Returns the library version string — the Cargo crate semver (e.g., "0.1.0"), // not the spec revision. Static lifetime, null-terminated. Caller must NOT free. // Rust equivalent: soliton::VERSION (&str, same value). const char *soliton_version(void); diff --git a/Audit-and-Testing.md b/Audit-and-Testing.md index 5f6a7fbd9e..ec0725b1a3 100644 --- a/Audit-and-Testing.md +++ b/Audit-and-Testing.md @@ -2,6 +2,14 @@ Trust signals for evaluating libsoliton's reliability and security posture. +## Formal Verification + +8 Tamarin models (55 lemmas) and 5 CryptoVerif models (7 queries) provide +machine-checked proofs of all 13 security theorems from the +[Formal Analysis](Formal-Analysis) specification. See +**[Formal Verification](Formal-Verification)** for full results, bounds, +and reproduction instructions. + ## Test Suite | Location | Count | Description | diff --git a/Formal-Analysis.md b/Formal-Analysis.md index 60c08e890d..20466be80b 100644 --- a/Formal-Analysis.md +++ b/Formal-Analysis.md @@ -136,16 +136,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](#52-kem-ratchet-step-send) (`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](#52-kem-ratchet-step-send) 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](#82-corruption-queries) diff --git a/Formal-Verification.md b/Formal-Verification.md new file mode 100644 index 0000000000..f5aee8f4e2 --- /dev/null +++ b/Formal-Verification.md @@ -0,0 +1,311 @@ +# Formal Verification + +Machine-checked proofs of all 13 security theorems from the +[Formal Analysis](Formal-Analysis) specification, using two independent +tools: Tamarin Prover (symbolic) and CryptoVerif (computational). + +These models were authored by the protocol designers and have not undergone +independent peer review. They are published for transparency and to facilitate +third-party verification. All results are machine-checkable and reproducible. + +**Totals**: 8 Tamarin models (55 lemmas) + 5 CryptoVerif models (7 queries) += 62 machine-checked results, 0 failures. + +Run `verify.sh` from the repository root to reproduce all results. See +[source](https://git.lo.sh/lo/libsoliton/src/branch/master/verify.sh). + +--- + +# Tamarin Models + +Symbolic formal verification of the Soliton cryptographic protocol using +[Tamarin Prover](https://tamarin-prover.com/). 8 models, 55 lemmas. + +These models were authored by the protocol designers and have not undergone +independent peer review. They are published for transparency and to facilitate +third-party verification. All results are machine-checkable and reproducible. + +## Requirements + +- tamarin-prover 1.12.0+ +- maude 3.5.1+ + +## Usage + +```bash +# All models +../verify.sh tamarin + +# Single model +tamarin-prover LO_Auth.spthy --prove +``` + +## Resource Usage + +All 8 models complete in under 90 seconds total with under 2 GB peak RAM. +No special hardware or overnight runs required — a laptop is sufficient. + +This is achieved through bounded unrolling (3–4 steps for ratchet and chain +models) and unique fact names per state (eliminating branching during source +analysis). + +## Results + +Verified with Tamarin 1.12.0, Maude 3.5.1. + +### LO_Auth.spthy — Theorem 6 (Key Possession) + +| Lemma | Result | Steps | +|-------|--------|-------| +| 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 | +| Theorem6_Key_Possession | verified | 11 | +| Theorem6_No_Oracle | verified | 11 | + +### LO_KEX.spthy — Theorems 1, 2a, 2b (Session Key Secrecy, Authentication) + +OPK-present case only. See header comment for OPK-absent scope note. + +| Lemma | Result | Steps | +|-------|--------|-------| +| KEX_Exists | verified | 27 | +| Theorem1_Session_Key_Secrecy_A | verified | 70 | +| Theorem1_Session_Key_Secrecy_B | verified | 136 | +| Theorem1_EK_Secrecy_A | verified | 70 | +| Theorem1_EK_Secrecy_B | verified | 136 | +| Theorem2a_Recipient_Binding | verified | 2 | +| Theorem2b_Initiator_Authentication | verified | 10 | +| OPK_Single_Use | verified | 24 | +| Key_Uniqueness | verified | 2 | + +### LO_Ratchet.spthy — Theorems 4, 5 (Forward Secrecy, PCS — structural) + +Abstract model using Fr() epoch keys. Proves FS and PCS are structural +properties of the state machine, independent of KDF/KEM security. + +| Lemma | Result | Steps | Notes | +|-------|--------|-------|-------| +| send_sanity | verified | 7 | | +| send_fs | verified | 2818 | Theorem 4a | +| send_corrupt_terminates | verified | 193 | | +| send_pcs | verified | 2 | Abstract model only | +| recv_sanity | verified | 6 | | +| recv_fs_1step | **falsified** | 11 | Expected — prev_ek_r retains old key | +| recv_fs_2step | verified | 9132 | Theorem 4b | +| recv_corrupt_terminates | verified | 273 | | +| recv_pcs | verified | 107 | Abstract model only (see comment) | + +### LO_Ratchet_PCS.spthy — Theorem 5 (PCS — KEM-level) + +KEM-level model proving the 1-step non-recovery / 1-direction-change recovery +that the abstract Fr() model cannot distinguish. + +| Lemma | Result | Steps | Notes | +|-------|--------|-------|-------| +| pcs_sanity | verified | 3 | | +| pcs_no_recovery_after_recv | **falsified** | 9 | Expected — adversary holds sk_own | +| pcs_recovery_after_send | verified | 7 | | +| pcs_recovery_sustained | verified | 15 | | +| pcs_f4_violated | verified | 7 | F4 defeats next recv, not this send | + +### LO_Call.spthy — Theorems 8–11 (Call Key Security) + +| Lemma | Result | Steps | +|-------|--------|-------| +| Call_Exists | verified | 6 | +| Call_Key_Agreement | verified | 56 | +| Theorem8_Call_Key_Secrecy | verified | 24 | +| Theorem9_Intra_Call_FS | verified | 193 | +| Theorem10_Call_Ratchet_Ind | verified | 3 | +| Theorem11_Concurrent_Ind | verified | 52 | + +### LO_AntiReflection.spthy — Theorem 12 (Anti-Reflection) + +| Lemma | Result | Steps | +|-------|--------|-------| +| Reflection_Sanity | verified | 8 | +| Theorem12_Anti_Reflection | verified | 5 | + +### LO_Stream.spthy — Theorem 13, Properties 2–5 (Streaming AEAD) + +| Lemma | Result | Steps | +|-------|--------|-------| +| Stream_Sanity | verified | 11 | +| Stream_Sanity_Finalize | verified | 7 | +| Theorem13_P2_Integrity | verified | 28 | +| Theorem13_P3_Ordering | verified | 18 | +| Theorem13_P4_No_False_Final | verified | 17 | +| Theorem13_P5_Cross_Stream | verified | 55 | +| Theorem13_Key_Secrecy | verified | 3 | + +### LO_NegativeTests.spthy — Expected Falsifications + +Each lemma confirms a known attack path works in the model. All should be +falsified (or verified for exists-trace). If any result flips, the model has +a bug. + +| Lemma | Result | Steps | Attack path | +|-------|--------|-------|-------------| +| neg_auth_ik_corrupt | falsified | 8 | IK corruption forges auth | +| neg_auth_rng_corrupt | falsified | 10 | RNG corruption forges auth | +| neg_ratchet_no_fs_0step | falsified | 8 | Corrupt immediately reveals ek | +| neg_ratchet_recv_1step | falsified | 10 | 1-step recv, prev retains ek | +| neg_call_rk_plus_rng | falsified | 9 | rk + RNG derives call key | +| neg_stream_key_corrupt | falsified | 5 | Key corruption enables forgery | +| neg_reflect_self_session | falsified | 7 | Self-session enables reflection | +| neg_kex_no_opk | falsified | 11 | IK+SPK alone breaks OPK-absent | +| neg_ratchet_duplicate | falsified | 7 | No recv_seen → duplicate accepted | +| neg_call_self_session | verified | 3 | Self-call reachable without guard | + +## Scope and Limitations + +- **OPK-absent KEX**: LO_KEX.spthy models the 3-key (OPK-present) case only. + The 2-key OPK-absent case has a weaker secrecy threshold (IK+SPK), validated + by neg_kex_no_opk in the negative tests. +- **X-Wing as black box**: All models treat X-Wing as a single IND-CCA2 KEM + without opening the combiner (draft-09 hybrid argument). +- **Abstract ratchet**: LO_Ratchet.spthy uses Fr() epoch keys (not KDF-derived). + KEM-level properties are in LO_Ratchet_PCS.spthy. +- **No Theorem 7**: Domain separation is vacuously true in Tamarin (string + constants are structurally distinct). +- **No Theorem 3/13-P1**: Message confidentiality (IND-CPA) is computational, + covered by the CryptoVerif models. +- **Bounded chains**: Ratchet and call chain steps are bounded (3–4 steps) + to prevent Tamarin non-termination. + +## Theorem Coverage + +| Theorem | Model | Type | +|---------|-------|------| +| 1 (KEX Key Secrecy) | LO_KEX | Symbolic secrecy | +| 2a (Recipient Auth) | LO_KEX | Structural binding | +| 2b (Initiator Auth) | LO_KEX | Correspondence | +| 4 (Forward Secrecy) | LO_Ratchet | Structural FS | +| 5 (PCS) | LO_Ratchet + LO_Ratchet_PCS | Structural + KEM-level | +| 6 (Auth Key Possession) | LO_Auth | Correspondence | +| 8 (Call Key Secrecy) | LO_Call | Symbolic secrecy | +| 9 (Intra-Call FS) | LO_Call | Chain one-wayness | +| 10 (Call/Ratchet Ind.) | LO_Call | Independence | +| 11 (Concurrent Calls) | LO_Call | Independence | +| 12 (Anti-Reflection) | LO_AntiReflection | AAD direction binding | +| 13 P2–P5 | LO_Stream | Integrity, ordering, truncation, isolation | + + +--- + +# CryptoVerif Models + +Computational formal verification of the Soliton cryptographic protocol using +[CryptoVerif](https://bblanche.gitlabpages.inria.fr/CryptoVerif/). + +These models were authored by the protocol designers and have not undergone +independent peer review. They are published for transparency and to facilitate +third-party verification. All results are machine-checkable and reproducible. + +## Requirements + +- CryptoVerif 2.12+ +- The `pq.cvl` library (ships with CryptoVerif) + +## Usage + +```bash +# All models +CV_LIB=/path/to/pq ../verify.sh cryptoverif + +# Single model +cryptoverif -lib /path/to/pq LO_Auth.cv +``` + +## Resource Usage + +All 5 models complete in under 5 seconds total with negligible RAM usage. +No special hardware required. + +## Results + +Verified with CryptoVerif 2.12. + +### LO_Auth.cv — Theorem 6 (Key Possession) + +| Query | Result | Bound | +|-------|--------|-------| +| event(ServerAccepts) ==> event(ClientResponds) | proved | Ns × P_mac + P_kem | +| inj-event(ServerAccepts) ==> inj-event(ClientResponds) | proved | Ns × P_mac + P_kem | + +Primitives: IND-CCA2 KEM (X-Wing), SUF-CMA deterministic MAC (HMAC-SHA3-256). + +### LO_KEX.cv — Theorem 2b (Initiator Authentication) + +| Query | Result | Bound | +|-------|--------|-------| +| event(Bob_Accept) ==> event(Alice_Init) | proved | P_sig_A | + +Primitives: EUF-CMA signature (HybridSig). Proof uses only Alice's signature +unforgeability. Non-injective (replay is application-layer per §7.5 A4). + +### LO_KEX_Secrecy.cv — Theorem 1 (Session Key Secrecy) + +| Query | Result | Bound | +|-------|--------|-------| +| secret rk_A [cv_onesession] | proved | 2·P_prf + 2·P_kem_ik + 2·P_kem_spk + 2·P_kem_opk + collision terms | + +Primitives: 3× IND-CCA2 KEM, PRF (HKDF). Signatures omitted (Theorem 1 is +secrecy, not authentication). No corruption oracles (Tamarin covers corruption +cases). See header comment for full simplifications list. + +### LO_Ratchet_MsgSecrecy.cv — Theorem 3 (Message Key Secrecy) + +| Query | Result | Bound | +|-------|--------|-------| +| secret test_mk [cv_onesession] | proved | 2 × P_prf | + +Precondition: epoch key ek is fresh (from Theorem 1 + KDF_Root output +independence). Combined with AEAD IND-CPA+INT-CTXT under random keys +(standard [BN00] composition), gives full message secrecy. + +### LO_Stream_Secrecy.cv — Theorem 13, Properties 1+2 (Streaming AEAD) + +| Query | Result | Bound | +|-------|--------|-------| +| secret b0 [cv_bit] (IND-CPA) | proved | 2·P_ctxt + 2·P_cpa(time, N_enc) | +| inj-event(Received) ==> inj-event(Sent) (INT-CTXT) | proved | P_ctxt | + +Adapted from CryptoVerif's TLS 1.3 Record Protocol example. Nonce uniqueness +enforced via table-based game hypothesis (§9.11(f)). base_nonce is public. + +Key properties of the bounds: +- **INT-CTXT has no Q-factor** — direct forgery reduction +- **IND-CPA scales as N_enc × P_cpa** — Q-step hybrid argument + +## Scope and Limitations + +- **X-Wing as black box**: All models treat X-Wing as a monolithic IND-CCA2 + KEM. The spec (§2.1) recommends opening the combiner for CryptoVerif. The + black-box assumption is stronger; bounds are in terms of P_kem rather than + component advantages (P_mlkem + P_x25519 + P_sha3_ro). +- **No corruption oracles**: The CryptoVerif KEX models prove security for + the no-corruption case. Corruption-parameterized secrecy (partial key + compromise, RNG corruption) is verified by the Tamarin models. +- **Simplified KDF info**: LO_KEX_Secrecy.cv binds fewer values in the PRF + input than the full HKDF info field. The PRF proof holds regardless of + info content; session-binding properties are verified by Tamarin. +- **Single-epoch message secrecy**: LO_Ratchet_MsgSecrecy.cv assumes a fresh + epoch key. The composition chain (Theorem 1 → KDF_Root → fresh ek → PRF → + fresh mk → AEAD) is sound but not mechanically verified end-to-end. +- **No Theorem 2c/d**: Key confirmation requires a combined KEX+Ratchet model. + +## Theorem Coverage + +| Theorem | Model | What's proved | +|---------|-------|---------------| +| 1 (KEX Key Secrecy) | LO_KEX_Secrecy | rk indistinguishable from random | +| 2b (Initiator Auth) | LO_KEX | σ_SI authentication via EUF-CMA | +| 3 (Message Secrecy) | LO_Ratchet_MsgSecrecy | mk indistinguishable from random | +| 6 (Auth Key Possession) | LO_Auth | Correspondence + injective | +| 13 P1 (IND-CPA) | LO_Stream_Secrecy | Bit secrecy of challenge bit | +| 13 P2 (INT-CTXT) | LO_Stream_Secrecy | Injective correspondence | + diff --git a/Paper.md b/Paper.md new file mode 100644 index 0000000000..625fbc169f --- /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 | diff --git a/Specification.md b/Specification.md index 8cb0caf5fb..47e59ea851 100644 --- a/Specification.md +++ b/Specification.md @@ -2971,7 +2971,7 @@ All CAPI functions with output buffer parameters zero the output upfront (after - `soliton_stream_encrypt_init(key, key_len, caller_aad, aad_len, compress, out)` — init encryptor (generates random base nonce). `key_len` MUST be exactly 32; any other value returns `InvalidLength`. Unlike `header_len` (lenient — extra bytes accepted), `key_len` is strict — the key is always exactly 32 bytes for XChaCha20-Poly1305. - `soliton_stream_encrypt_header(enc, out, out_len)` — copy 26-byte header into caller-allocated buffer; `out_len` MUST be ≥ 26 (lenient: extra buffer space is accepted) - `soliton_stream_encrypt_chunk(enc, plaintext, ..., is_last, out)` — encrypt one chunk; `out_len` MUST be ≥ `STREAM_ENCRYPT_MAX` (1,048,849 bytes) — returns `InvalidLength` for smaller buffers (parallel to the `out_len < STREAM_CHUNK_SIZE → InvalidLength` rule for decrypt chunk) -- `soliton_stream_encrypt_chunk_at(enc: *const, index, plaintext, ..., is_last, out)` — encrypt at explicit index (stateless, random-access); uses `*const SolitonStreamEncryptor` (not `*mut`) to reflect the `&self` Rust contract — see [§15.11](#1511-random-access) for the `*const` caveat. Same `out_len` ≥ `STREAM_ENCRYPT_MAX` requirement as the sequential variant. `index` MUST be unique per call — calling with the same `index` and different plaintexts produces nonce reuse ([§15.12](#1512-stream-level-security-analysis)). Does not advance `next_index`. Not interchangeable with the sequential variant; see [§15.11](#1511-random-access) for mixed-mode use. **Absent from `soliton.h`**: this function is implemented and exported (`#[unsafe(no_mangle)]`) but has no declaration in the C header — its decrypt counterpart `soliton_stream_decrypt_chunk_at` is declared in the header. Binding authors (C, C++, Go cgo, C#, Dart) must supply a manual `extern` declaration matching the signature above until the header is updated. +- `soliton_stream_encrypt_chunk_at(enc: *const, index, plaintext, ..., is_last, out)` — encrypt at explicit index (stateless, random-access); uses `*const SolitonStreamEncryptor` (not `*mut`) to reflect the `&self` Rust contract — see [§15.11](#1511-random-access) for the `*const` caveat. Same `out_len` ≥ `STREAM_ENCRYPT_MAX` requirement as the sequential variant. `index` MUST be unique per call — calling with the same `index` and different plaintexts produces nonce reuse ([§15.12](#1512-stream-level-security-analysis)). Does not advance `next_index`. Not interchangeable with the sequential variant; see [§15.11](#1511-random-access) for mixed-mode use. Declared in `soliton.h` (lines 1926–1962) with full documentation. - `soliton_stream_encrypt_is_finalized(enc, out: *mut bool)` — write finalized state to `out` - `soliton_stream_encrypt_free(enc)` — free encryptor (zeroizes key). Returns `int32_t`: 0 on success, `NullPointer` (-13) if outer pointer null, 0 (safe no-op) if inner pointer null (null inner pointer means the handle was already freed or never initialized — matches the double-free behavior of `soliton_ratchet_free` / `soliton_keyring_free`; does NOT return `NullPointer` for inner-null), `ConcurrentAccess` (-18) if in use, `InvalidData` (-17) if type discriminant wrong @@ -2985,13 +2985,7 @@ All CAPI functions with output buffer parameters zero the output upfront (after - `soliton_stream_decrypt_expected_index(dec, out: *mut u64)` — write next expected sequential index to `out` - `soliton_stream_decrypt_free(dec)` — free decryptor (zeroizes key). Returns `int32_t`: 0 on success, `NullPointer` (-13) if outer pointer null, 0 (safe no-op) if inner pointer null (null inner pointer means already-freed or never-initialized — does NOT return `NullPointer` for inner-null, consistent with `soliton_ratchet_free` / `soliton_keyring_free`), `ConcurrentAccess` (-18) if in use, `InvalidData` (-17) if type discriminant wrong -**`SOLITON_STREAM_ENCRYPT_MAX` and `SOLITON_STREAM_CHUNK_SIZE` are NOT defined as `#define` constants in `soliton.h`**: The header references these names in documentation comments but does not provide `#define` or `constexpr` entries. Binding authors who write `out_len = SOLITON_STREAM_ENCRYPT_MAX` get a compile error. The values must be embedded as integer literals in bindings: `STREAM_ENCRYPT_MAX = 1,048,849` (encrypt output buffer, see Appendix A) and `STREAM_CHUNK_SIZE = 1,048,576` (decrypt output buffer, see Appendix A). Language-idiomatic constant definitions are recommended: -```c -// C/C++ — add to binding wrapper or generated header -#define SOLITON_STREAM_ENCRYPT_MAX 1048849UL -#define SOLITON_STREAM_CHUNK_SIZE 1048576UL -``` -These values are stable and will not change without a major version bump. +`SOLITON_STREAM_ENCRYPT_MAX` (1,048,849) and `SOLITON_STREAM_CHUNK_SIZE` (1,048,576) are defined as `#define` constants in `soliton.h` (lines 53–54). Binding authors can use these names directly. These values are stable and will not change without a major version bump. **Streaming decrypt output buffer minimum — `STREAM_CHUNK_SIZE` (1,048,576 bytes)**: Both `soliton_stream_decrypt_chunk` and `soliton_stream_decrypt_chunk_at` require the output buffer to be at least `STREAM_CHUNK_SIZE` bytes regardless of the expected plaintext size. This is because the buffer size cannot be known before decryption completes (for compressed streams, the decompressed size is variable and determined post-AEAD; for uncompressed streams, the plaintext size equals the ciphertext minus the 16-byte AEAD tag, which requires parsing the ciphertext first). The library therefore mandates a worst-case buffer that can hold any valid decrypted chunk. **This is asymmetric with the encrypt side**: the encrypt output buffer uses `STREAM_ENCRYPT_MAX` (1,048,849 bytes), which is larger than `STREAM_CHUNK_SIZE` to accommodate compression overhead and the tag_byte. The decrypt minimum is the raw `STREAM_CHUNK_SIZE` because decrypt outputs plaintext (no tag_byte, no compression overhead). Binding authors who size the output buffer to the expected plaintext for a small final chunk (e.g., a 100-byte final chunk with a 100-byte output buffer) will receive `InvalidLength` with no diagnostic in the error message indicating that buffer size is the cause. See Appendix A for the constant value. diff --git a/_Sidebar.md b/_Sidebar.md index 689aed7c0b..4207fe6213 100644 --- a/_Sidebar.md +++ b/_Sidebar.md @@ -10,6 +10,8 @@ ### Trust +- [Paper](Paper) +- [Formal Verification](Formal-Verification) - [Audit & Testing](Audit-and-Testing) - [Security Policy](Security-Policy)