# ProVerif formal verification results — 2026-06-13T17:04:58Z
# proverif Proverif 2.05. Cryptographic protocol verifier, by Bruno Blanchet, Vincent Cheval, and Marc Sylvestre

===== billing_token.pv =====
RESULT not attacker(apikey[]) is true.
RESULT event(TokenAccepted(t)) ==> event(TokenIssued(t)) is true.

===== multi_recipient.pv =====
RESULT not attacker(dek[]) is true.
RESULT not attacker(payload[]) is true.

===== remote_manifest.pv =====
RESULT event(Restored(g_1,oh_1)) ==> event(Uploaded(g_1,oh_1)) is true.

===== ratchet_fs.pv =====
RESULT not attacker_p1(msg[]) is true.

# --- post-compromise security (PCS): NOT CLAIMED AS PROVEN ---
# The query below closes, BUT ratchet_pcs.pv signs every ratchet ephemeral with
# the long-term identity key, while the shipping qs-chat ratchet leaves ratchet
# public keys UNSIGNED (chain-key authenticated only, like Signal). The model is
# therefore a stronger-authentication variant, not the deployed protocol, so PCS
# is listed as OPEN on the validation page. Tamarin (ratchet_pcs.spthy) did not
# converge. Published for transparency, not counted among the proven properties.
===== ratchet_pcs.pv (non-faithful model; PCS remains OPEN) =====
RESULT not attacker_p1(msg[]) is true.