A signed pre-key: its private half (the public half is derived, keyPairOf), its signature and its timestamp.

A Kyber1024 pre-key: public and secret key, its signature and its timestamp.

A party's state on PQXDH directories: everything its directory holds.

The record of a one-time pre-key with id id (PreKeyRecord::serialize).

The files of a party's directory (paths relative to it):

• address (text), identity-key-pair (IdentityKeyPair::serialize: the public key derived from the private key, and the private key), registration-id (u32 little-endian);

• identities/<peer name>: the peer's pinned identity key, if any;

• sessions/<peer address>: the session's record (encodeRecordUnderExtras), if any;

• each signed pre-key, one-time pre-key and one-time Kyber pre-key record (an empty file when used), each last-resort Kyber pre-key record and its .base-keys file (always written). The directories are partyDirs.

The inputs of one call of the party st with command cmd: its directory, the files extra (the bundle directory for init), the coins file coins, and stdin stdin.

The bundle directory's contents for a typed bundle (public.rs): keys serialized behind their type bytes.

init <peer> bundle by st with the typed bundle b in the bundle directory and the 192 coin bytes t.

The trust check (is_trusted_identity, trust on first use): no pinned key, or the pinned key is k.

init's model (process_prekey_bundle): the trust check of the bundle's identity key, then initiateState (the bundle's signatures, PQXDH, the initiator session; null on any failure); on success the peer's identity key is pinned and the session stored. Never panics.

send's model (message_encrypt): no session rejects; else the session model's messageEncrypt with V1 SPQR, the party's address blob and the coins r (panic aborts, other errors reject), then the trust check of the session's remote identity. On success the new session (same extras) and the remote identity pinned; stdout 3 ‖ firstMessageBody while unacknowledged, else 2 ‖ SignalMessage, as sendWireModel.

The receiving session's outcome for a parsed SignalMessage msg of type ty on the session (x, g) (decrypt_message_with_record on a record without previous sessions): the session model's tryDecryptFromRecord (the party's expected addresses, coins rc; panic aborts, other errors reject), then the trust check of the remote identity; on success the new session (same extras, ghost state otherwise unchanged) and the plaintext.

recv's model on 2 ‖ c (message_decrypt_signal): no session rejects; c that does not parse (SignalMessage::try_from) rejects; else pqxdhSessionDecryptModel with type Whisper.

The pre-keys a pre-key message m names, from st's stores, as ResponderPreKeySecrets (none: one is missing, so libsignal rejects):

• the signed pre-key m.spkId (get_signed_pre_key);

• the Kyber pre-key m.kpkId (get_kyber_pre_key): the one-time key if its file is not empty, else the last-resort key with that id;

• the one-time pre-key m.opkId, if m names one (get_pre_key): a used (empty) one is missing.

mark_kyber_pre_key_used(m.kpkId, m.spkId, m.baseKey) on st's stores (none: the store refuses, so libsignal rejects): a one-time Kyber pre-key whose file is not empty is emptied; else the last-resort key m.kpkId refuses when its .base-keys replay list exceeds fileCapBytes (37 * seen.length > fileCapBytes, where Dir::get / readFileHook returns Err) or holds the (signed pre-key id, base key) pair ("reused base key"), and otherwise appends it.

remove_pre_key(m.opkId), if m names a one-time pre-key: its file is emptied.

recv's model on 3 ‖ m.bytes for a typed pre-key message m (message_decrypt_prekey):

1. m.inner that does not parse (SignalMessage::try_from) rejects (PreKeySignalMessage:: try_from parses it);

2. the trust check of m's identity key (process_prekey);

3. with a session that matches m (PqSessionMatches; promote_matching_session): the session's remote identity must be m's identity key, then the session's tryDecryptFromRecord with type PreKey; no pre-key is used;

4. with no session: preKeysNamedBy (a missing pre-key rejects), recvPrekeyState (PQXDH, the recipient session, the first decryption; panic aborts), markKyberUsed (a refusal — missing key, last-resort .base-keys above fileCapBytes, or replayed base key — rejects with exit 1 and files unchanged), then removeOpk;

5. on success m's identity key is pinned and the session stored; stdout is the plaintext. A session that does not match m is outside CliSpecPqxdh's domain (libsignal would archive it, and encodeRecordUnderExtras writes no previous sessions: DEV-C-PREV); the model then rejects.

The party states CliSpecPqxdh covers (the games keep their parties in it):

• a session, if any, encodes as a reachable one (ReachablePqxdhSession: a PQXDH handshake started it and the wire entries continued it) for st's identity: some reachable g₀ has the same party and session state, is st.party's, and its record is below 2^31 bytes (the bound ReachablePqxdhSession's steps carry);

• every file of the directory is below 2^31 bytes, and every file other than a last-resort .base-keys file (baseKeysFile i) is at most fileCapBytes (2^21) bytes;

• the pre-key ids of each kind are distinct (each names one file).

DEV-CLI21 (libsignal): bounded I/O caps and stated last-resort .base-keys cap rejection (effect: none). Each CLI run enforces the bounded-read I/O caps (stdinCapBytes = 2^20, fileCapBytes = 2^21, cliPathMaxBytes = 4096) and refuses send plaintext above maxPlaintextBytes (1_000_000) with exit 1. In PqxdhPartyInSpecDomain and markKyberUsed: (i) non-.base-keys files are at most fileCapBytes (ReachablePqxdhSession records are ≤ 1,209,331 B; other store files are fixed-size), while .base-keys (baseKeysFile i) stays below 2^31 bytes; (ii) the .base-keys read cap (37 * seen.length > fileCapBytes in markKyberUsed, from the 56,681-st handshake on one unrotated last-resort key) is a modelled exit-1 rejection with files unchanged; (iii) cliPqExp never reaches that rejection (seen.length ≤ 1).

The session conjunct ignores ghost epochs (GhostState.epoch, chainEpochs), which are not serialized by encodeRecordUnderExtras.

The CLI on PQXDH directories (run is any implementation; the real one is the engine process of the CLI's ELF). For every model primitives W and model extras X, every party state st in the domain (PqxdhPartyInSpecDomain), and each call below, standard input above stdinCapBytes (2^20) exits 2 (read_stdin cap), send plaintext above maxPlaintextBytes (10^6) exits 1 before running the model (with every file unchanged in both cases), and otherwise the run's outcome is the model's (pqxdhExpectedOutcome):

1. init <peer> bundle with no session (DEV-C-PREV), any typed bundle b and the 192 coin bytes t: pqInitModel;

2. send <peer> of any plaintext m below 2^32 bytes with the 64 coin bytes r: exit 2 if m.length > stdinCapBytes, else exit 1 if m.length > maxPlaintextBytes, else pqSendModel;

3. recv <peer> of 2 ‖ c for any c below 2^32 bytes, with coins rc: exit 2 if (2 ‖ c).length > stdinCapBytes, else pqRecvWhisperModel;

4. recv <peer> of 3 ‖ m.bytes for a typed pre-key message m (other encodings are outside the domain) whose inner message is below 2^32 - 2048 bytes, when there is no session or the session matches m (DEV-C-PREV), with coins rc: exit 2 if (3 ‖ m.bytes).length > stdinCapBytes, else pqRecvPrekeyModel;

5. recv <peer> of any input below 2^32 bytes whose first byte is neither 2 nor 3, or of nothing: exit 2 if c.length > stdinCapBytes, else exit 1, with every file unchanged. In 1–4 m's registration id, ids, keys and inner message are any values (the adversary's).