QNSQY formal-verification models and results
============================================
These are the machine-checked security proofs referenced on
https://quantumsequrity.com/validation (Section 4.5).

They contain protocol ABSTRACTIONS and prover output only. They contain
NO QNSQY proprietary source, no file-format internals, and no findings.
They prove properties of the abstract protocol MODELS, not of the shipping
Rust implementation; there is no automated model-to-code link.

Provers (install via opam / Homebrew):
  - ProVerif 2.05  : billing_token.pv, multi_recipient.pv, remote_manifest.pv,
                     ratchet_fs.pv
                     (ratchet_pcs.pv is also included but is NOT counted as a
                      proof of the shipping protocol; see "Open" below)
  - Tamarin        : rollback.spthy   (ratchet_pcs.spthy did NOT converge)
  - CryptoVerif    : aead.cv, aead_secrecy.cv

Run, e.g.:
  proverif billing_token.pv          # expect: RESULT ... is true (x2)
  tamarin-prover --prove rollback.spthy   # expect: no_rollback verified
  cryptoverif aead.cv                # expect: RESULT Proved event(accept) ==> event(sent)

RESULTS.txt          : consolidated ProVerif verdicts.
rollback.tamarin.out : Tamarin anti-rollback proof (no_rollback verified, 12 steps).
aead.cv.out          : CryptoVerif AEAD integrity proof.

Proven (no attack exists):
  1. Billing: API-key secrecy + ML-DSA-44 subscription-token unforgeability.
  2. Multi-recipient: an outsider with no recipient key learns neither the data key nor the data.
  3. Remote backup: a malicious bucket cannot tamper with or substitute objects undetected.
  4. Remote backup: a malicious bucket cannot roll the client back to an older generation.
  5. qs-chat: forward secrecy holds after long-term key compromise.
  6. AEAD: forged ciphertext is rejected (computational integrity, INT-CTXT).

Open (stated honestly, NOT claimed as proven):
  - qs-chat post-compromise security (self-healing). ratchet_pcs.pv DOES close a
    self-healing query, but ONLY under an assumption that does NOT match the
    shipping protocol: it signs every new ratchet public key with the parties'
    long-term identity keys and gates on checksign. The real qs-chat ratchet
    (like Signal's Double Ratchet) leaves ratchet public keys UNSIGNED in the
    message header and authenticates them through the symmetric key chain.
    Identity-key signing is strictly stronger than chain-key authentication, so
    ratchet_pcs.pv proves an easier variant, not the deployed ratchet. The
    Tamarin model of the same property did not converge. PCS is therefore listed
    as OPEN. The model is published anyway so the gap and the work are visible.
  - AEAD computational secrecy is content-only: the CryptoVerif IND-CPA secrecy
    query did not resolve because the symmetric-encryption model does not hide
    plaintext length. Integrity (INT-CTXT) IS proven; length is not hidden.
