diff --git a/spec/modules/README.md b/spec/modules/README.md index 9f057b903..ef2b45881 100644 --- a/spec/modules/README.md +++ b/spec/modules/README.md @@ -52,6 +52,21 @@ Things that would surprise a competent Haskell developer reading the code for th - Alternatives considered and rejected - Known limitations and their justification +## Non-obvious threshold + +The guiding principle: **non-obvious state machines and flows require documentation; standard things don't.** + +Document: +- Multi-step protocols and negotiation flows (e.g., KEM propose/accept round-trips) +- Monotonic or irreversible state transitions (e.g., PQ support can only be enabled, never disabled) +- Silent error behaviors (e.g., `verify` returns `False` on algorithm mismatch instead of an error) +- Design rationale for non-standard choices (e.g., why byte-reverse a nonce, why hash-then-encrypt for authenticators) + +Do NOT document: +- Standard algorithm properties (e.g., Ed25519 public key derivable from private key) +- Well-known protocol mechanics (e.g., HKDF usage per RFC 5869, deterministic nonce derivation in double ratchet) +- Implementation details that follow directly from the type signatures + ## What NOT to include - **Type signatures** — the code has them @@ -107,6 +122,14 @@ This is valuable — it confirms someone looked and found nothing to document. ## Linking conventions +### Module doc → protocol docs +When a module implements or is governed by a protocol specification in `protocol/`, link to it near the top of the module doc (after the overview). Do not duplicate protocol content — just reference it: +```markdown +**Protocol spec**: [`protocol/pqdr.md`](../../../../protocol/pqdr.md) — Post-quantum resistant augmented double ratchet algorithm. +``` + +This is especially important for modules in transport, protocol, client, server, and agent layers where behavior is defined by the protocol spec rather than being self-evident from the code. + ### Module doc → other module docs Use fully qualified names as link text: ```markdown diff --git a/spec/modules/Simplex/Messaging/Crypto.md b/spec/modules/Simplex/Messaging/Crypto.md index f1c660512..10f074d5b 100644 --- a/spec/modules/Simplex/Messaging/Crypto.md +++ b/spec/modules/Simplex/Messaging/Crypto.md @@ -55,10 +55,6 @@ Both apply `pad`/`unPad` by default. The `NoPad` variants skip padding. The XSalsa20 implementation splits the 24-byte nonce into two 8-byte halves. The first half initializes the cipher state (prepended with 16 zero bytes), the second derives a subkey. The first 32 bytes of output become the Poly1305 one-time key (`rs`), then the rest encrypts the message. This is the standard NaCl construction. -## CbAuthenticator - -An authentication scheme that encrypts the SHA-512 hash of the message using crypto_box, rather than the message itself. The result is 80 bytes (64 hash + 16 auth tag). Used for authenticating messages where the content is transmitted separately from the authentication proof. - ## Secret box chains (sbcInit / sbcHkdf) HKDF-based key chains for deriving sequential key+nonce pairs: @@ -77,6 +73,22 @@ All keys are encoded as ASN.1 DER (X.509 SubjectPublicKeyInfo for public, PKCS#8 `GCMIV` constructor is not exported — only `gcmIV :: ByteString -> Either CryptoError GCMIV` is available, which validates that the input is exactly 12 bytes. This prevents construction of invalid IVs. +## verify silently returns False on algorithm mismatch + +`verify :: APublicVerifyKey -> ASignature -> ByteString -> Bool` uses `testEquality` on the algorithm singletons. If the key is Ed25519 but the signature is Ed448 (or vice versa), `testEquality` fails and `verify` returns `False` — no error, no indication of a type mismatch. A correctly-formed signature can "fail" simply because the wrong algorithm key was passed. + +## dh' returns raw DH output — no key derivation + +`dh'` returns the raw X25519/X448 shared point with no hashing or HKDF. Callers must apply their own KDF: [SNTRUP761](./Crypto/SNTRUP761.md) hashes with SHA3-256, the [ratchet](./Crypto/Ratchet.md#kdf-functions) uses HKDF-SHA512. Not all DH libraries behave this way — some hash the output automatically. + +## reverseNonce + +`reverseNonce` creates a "reply" nonce by byte-reversing the original 24-byte nonce. Used for bidirectional communication where both sides need distinct nonces derived from the same starting value. The two nonces are guaranteed distinct unless the original is a byte palindrome, which is astronomically unlikely for random 24-byte values. + +## CbAuthenticator + +An authentication scheme that encrypts the SHA-512 hash of the message using crypto_box, rather than the message itself. The result is 80 bytes (64 hash + 16 auth tag). This is the djb-recommended authenticator scheme: it proves knowledge of the shared secret and the message content, without requiring the message to fit in a single crypto_box, and without revealing message content even to someone who compromises the shared key after verification. + ## generateKeyPair is STM Key generation uses `TVar ChaChaDRG` and runs in `STM`, not `IO`. This allows key generation inside `atomically` blocks, which is used extensively in handshake and ratchet initialization code. diff --git a/spec/modules/Simplex/Messaging/Crypto/Ratchet.md b/spec/modules/Simplex/Messaging/Crypto/Ratchet.md index ebbc9c5a6..b26f95ce6 100644 --- a/spec/modules/Simplex/Messaging/Crypto/Ratchet.md +++ b/spec/modules/Simplex/Messaging/Crypto/Ratchet.md @@ -12,6 +12,8 @@ Implements the Signal double ratchet protocol extended with: The ratchet uses X448 (not X25519) for DH operations — `type RatchetX448 = Ratchet 'X448`. +**Protocol spec**: [`protocol/pqdr.md`](../../../../protocol/pqdr.md) — Post-quantum resistant augmented double ratchet algorithm. + ## PQ X3DH key agreement `pqX3dhSnd` / `pqX3dhRcv` perform the extended X3DH: @@ -46,9 +48,13 @@ Each message header carries `msgMaxVersion` (the sender's max supported ratchet `largeP` detects the length-prefix format by peeking at the first byte: if < 32, it's a 2-byte `Large` prefix (new format); otherwise it's a 1-byte prefix (old format). This allows upgrading the header encoding format in a single message without a version bump. +## maxSkip = 512 — DoS protection + +`maxSkip` is a hardcoded constant (not configurable). Messages claiming to be more than 512 positions ahead of the current counter are rejected with `CERatchetTooManySkipped`. This prevents an attacker from forcing the receiver to compute and store an unbounded number of skipped message keys. + ## Skipped message keys -When messages arrive out of order, the ratchet computes and stores the message keys for skipped messages (up to `maxSkip = 512`). Skipped keys are stored in a `Map HeaderKey (Map Word32 MessageKey)` — keyed first by header key, then by message number. +When messages arrive out of order, the ratchet computes and stores the message keys for skipped messages (up to `maxSkip`). Skipped keys are stored in a `Map HeaderKey (Map Word32 MessageKey)` — keyed first by header key, then by message number. The `SkippedMsgDiff` type represents changes to the skipped key store as a diff rather than a full replacement — this is persisted to the database, and the full state is loaded for the next message. `applySMDiff` is only used in tests. @@ -61,6 +67,14 @@ Decryption tries three strategies in order: If strategy 1 decrypts the header but the message number isn't in skipped keys, it checks whether this header key corresponds to the current or next ratchet to decide whether to advance. +### decryptSkipped — linear scan through all stored header keys + +`decryptSkipped` iterates through ALL `(HeaderKey, SkippedHdrMsgKeys)` pairs, attempting header decryption with each key. When header decryption succeeds but the message number is NOT in the skipped keys for that header, the result is `SMHeader` — which includes whether the key matches the current ratchet (`rcHKr` → `SameRatchet`) or the next ratchet (`rcNHKr` → `AdvanceRatchet`). This falls through to normal decryption processing rather than producing an error. + +### decryptMessage — ratchet advances even on failure + +`decryptMessage` returns `Either CryptoError ByteString` inside the `ExceptT` monad — a message decryption failure does NOT abort the ratchet state update. The ratchet counter advances (`rcNr + 1`) and chain key updates (`rcCKr'`) regardless of whether the message body decrypts successfully. This preserves ratchet state consistency for retransmission and error recovery. + ## rcEncryptHeader — separated from rcEncryptMsg Encryption is split into two steps: `rcEncryptHeader` produces a `MsgEncryptKey` (containing the encrypted header and message key), then `rcEncryptMsg` uses that key to encrypt the message body. This separation allows the ratchet state to be updated (persisted) before the message is encrypted, which is important for crash recovery — if the process crashes after encrypting but before sending, the ratchet state must already reflect the advanced counter. @@ -80,6 +94,19 @@ Two distinct newtypes with identical structure (`Bool` wrapper): - `PQSupport`: whether PQ **can** be used (determines header padding size, cannot be disabled once enabled) - `PQEncryption`: whether PQ **is** being used for the current send/receive ratchet +### pqEnableSupport is monotonic + +`pqEnableSupport v sup enc = PQSupport $ sup || (v >= pqRatchetE2EEncryptVersion && enc)`. The `||` means once PQ support is `True`, it stays `True` regardless of subsequent messages. PQ encryption (usage) can be toggled per-message; PQ support (capability / header size) only ratchets up. This prevents the larger header format from being downgraded once negotiated. + +## replyKEM_ — two-step KEM negotiation + +KEM establishment requires two message round-trips, as described in the [PQDR KEM state machine](../../../../protocol/pqdr.md#kem-state-machine): + +1. **Propose**: if the sender has no KEM in their header but the replier supports PQ at sufficient version, the replier includes a KEM proposal (`RKParamsProposed` — their encapsulation public key) +2. **Accept**: if the sender proposed KEM, the replier accepts by encapsulating against the proposed key and including the ciphertext + their own new encapsulation key (`RKParamsAccepted`) + +After acceptance, both sides have a shared KEM secret that is folded into the root KDF. Subsequent ratchet steps continue the KEM exchange with fresh keypairs on each side. + ## Error semantics - `CERatchetEarlierMessage n`: message number is `n` positions before the next expected (already processed or skipped-and-consumed) diff --git a/src/Simplex/Messaging/Crypto.hs b/src/Simplex/Messaging/Crypto.hs index d283ab899..79a9b593c 100644 --- a/src/Simplex/Messaging/Crypto.hs +++ b/src/Simplex/Messaging/Crypto.hs @@ -1285,11 +1285,13 @@ verify' (PublicKeyEd25519 k) (SignatureEd25519 sig) msg = Ed25519.verify k msg s verify' (PublicKeyEd448 k) (SignatureEd448 sig) msg = Ed448.verify k msg sig {-# INLINE verify' #-} +-- spec: spec/modules/Simplex/Messaging/Crypto.md#verify-silently-returns-false-on-algorithm-mismatch verify :: APublicVerifyKey -> ASignature -> ByteString -> Bool verify (APublicVerifyKey a k) (ASignature a' sig) msg = case testEquality a a' of Just Refl -> verify' k sig msg _ -> False +-- spec: spec/modules/Simplex/Messaging/Crypto.md#dh-returns-raw-dh-output--no-key-derivation dh' :: DhAlgorithm a => PublicKey a -> PrivateKey a -> DhSecret a dh' (PublicKeyX25519 k) (PrivateKeyX25519 pk) = DhSecretX25519 $ X25519.dh k pk dh' (PublicKeyX448 k) (PrivateKeyX448 pk) = DhSecretX448 $ X448.dh k pk @@ -1418,6 +1420,7 @@ randomCbNonce = fmap CryptoBoxNonce . randomBytes 24 randomBytes :: Int -> TVar ChaChaDRG -> STM ByteString randomBytes n gVar = stateTVar gVar $ randomBytesGenerate n +-- spec: spec/modules/Simplex/Messaging/Crypto.md#reversenonce reverseNonce :: CbNonce -> CbNonce reverseNonce (CryptoBoxNonce s) = CryptoBoxNonce (B.reverse s) diff --git a/src/Simplex/Messaging/Crypto/Ratchet.hs b/src/Simplex/Messaging/Crypto/Ratchet.hs index 5f91e728b..02ddd6a68 100644 --- a/src/Simplex/Messaging/Crypto/Ratchet.hs +++ b/src/Simplex/Messaging/Crypto/Ratchet.hs @@ -840,9 +840,11 @@ pqEncToSupport (PQEncryption pq) = PQSupport pq pqSupportAnd :: PQSupport -> PQSupport -> PQSupport pqSupportAnd (PQSupport s1) (PQSupport s2) = PQSupport $ s1 && s2 +-- spec: spec/modules/Simplex/Messaging/Crypto/Ratchet.md#pqenablesupport-is-monotonic pqEnableSupport :: VersionE2E -> PQSupport -> PQEncryption -> PQSupport pqEnableSupport v (PQSupport sup) (PQEncryption enc) = PQSupport $ sup || (v >= pqRatchetE2EEncryptVersion && enc) +-- spec: spec/modules/Simplex/Messaging/Crypto/Ratchet.md#replykem_--two-step-kem-negotiation replyKEM_ :: VersionE2E -> Maybe (RKEMParams 'RKSProposed) -> PQSupport -> Maybe AUseKEM replyKEM_ v kem_ = \case PQSupportOn | v >= pqRatchetE2EEncryptVersion -> Just $ case kem_ of @@ -994,6 +996,7 @@ data RatchetStep = AdvanceRatchet | SameRatchet type DecryptResult a = (Either CryptoError ByteString, Ratchet a, SkippedMsgDiff) +-- spec: spec/modules/Simplex/Messaging/Crypto/Ratchet.md#maxskip--512--dos-protection maxSkip :: Word32 maxSkip = 512 @@ -1131,6 +1134,7 @@ rcDecrypt g rc@Ratchet {rcRcv, rcAD = Str rcAD, rcVersion} rcMKSkipped msg' = do let (ck', mk, iv, _) = chainKdf ck mks' = M.insert msgNs (MessageKey mk iv) mks in advanceRcvRatchet (n - 1) ck' (msgNs + 1) mks' + -- spec: spec/modules/Simplex/Messaging/Crypto/Ratchet.md#decryptskipped--linear-scan-through-all-stored-header-keys decryptSkipped :: EncMessageHeader -> EncRatchetMessage -> ExceptT CryptoError IO (SkippedMessage a) decryptSkipped encHdr encMsg = tryDecryptSkipped SMNone $ M.assocs rcMKSkipped where @@ -1163,6 +1167,7 @@ rcDecrypt g rc@Ratchet {rcRcv, rcAD = Str rcAD, rcVersion} rcMKSkipped msg' = do decryptHeader k EncMessageHeader {ehVersion, ehBody, ehAuthTag, ehIV} = do header <- decryptAEAD k ehIV rcAD ehBody ehAuthTag `catchE` \_ -> throwE CERatchetHeader parseE' CryptoHeaderError (msgHeaderP ehVersion) header + -- spec: spec/modules/Simplex/Messaging/Crypto/Ratchet.md#decryptmessage--ratchet-advances-even-on-failure decryptMessage :: MessageKey -> EncRatchetMessage -> ExceptT CryptoError IO (Either CryptoError ByteString) decryptMessage (MessageKey mk iv) EncRatchetMessage {emHeader, emBody, emAuthTag} = -- DECRYPT(mk, cipher-text, CONCAT(AD, enc_header))