← Validation

Formal Proof Files

Formal-verification models and prover output (ProVerif .pv, Tamarin .spthy, CryptoVerif .cv) behind the six protocol proofs on the Validation page. They hold protocol abstractions and prover results only, no QNSQY source. All of them are also in qnsqy-formal-proofs-v1.tar.gz (SHA-256).

• README.txt 2,955 bytes
• RESULTS.txt 1,244 bytes
• aead.cv 1,182 bytes
• aead.cv.out 8,609 bytes
• aead_secrecy.cv 744 bytes
• aead_secrecy.cv.out 3,086 bytes
• aead_secrecy2.cv 746 bytes
• aead_secrecy2.cv.out 3,100 bytes
• billing_token.out 2,073 bytes
• billing_token.pv 1,583 bytes
• multi_recipient.out 1,391 bytes
• multi_recipient.pv 1,304 bytes
• ratchet_fs.out 2,111 bytes
• ratchet_fs.pv 1,592 bytes
• ratchet_pcs.pv 1,939 bytes
• ratchet_pcs.pv.out 2,110 bytes
• ratchet_pcs.retry.out 462 bytes
• ratchet_pcs.spthy 1,628 bytes
• ratchet_pcs.tamarin.out 443 bytes
• remote_manifest.out 1,640 bytes
• remote_manifest.pv 1,526 bytes
• rollback.spthy 2,110 bytes
• rollback.tamarin.out 4,603 bytes