AliceDone or BobDone was logged at trace index i with keys.

Block k of keys was directly exposed as Triple Ratchet session state (ExposedSpqr for pqr, ExposedCKr / ExposedCKs for ck, or ExposedRK for rk) on a session started by a handshake deriving keys.

Compromise excuse for Alice's handshake key at i (Bhargavan et al., Theorem 7): either IK_B was compromised (before i, or alongside spk and PQProtectionBypassed), or BrokenDH occurred (before i, or alongside PQProtectionBypassed).

Secrecy of Alice's handshake blocks (Theorem 7).

Pre-acceptance authentication compromise excuse at i (Theorem 8): IK_A, Bob's spk, or DH was compromised strictly before i.

Agreement witness for Theorem 8: a logged AliceDone strictly before i on the same pqpk, spk (up to SameDHKey), and opk (up to SameOPK).

Authentication of Alice to Bob (Theorem 8).

Compromise excuse for Bob's handshake key at i (Theorem 9): pre-acceptance authentication compromise, compromise of all of Bob's session secrets (IK_B, spk, opk, and pqpk/KEM), or BrokenDH paired with PQProtectionBypassed.

Secrecy of Bob's handshake blocks (Theorem 9).

Premise for handshake forward secrecy at i: identity keys are compromised only after i, session spk and pqpk are uncompromised, and neither DH nor the KEM is broken.

Handshake forward secrecy (Theorem 1).

Premise for harvest-now-decrypt-later resistance at i: BrokenDH occurs only after i, the KEM is unbroken, and ikA, ikB, spk, and pqpk are not explicitly compromised.

Harvest-now-decrypt-later resistance (Theorem 1).

Key-compromise-impersonation resistance (Theorem 1).

Peer authentication (Theorem 1).

Premise for session independence: identity keys, DH, and the KEM are uncompromised, and only prekeys distinct from (spk, pqpk, opk) are compromised.

Session independence against compromise of other sessions' prekeys (Theorem 1).

Ratchet secret k was compromised on tr: directly exposed (ExposedRK, ExposedDHs, ExposedCKs, ExposedCKr, ExposedMK), derived from HandshakeRootCompromised, or an HonestDHKey under BrokenDH (ExposedSpqr excuses no ratchet secret).

Ratchet forward secrecy (Cheval et al., Table 2): if TRKeyKnown Knows seed pqSalt holds for a used seed, then seed, an ancestor chain key (DerivesMsgKey), or an ancestor root key (DerivesChain) satisfies CompromisedKey.

Ratchet post-compromise security (Cheval et al., Table 2): if seed descends from a healing DH step createChain rk_prev (dhPk peerSk) ownSk between honest DH secrets ownSk and peerSk and TRKeyKnown Knows seed pqSalt holds, then seed, a post-heal chain or root key, or both a pre-heal root key and one of (ownSk, peerSk) satisfies CompromisedKey.

Conjunction of all ten whole-trace security queries on tr against Knows.

Conjunction of all ten security properties over reachable traces of Composed.reachability.