NyxChat is a serverless, end-to-end encrypted messenger for Android. This document states precisely what protocol v4 protects, what it does not, and how to report problems. Claims are limited to what the code in lib/core/crypto, lib/core/network, lib/core/mesh and lib/core/relay implements and what the automated tests exercise. Tamarin models of the handshake and asynchronous initiation are in formal/.

Open a private security advisory on GitHub or email the maintainer listed in pubspec.yaml. Include the protocol version (v4), a reproduction and the impact. We aim to acknowledge within 7 days.

Passive observer (Wi-Fi or Bluetooth):

• Cannot read message contents, in-conversation metadata or file contents.
• In private discovery mode cannot tell that a device runs NyxChat, cannot learn its handle or name, and cannot track it across 15-minute slots. In public mode the handle and name are visible.
• Can see that two devices exchange traffic, packet size buckets and timing. Cover traffic reduces, but does not eliminate, timing analysis.

Active network attacker (MITM on first contact):

• Cannot complete a handshake as a known contact (pinned keys, signed transcript, nonce echo).
• On true first contact without a contact card, TOFU applies: one substitution window, closed by safety-number comparison or scanning a card.

Mesh relay (untrusted intermediate device):

• Cannot read, forge or re-address envelopes (sealed for the pair, AAD-bound) and cannot see identities or ratchet headers.
• Can link a recipient token to a reply token within one hour and count packets; cannot link across epochs. Can drop, delay or replay packets (replays are rejected end to end). Learns which packet ids were acknowledged.

Public Nostr relay:

• Sees daily tokens, event sizes and timing, and a throwaway key per event; cannot read content or learn identities. Can drop or delay.

Device seizure (locked, password enabled):

• Must brute-force the password through Argon2id from a disk image; the in-app attempt counter does not bound an offline attacker. Without a password, protection rests on the Android keystore and lock screen.
• Under coercion the duress password opens a decoy profile with its own keys and empty history; if configured, the real profile is destroyed first.

Compromise of long-term keys:

• Past direct-link sessions stay confidential (ephemeral X25519 keys and an ephemeral ML-KEM key in every handshake, so neither a classical nor a quantum adversary gains from a later key compromise). Asynchronous sessions started with a one-time prekey are protected from the first message (the recipient deleted the prekey's private half on use); a session that had to fall back to the long-term KEM key is protected from the first reply onward. Pair-derived keys (presence, mesh, relay tokens, sealed-sender wrapper) are static-DH based and are therefore exposed: an attacker with a victim's identity key can recognise the victim's beacons and unseal the outer wrapper of past mesh/relay traffic, but the inner envelope remains ratchet-protected. The victim should rotate keys (signed transition) and contacts re-verify.

1. No physical-device field measurements yet for BLE, Wi-Fi Direct and Wi-Fi Aware; behaviour across Android vendors, throughput and battery are untested by the maintainers.
2. Not a FIPS 140-3 module. ML-KEM-768 is the PQClean reference code verified against ACVP vectors, compiled with the NDK; side-channel behaviour of the surrounding pure-Dart X25519/Ed25519/AES code has not been evaluated.
3. Pair keys are static-DH derived (see above): compromise of an identity key exposes token unlinkability and the outer wrapper retroactively.
4. Bloom beacons have false positives (about 2% per stranger at 10 contacts on BLE); a false positive only causes a handshake attempt that fails harmlessly, but leaks that the scanner has some contact whose token collided.
5. Group membership is authenticated only to current members; any member can add anyone.
6. Legacy v2 handles (32 bits of key material) are still accepted; trust rests on pinned keys.
7. Nostr relays have size limits (48 KiB payload) and may require authentication (NIP-42, unsupported); the client falls back to other carriers.
8. Formal models cover the handshake and asynchronous initiation, not everything. Three Tamarin theories are machine-checked with Tamarin 1.12.0 (formal/RESULTS.md): all 12 handshake lemmas and all 9 asynchronous-initiation lemmas (including post-quantum forward secrecy through one-time prekeys) verify; of the collision-rule theory the executable trace is found and its three consistency lemmas are undecided within a five-minute budget (no counterexample). The ratchet, group sender keys and mesh privacy are tested but not modelled. Writing and checking the models surfaced four protocol fixes now implemented: binding the responder's signature to the initiator's hello, a responder-side nonce cache, rejecting stale initiation blocks from a lost collision (the loser announces the ephemeral it abandoned, the winner blacklists every init it ignored), and remembering every accepted initiation ephemeral so a replayed older initiation cannot rebuild a stale session.
9. No external audit.
10. Asynchronous sessions without a prekey are the weaker case. A one-time prekey exists only for contacts met on a direct link since 3.2, and each initiation consumes one of eight; when none is left the session starts against the long-term KEM key and gains post-quantum forward secrecy only at the first reply. The contact screen shows this state. Unused prekeys are part of encrypted backups, so restoring a backup can bring back a private half the live device had already deleted: a session that used it is then only as confidential as that backup.

bash tool/build_native.sh        # or pwsh tool/build_native.ps1 on Windows
flutter test test/crypto         # ratchet, handshake, ML-KEM KATs, sender keys, sessions, one-time prekeys, pair keys, beacons, mesh, key transition, trust, outbox
flutter test test/fuzz           # seeded fuzzing of every wire parser and the BLE reassembler
flutter test test/integration    # two/three full stacks: handshake, receipts, reconnect, reset, sealed mesh, groups, prekey bundles and mesh sessions with one-time prekeys
flutter test test/relay          # Nostr transport against an in-process mock relay