Pixieby Sociofabric

Algorithm: Sealing the Envelope

A deep dive into the exact bytes: what goes inside the seal, what stays outside, and the one MAC (a message authentication code, a keyed checksum) that ties them together so a message is authentic, replay-proof, and deniable all at once.

This is the wire-format counterpart to Sealed Sender, The Envelope, and Deniability. It assumes you have read those; here we assemble their ideas into the concrete object that travels the network.


1. Two nested structures

Every message is two structures, one inside the other.

The inner payload is what only Bob can read. Before encryption, it is built as three parts joined end to end (that is what the ‖ symbol below means):

InnerPayload =  SenderCert  ‖  MAC(channel_key, header_preimage)  ‖  CBOR(Payload)

This whole InnerPayload is then handed to libsignal's session cipher (libsignal is the open-source cryptographic engine behind the Signal messenger), which encrypts it under the PQXDH + Double Ratchet + SPQR session. The output is the sealed_payload: opaque, post-quantum bytes with forward secrecy, meaning past messages stay unreadable even if today's keys later leak. (The sealed-sender property here comes from our own envelope, not from libsignal's sealed-sender mode: what hides the sender is that the identity rides inside these bytes.)

The outer envelope is what the relay reads. It wraps the sealed payload with exactly the routing and handling fields established across the series:

Envelope = { to, envelope_id, wake_class, created_at, ttl_secs, cert_id,
             rate_limit_token, sealed_payload }

Each field is one the series has already met. to is the rotating per-pair address. envelope_id is 16 bytes, unique to this envelope. It is what makes each authenticator unrepeatable. wake_class is the coarse 6-value class. created_at is the send time, rounded into a 5-minute bucket. ttl_secs says how long the envelope may sit in the delivery window. cert_id is the per-conversation coat-check ticket. And rate_limit_token is the single-use admission token.

It travels the WebSocket (the long-lived, two-way connection each device keeps open to the relay) as a binary frame with a one-byte tag (0x01 for a normal message; a separate 0x02 tags a first-contact discovery frame). The formal schema lives in the project's CDDL definition. CDDL is a small language for pinning down the exact shape a CBOR structure is allowed to take (RFC 8610).

WHAT ONLY BOB CAN READ WHAT THE RELAY READS SENDER CERT MAC · CHANNEL KEY CBOR PAYLOAD CONCATENATED, THEN SEALED THE SEAL PQXDH · RATCHET · SPQR TO — ROUTING KEY WAKE_CLASS — COARSE 6-VALUE CREATED_AT — 5-MIN BUCKET CERT_ID — COAT-CHECK TICKET RATE_LIMIT_TOKEN — SINGLE-USE SEALED_PAYLOAD TWO STRUCTURES — THE RELAY READS ONLY THE OUTER ONE

2. The MAC that replaced a signature

The middle field is where three requirements meet, so it is worth dwelling on.

Earlier designs put an Ed25519 signature here: Alice signing each message. As Deniability explained, that is transferable proof and had to go. The replacement is an HMAC (the standard recipe for building a message authentication tag out of a hash function) computed under the pairwise channel key, a secret Alice and Bob share for their conversation and no one else holds:

That handles who. The MAC also has to handle replay: stopping the relay, or anyone, from lifting a valid message and re-injecting it later. It does so by what it is computed over: the header_preimage, which is just the outer header's fields laid out in a fixed order as one byte string, the exact input the tag is computed on.

That preimage binds the MAC to this specific envelope (its routing address, its unique envelope_id, its coarse class, its bucketed time, its lifetime, its certificate), so the tag is only valid in the exact envelope it was made for, and the envelope_id is what makes it unrepeatable rather than merely header-shaped.

Copy the sealed payload into a different envelope and the recipient's recomputed MAC won't match; replay the same envelope and the message's double-spent token is already burned. The MAC is the glue between the sealed inside and the visible outside: it makes the outer header tamper-evident to the recipient without making it readable by the relay.

One header field is pointedly left out of the preimage: the anonymous rate-limit token. That is deliberate. If the sender's authenticator covered the token, the pair would be cryptographically joined, and a relay holding both could tie a spent credential to a particular sender's channel. Leaving it uncovered keeps admission and authentication in separate worlds, which is the whole reason the token can be anonymous at all.

ORIGINAL ENVELOPE CHANGED ENVELOPE BOB HEADER PREIMAGE TO BOB SILENT T+5M CERT7 MAC BINDS THE HEADER SEALED PAYLOAD + MAC TRANSPLANT ATTACK TO CAROL SILENT CERT7 COPIED SEALED PAYLOAD MAC CHECK HEADER CHANGED REJECT EXACT REPLAY TOKEN LEDGER ALREADY SPENT REJECT CHANGE THE OUTSIDE → MAC FAILS · REPEAT IT EXACTLY → TOKEN FAILS THE MAC BINDS THIS SEALED INSIDE TO THIS EXACT OUTSIDE

3. What each layer defends

It helps to see the construction as concentric shells, each answering a different attacker:

Layer Protects against Mechanism
sealed_payload (libsignal) a relay reading content; a recorder decrypting later PQXDH + ratchet + SPQR
SenderCert (inside) an impostor claiming to be Alice hybrid Ed25519 + ML-DSA-65 signature Bob verifies
MAC(channel_key, …) (inside) forgery and replay and courtroom transfer pairwise-key HMAC over the header preimage
cert_id / wake_class / created_at (outside) the relay learning identity / type / precise time minimized to a ticket, a coarse class, a fuzzy time

The design rule visible in that table: anything that could identify, prove, or reveal lives inside the seal; only the irreducible routing-and-handling residue lives outside, and the MAC stitches the two so the outside cannot be tampered with undetected.

ATTACKER THE LAYER THAT STOPS IT PROTECTED FACT RELAY + FUTURE RECORDER PQXDH + RATCHET + SPQR CONTENT STAYS SECRET IMPOSTOR HYBRID SENDER CERT SENDER AUTHENTIC FORGER · REPLAYER THIRD-PARTY JUDGE PAIRWISE HEADER MAC AUTHENTIC · BOUND NON-TRANSFERABLE METADATA OBSERVER TICKET · COARSE CLASS FUZZY TIME ONLY IDENTITY · TYPE EXACT TIME HIDDEN ONE ENVELOPE · FOUR DISTINCT DEFENSE JOBS EVERY LAYER HAS ONE ATTACKER IT MUST STOP

4. A machine-checked guarantee

The security-critical claim here is that the v4 MAC ("v4" is simply the envelope format's current version) is strongly unforgeable: no one without the channel key can produce a valid (envelope, tag) pair the recipient will accept, even after seeing many legitimate ones, which is what makes the replay and forgery defenses real rather than hopeful.

That property is called SUF-CMA: "strong unforgeability under chosen-message attack," where the forger even gets to see valid tags on messages of its own choosing and still cannot make a new one. It is proved by machine for this construction, in two styles: a computational model in EasyCrypt, a proof assistant that tracks an attacker's actual odds of winning, alongside a symbolic model in ProVerif, a tool that treats the cryptography as ideal and hunts for flaws in the message flow. They are the same two provers, used the same two ways, that check the envelope's indistinguishability claim. The sealing is not just assembled and tested; the core unforgeability is a checked theorem.


5. Why this order, and this serialization

A couple of choices that look arbitrary but aren't:


References & further reading

← Deniability: Messages No One Can Prove You SentAlgorithm: The Admission Token (Lattice OPRF) →