crypto formal verification

Research, not an audit

These pages are research and development and may not match the live app. Do not treat this as an audit. Shared for testing and demo only. Please use responsibly.

crypto is two crates with different trust jobs. Password sealing of your files is not the recipient cascade. Gallery: positive-intentions.github.io/crypto. Same claim words as the other library pages. A green job is not a proof of the Glitr messenger.

Start from the verification report.

crypto-core (password envelope and primitives)

crypto-core owns mailbox sealing and primitive glue:

$$\begin{aligned} k &= \mathrm{Argon2id}_{m=19456,\,t=2,\,p=1}(\mathit{password},\; \mathit{salt}), \\ c &= \mathrm{AES\text{-}256\text{-}GCM}_{k,\,\mathit{nonce}}(m), \\ \mathrm{env} &= (v{=}1,\; \mathrm{kdf}{=}1,\; \mathrm{aead}{=}1,\; \mathit{salt}_{16},\; \mathit{nonce}_{12},\; c). \end{aligned}$$

Also: AES-256-GCM, RSA-OAEP-4096 + AES hybrid, SHA-256/512 and SHA3-512, and a generic ordered-layer manager that nests inner parameters into the next plaintext.

Production enables crypto-backend. Extraction builds --no-default-features. Stubs use AbstractCrypto.

Executable tests

Suite	What it covers	Gate
Rust tests (both features)	Envelope guards, AES/RSA hybrid, cascade encode/decode, empty password	Must pass
Line coverage	crypto-core	100% lines on both feature builds (CI runs production and --no-default-features; npm run test:rust:coverage:ci is production only)
Official KATs	NIST SHA-256/512, SHA3-512, AES-256-GCM	Must pass
Argon2id	RFC 9106 params do not match (19 MiB, t=2, p=1). A pinned implementation vector is replayed and labeled as not an RFC vector	Must pass
proptest	Password round-trip, AES tamper, RSA wrap, chunk inverse, cascade reverse	Must pass
Fuzz	Envelope fields, decode_chunks, AES decrypt blobs, RSA DER	Time-boxed CI
WASM	Password envelope, AES tamper, empty-password reject	Must pass

Wrapper lemmas

Proved on the spec: empty password fails before KDF; wrong-length AES key/nonce fails before AEAD; decode_chunks rejects truncated prefixes.

Assumed: Argon2id, AES-GCM, RSA-OAEP, SHA-2/3, CSPRNG.

Argon2 in ProVerif is a public KDF equation — not a memory-hard proof.

Symbolic models (ProVerif)

Model	Queries
password_security.pv	Attacker without the password does not obtain plaintext; decrypt \Rightarrow encrypt
password_roundtrip.pv	Honest recover; empty password rejected as an event
aes_security.pv	Plaintext secrecy; tamper fails
rsa_hybrid.pv	RSA-OAEP wrap of an AES key; plaintext secrecy
cascade_core.pv	Ordered Aes + Password layers; inner key material not in the clear beside the outer ciphertext

crypto-cascade (product composition)

crypto-cascade owns product composition, not new primitives: encrypt_for_peer / decrypt_from_peer, layer adapters, JSON wire v3. Password sealing stays outside this crate.

Optional feature mls-layer exposes an MlsLayer stub that implements CipherLayer but is not inserted into encrypt_for_peer. Wire stays v3. Group create/add/welcome live in the sibling mls library.

The full product crate is not extracted through hax (it pulls three protocol cores). Composition is modeled symbolically and cites sibling models.

Executable tests

Suite	What it covers	Gate
Clippy / cargo test	Product crate in CI (sibling checkout)	Must pass
Line coverage	crypto-cascade	Intended 100% llvm-cov gate (--fail-under-lines 100). After removing blanket coverage(off), the last measured run was not 100% (product/layers still have a handful of instrumented lines). Only u32_from_be4 stays excluded.
Unit tests	Identities → encrypt → decrypt; second message uses stored ratchets; v2 legacy still decrypts; tampered outer ML-KEM fails; password is never a cascade layer	Must pass

Symbolic models (ProVerif)

Model	Queries
product_cascade.pv	Encrypt order AES → Signal → PQXDH → RSA → ML-KEM; decrypt reverse; plaintext secrecy against the network attacker
wire_v3.pv	Only outermost ML-KEM ciphertext and public headers on the wire
first_message.pv	Signal and PQXDH handshake blobs ride inside inner layers
layer_independence.pv	The honest process uses all five layers

Queries are Modeled on an idealized nesting. They do not prove Signal, PQXDH, ML-KEM, RSA, or AES. They do not prove git mailbox delivery, a stolen device, or db-core sealing of ProtocolSecrets.

Automated jobs

Job	What it runs
Format, Clippy, tests	crypto-core (both features) and crypto-cascade
Coverage	100% lines on crypto-core (both features in CI). Cascade uses the same --fail-under-lines 100 command; qualify until that gate is green after unhiding helpers.
WASM	Node wasm-pack on core bindings
ProVerif	Core + cascade models
F* / Rocq / Lean	crypto-core stub extract / AbstractCrypto
Fuzz	Time-boxed cargo-fuzz

verify:host:full is ProVerif + F* + Rocq + Lean. There is no libcrux job.

What this does not prove

• The Glitr messenger
• Git mailbox delivery or a compromised host
• Argon2id as a memory-hard function
• AES-GCM, RSA-OAEP, or SHA internals
• Signal, PQXDH, or ML-KEM (those have their own pages; cascade models cite them)
• Refinement from production backends to AbstractCrypto
• Extracting encrypt_for_peer through hax

Next: Cryptography and Persistence.