============================================================================== MVPS PROOF ENVELOPE -- MATHEMATICAL EXISTENCE PROOF (Tamper-evident binding of theorem catalogues, validators, and numerical receipts; optional Post-Quantum Protection profile) "A criptografia nao prova o teorema. Ela prova que ninguem trocou o teorema. O teorema continua sendo verdade pela matematica -- e isso ninguem quebra, nem maquina quantica, porque ja esta provado." -- selo final MVPS ============================================================================== Mathematical assembly: Leonardo Melegassi (Catellix) Produced: 2026-05-28 Companion: docs/draft-melegassi-ippm-mvps-proof-envelope-00.txt Siblings: docs/MVPS_CWT_MATHEMATICAL_PROOF.txt docs/MVPS_TRUST_MATHEMATICAL_PROOF.txt docs/MVPS_PERFSEC_COUPLING_PROOF.txt Extends: docs/MVPS_MATHEMATICAL_EXISTENCE_PROOF_V4.txt (v4.0 catalogue) Registry: docs/MVPS_IETF_FOUNDATIONS.txt (theorem traceability table) Numerical receipt: scripts/validate_proof_envelope.py (exit 0 required) evidence/proof_envelope_receipt.json ============================================================================== 0. WHAT THIS DOCUMENT IS (AND IS NOT) ============================================================================== This is a self-contained mathematical specification of the MVPS Proof Envelope: the layer that BINDS the existing MVPS proof artifacts (companion .txt documents, validator scripts, numerical receipts) into a single canonical, tamper-evident manifest, anchored by the witness- cosigned checkpoint machinery already specified in docs/MVPS_CWT_MATHEMATICAL_PROOF.txt. This document has three properties parallel to v4.0 and CWT: (i) Every Theorem reduces to an imported cryptographic result (collision resistance, EUF-CMA, PRF) OR to a definitional / constructive chase. (ii) Every binding claim is about ARTIFACTS, never about the mathematical truth of the bound theorems. The truth of T1..T9, T-COAL-1, etc. is established in their own companion proofs and is NOT re-derived here. (iii) Every security statement is conditioned on stated cryptographic assumptions and an explicit, FINITE security floor. Nothing in this document claims unconditional or perpetual security. WHAT THIS DOCUMENT PROVES: T-BIND-1 Tamper-evidence: altering any bound artifact is detected by the manifest Merkle root with overwhelming probability (reduces to SHA-256 collision resistance + Ed25519 EUF-CMA). T-TRACE-1 Traceability: every theorem identifier carried by a manifest resolves to a catalogue document in the registry. This is a DOCUMENTATION binding, not a re-proof. T-PQ-MIG-1 Migration safety: the Layer-1 HMAC hot path is invariant under replacement of the Layer-2/3 anchor signature scheme (e.g., Ed25519 -> ML-DSA-65), so a post-quantum migration is a local change with no effect on per-snapshot authentication. WHAT THIS DOCUMENT DOES NOT PROVE (stated up front, by the Ten Commandments discipline of docs/MVPS_TEN_COMMANDMENTS.txt): (a) It does NOT prove any MVPS detection theorem cryptographically. Hashes and signatures bind bytes, not theorems. (b) It does NOT claim "unbreakable forever". The phrase used in the v4.0 proof is the precise import-chase sense (every reduction closes); the Proof Envelope's guarantee is conditional on the collision resistance of SHA-256 and the EUF-CMA security of the anchor signature, with a documented finite security floor. (c) It does NOT claim post-quantum security for the Ed25519 anchor layer. The PQ-Protection profile (Section 5) is OPTIONAL and is the mechanism by which the finite floor is RAISED, not removed. ============================================================================== 0.1 ELEMENTARY FACTS ============================================================================== F-PE1. SHA-256 is modeled as a collision-resistant, preimage-resistant hash H: {0,1}* -> {0,1}^256. No PPT adversary finds x != y with H(x) = H(y) except with negligible probability. F-PE2. Under Grover's algorithm a quantum adversary reduces the preimage search of an n-bit hash from 2^n to 2^(n/2). For SHA-256 the effective preimage floor is 2^128; the collision floor under Brassard-Hoyer-Tapp is ~2^85, still classically infeasible. These are FINITE, documented margins. F-PE3. HMAC-SHA256 unforgeability reduces to the PRF assumption (Bellare-Canetti-Krawczyk 1996; RFC 2104), inherited verbatim from CWT fact F-C1. F-PE4. Ed25519 is EUF-CMA secure (RFC 8032). ML-DSA-65 (FIPS 204, the standardized CRYSTALS-Dilithium level 3) is EUF-CMA secure under Module-LWE / Module-SIS, and is believed secure against quantum adversaries. F-PE5. A Merkle tree over leaf digests with RFC 9162 domain separators (0x00 leaf, 0x01 node) is binding: the root commits to the ordered multiset of leaves; finding two distinct leaf sets with the same root reduces to a SHA-256 collision (F-PE1). F-PE6. JCS (RFC 8785) canonicalization yields a unique byte string for a given JSON value; therefore H(JCS(v)) is well-defined and order-independent over object keys. ============================================================================== 0.2 IMPORTED THEOREMS (used in published form, with citations) ============================================================================== I-PE1. (Merkle 1989; RFC 9162 Section 2.) Tree-head binding: the root hash is a binding commitment to the leaf sequence under collision resistance of the node hash. I-PE2. (Bellare-Canetti-Krawczyk 1996; RFC 2104.) HMAC PRF / unforgeability. Same as CWT I-C1. I-PE3. (Ed25519 EUF-CMA; RFC 8032.) Same as CWT I-C3. I-PE4. (FIPS 204, 2024.) ML-DSA (Dilithium) EUF-CMA under Module-LWE / Module-SIS, with NIST category-3 parameters for ML-DSA-65. I-PE5. (RFC 8785.) JSON Canonicalization Scheme determinism. I-PE6. (v4.0 catalogue; CWT catalogue; PerfSec catalogue.) Imported as already-proved in their companion documents; NOT re-derived. ============================================================================== 1. DEFINITIONS (Proof Envelope mathematical object) ============================================================================== D-PE1. (Artifact.) a = (kind, name, h) where kind in {proof, validator, receipt}, name is the repository-relative path, and h = H(file_bytes) is the SHA-256 digest of the file. D-PE2. (Proof Manifest.) M = (manifest_version, catalog, theorem_ids, A, issued_at), where catalog is the ordered list of catalogue versions (e.g., mvps-v4.0, cwt-v1, perfsec-v1, proof-envelope-v1), theorem_ids is a set of theorem identifiers, and A = (a_1, ..., a_k) is the name-sorted artifact list (D-PE1). D-PE3. (Manifest leaves.) leaf_i = H(0x00 || JCS({name: a_i.name, sha256: a_i.h})). The canonical artifact order is ascending by a_i.name (a normative MUST; see T-BIND-2). D-PE4. (Manifest root.) root(M) = MerkleTreeRoot(leaf_1, ..., leaf_k) with RFC 9162 node separators. D-PE5. (Envelope.) E = (M, root(M), sigma), where sigma is an anchor signature over root(M) by the Operator Epoch key (Ed25519 in the base profile; ML-DSA-65 in the PQ profile) and, when CWT Layer 3 is present, witness cosignatures on the bundle checkpoint that carries root(M) in its `extra` field. D-PE6. (Theorem registry R.) A partial map theorem_id -> document. R is realized in the repository by docs/MVPS_IETF_FOUNDATIONS.txt and, for the validator harness, by THEOREM_REGISTRY in scripts/validate_proof_envelope.py. D-PE7. (Verify-Envelope.) Envelope E is accepted iff: (a) artifacts are in canonical (name-sorted) order, (b) for every listed a_i still present to the verifier, H(file_bytes_i) == a_i.h, (c) root(M) recomputed from A equals the carried root, (d) sigma verifies over root(M) under the anchor public key, (e) every t in theorem_ids has R(t) defined, (f) when CWT Layer 3 is required, the checkpoint carrying root(M) is q-witnessed (CWT D-C5(g)). D-PE8. (Tamper.) An adversary tampers iff it presents an envelope E' accepted by Verify-Envelope in which at least one bound artifact differs in content from the artifact the manifest author hashed. ============================================================================== 2. THEOREM -- TAMPER-EVIDENT BINDING ============================================================================== THEOREM T-BIND-1 (Tamper-evidence of the Proof Envelope). Assume I-PE1 (Merkle binding), I-PE3 / I-PE4 (anchor EUF-CMA), and F-PE1 (SHA-256 collision resistance). If an adversary presents an envelope E' that passes Verify-Envelope but in which some bound artifact a_j has content differing from the author's original, then one of the following held with non-negligible probability, a contradiction: (1) the adversary found a SHA-256 collision a_j.h = H(forged_j) with forged_j != original_j, OR (2) the adversary forged the anchor signature sigma over a root it did not legitimately commit to. Hence, under the stated assumptions, any content alteration of a bound artifact is detected, except with negligible probability. PROOF. Suppose E' is accepted (D-PE7) yet artifact a_j carries forged content C' != C (the author's content). By D-PE7(b) the verifier recomputes H(C') and compares to a_j.h. Acceptance requires H(C') == a_j.h. Two cases: Case A: a_j.h == H(C). Then H(C') == H(C) with C' != C, a SHA-256 collision, contradicting F-PE1. Case B: a_j.h == H(C') != H(C), i.e. the adversary rewrote the manifest digest field. Then the manifest M' differs from M in leaf_j (D-PE3), so by I-PE1 root(M') != root(M) except with negligible collision probability. Verify-Envelope(d) requires sigma to verify over root(M'). The author signed root(M), not root(M'); producing a valid sigma over root(M') without the anchor secret key contradicts EUF-CMA (I-PE3 / I-PE4). Both cases contradict an assumption. Therefore acceptance of a content-altered artifact has negligible probability. QED. COROLLARY T-BIND-1.1 (Set binding). Adding or removing an artifact changes the leaf multiset, hence root(M) (I-PE1); the same EUF-CMA argument of Case B applies. The envelope binds not only each artifact's content but the exact SET of artifacts. REMARK. T-BIND-1 binds BYTES. It says nothing about whether the bound proof is mathematically correct -- that is the job of the companion proof of each theorem and of the validators. The Proof Envelope guarantees only that the proof you verify is the proof the author published, unchanged. THEOREM T-BIND-2 (Canonical order necessity). The Merkle root of D-PE4 is position-sensitive: permuting the artifact list generally changes root(M). Therefore a canonical order is REQUIRED for deterministic verification. Under the name-sorted order of D-PE3, any two verifiers computing root(M) from the same artifact SET obtain the same root. PROOF. Position sensitivity is immediate from the tree construction (interior nodes hash ordered child pairs). Determinism under name sorting: names are unique repository paths, so the sort is a total order; both verifiers enumerate identical leaves in identical order and obtain identical roots. QED. THEOREM T-BIND-3 (Inclusion soundness). For an artifact a_i in M, the standard RFC 9162 inclusion proof for leaf_i verifies against root(M); for any forged leaf' != leaf_i the recomputed root differs from root(M) except with negligible collision probability. PROOF. Inclusion verification recomputes the root along the audit path; correctness is the RFC 9162 inclusion property (I-PE1). Soundness against a forged leaf reduces to collision resistance (F-PE1) at the first differing node. QED. ============================================================================== 3. THEOREM -- TRACEABILITY ============================================================================== THEOREM T-TRACE-1 (Theorem-identifier traceability). Let M carry theorem_ids = {t_1, ..., t_n}. Verify-Envelope(e) requires R(t_j) defined for all j. Then every claim transported by the envelope is anchored to a named catalogue document; there is no accepted envelope that asserts an orphan theorem. PROOF. Constructive / definitional. D-PE7(e) rejects any envelope with a t_j for which R(t_j) is undefined. Hence acceptance implies totality of R on theorem_ids. By D-PE6, R(t_j) names a document; by T-BIND-1 the digest of that document is itself bound in A whenever the document is listed as an artifact, closing the loop between "claim", "naming", and "bytes". QED. COROLLARY T-TRACE-1.1 (No silent theorem). An envelope cannot smuggle an unrecognized theorem identifier: an unknown id is rejected (validator check T-TRACE-2, negative control). REMARK. Traceability is DOCUMENTATION binding. It guarantees that a reader can find, for every transported claim, the document that proves it; it does not itself prove the claim. THEOREM T-TRACE-2 (No dangling target). Every registry target document for a Proof-Envelope-native or present-companion theorem exists on disk (validator check T-TRACE-3). Hence traceability is not vacuous: each resolved name points to a real artifact whose bytes are hashable and bindable. PROOF. Constructive: enumerated by the validator over the registry. QED. ============================================================================== 4. THEOREM -- COMPOSITION WITH CWT / v4.0 ============================================================================== THEOREM T-COMP-PE (Envelope composes with the trust chain). When the manifest root is carried in the `extra` field of a CWT bundle checkpoint (D-PE5) and the checkpoint is q-witnessed, the Proof Envelope inherits CWT T-SPLIT-1 (no split-view of the manifest) and T-COAL-1 (coalition cannot substitute a manifest without corrupting a witness quorum). Under H-TRUST-CWT + H-ADM + H-WIT + f < N/2, the v4.0 catalogue applies to the bundle whose proofs the envelope binds. PROOF. The manifest root is a bitstring placed in the checkpoint `extra`; from the witnesses' standpoint it is part of the cosigned bytes. T-SPLIT-1 then forbids two distinct accepted roots for the same (bundle_id, bundle_seq); T-COAL-1 bounds coalition substitution by (b/w)^q. Inheritance of v4.0 is CWT T-COMP-2-CWT, unchanged. QED. ============================================================================== 5. THEOREM -- POST-QUANTUM PROTECTION PROFILE (OPTIONAL) ============================================================================== THEOREM T-PQ-MIG-1 (Hot-path invariance under anchor migration). Let the base profile use Ed25519 for sigma (D-PE5) and the PQ profile use ML-DSA-65 (I-PE4). The Layer-1 per-snapshot HMAC tag (CWT D-C1) is a function of (K_v_epoch, M) only and does not depend on the anchor signature scheme. Therefore migrating sigma from Ed25519 to ML-DSA-65 leaves every per-snapshot tag unchanged. PROOF. By CWT D-C1, tag = HMAC-SHA256(K_v_epoch, message), with message independent of sigma. The anchor signature sigma is computed over root(M) at Layer 2/3 and is consumed only in Verify-Envelope(d). Substituting the signing algorithm changes sigma and the anchor public key but not K_v_epoch nor message, hence not tag. Constructive check: validator T-PQ-MIG-1 recomputes the tag across a simulated migration and asserts bytewise equality. QED. COROLLARY T-PQ-MIG-1.1 (Localized migration cost). A campaign migrates to post-quantum protection by reissuing only Operator Epoch and witness keys under ML-DSA-65; vantages, session keys, and the per-snapshot wire format are untouched. THEOREM T-PQ-MIG-2 (Finite, documented security floor). Under F-PE2, the SHA-256 / HMAC-SHA256 primitives retain a quantum preimage floor of 2^128 (Grover) and a collision floor of ~2^85 (BHT). These are FINITE and documented; the envelope's guarantee is conditional on them. PROOF. Direct from F-PE2. The claim is explicitly NOT "unbreakable"; it is "no known classical or quantum attack reduces the floor below the stated bound." QED. REMARK (the seal, stated honestly). The mathematical truth of the MVPS theorems is established by proof and is not subject to cryptanalysis at all -- a proved theorem is not "broken" by any machine, classical or quantum. What cryptanalysis could target is the BINDING (can someone swap the artifacts undetected?). T-PQ-MIG-1/2 ensure that even that binding survives the migration to post-quantum signatures, with a finite, named security floor. This is the strongest HONEST statement available, and it is the one the IETF will accept. ============================================================================== 6. DESIGNS (declared, not theorems) ============================================================================== D-PE-ORDER. Canonical artifact order = ascending by repository-relative name (UTF-8 byte order). Normative MUST (T-BIND-2). D-PE-ANCHOR. Anchor signature scheme is profile-selected: base = Ed25519; pq = ML-DSA-65 (FIPS 204). Layer 1 unchanged. D-PE-REGEN. The receipt evidence/proof_envelope_receipt.json is regenerated deterministically by scripts/validate_proof_envelope.py over the artifacts present at run time; its body digest is recorded in the receipt itself (T-RECEIPT-1). D-PE-CARRY. When deployed with CWT, root(M) is carried in the bundle checkpoint `extra` field; standalone deployments MAY publish the signed envelope out of band. ============================================================================== 7. CONJECTURES (none of mathematical type) ============================================================================== The Proof Envelope introduces no empirical conjecture. All claims reduce to imported cryptographic results (Section 0.2) or to definitional chases. The PQ-Protection profile inherits the standard (community-held, not herein proved) belief that ML-DSA-65 resists quantum cryptanalysis; this is labelled an IMPORTED ASSUMPTION (I-PE4), not a Catellix conjecture. ============================================================================== 8. NUMERICAL RECEIPT ============================================================================== Constructive witnesses for T-CANON-1, T-BIND-1, T-BIND-2, T-BIND-3, T-SIG-1, T-TRACE-1, T-TRACE-2, T-TRACE-3, T-PQ-MIG-1, T-PQ-MIG-2, and T-RECEIPT-1 are produced by scripts/validate_proof_envelope.py and recorded in evidence/proof_envelope_receipt.json. The receipt records: - the manifest Merkle root over all bound artifacts present at run, - the platform metadata for independent reproduction, - the explicit non-claims (Section 0), - the body SHA-256 of the receipt itself. Implementations SHOULD run this validator in CI alongside scripts/validate_v4_against_all_attacks.py and scripts/validate_cwt_theorems.py. ============================================================================== 9. CLOSING STATEMENT ============================================================================== What the Proof Envelope proves: (i) T-BIND-1: you cannot alter a bound proof, validator, or receipt without detection, under SHA-256 collision resistance and anchor EUF-CMA. (ii) T-TRACE-1: every transported theorem identifier resolves to a named, on-disk catalogue document. (iii) T-PQ-MIG-1: the binding survives migration to post-quantum signatures with the per-snapshot hot path untouched. What the Proof Envelope does NOT claim: (a) It does not cryptographically prove any MVPS theorem. (b) It does not claim perpetual or unconditional security. (c) It does not make Ed25519 quantum-safe; the PQ profile raises the floor by substituting ML-DSA-65 at the anchor layers. The honest seal: the MATHEMATICS is proved, and a proof is not something a quantum computer can "break." The Proof Envelope guarantees that the proof on the wire is the proof that was published -- bound, traceable, and migratable to post-quantum anchors. That is a claim the IETF can verify line by line, and it is the claim this document makes. ============================================================================== 10. REFERENCES ============================================================================== [I-D.melegassi-ippm-mvps-proof-envelope] Melegassi, L., "MVPS Proof Envelope: Tamper-Evident Binding of Theorem Catalogues, Validators, and Numerical Receipts, with an Optional Post-Quantum Protection Profile", draft-melegassi-ippm-mvps-proof-envelope-00, May 2026. [I-D.melegassi-santos-ippm-mvps-cwt] Melegassi, L., Santos, J. A., "MVPS Coherent-Witness Trust", draft-melegassi-santos-ippm-mvps-cwt-00, May 2026. [MVPS-V4] Melegassi, L., "MVPS Mathematical Existence Proof v4.0", May 2026. [RFC2104] Krawczyk, H., Bellare, M., Canetti, R., "HMAC", Feb 1997. [RFC5869] Krawczyk, H., Eronen, P., "HKDF", May 2010. [RFC8032] Josefsson, S., Liusvaara, I., "EdDSA (Ed25519)", Jan 2017. [RFC8785] Rundgren, A., Jordan, B., Erdtman, S., "JSON Canonicalization Scheme (JCS)", June 2020. [RFC9162] Laurie, B., Messeri, E., Stradling, R., "Certificate Transparency Version 2.0", Dec 2021. [FIPS204] NIST, "Module-Lattice-Based Digital Signature Standard (ML-DSA)", FIPS 204, August 2024. [BHT1998] Brassard, G., Hoyer, P., Tapp, A., "Quantum Cryptanalysis of Hash and Claw-Free Functions", LATIN 1998. [Grover1996] Grover, L., "A fast quantum mechanical algorithm for database search", STOC 1996. [BellareCanettiKrawczyk1996] Bellare, M., Canetti, R., Krawczyk, H., "Keying Hash Functions for Message Authentication", CRYPTO 1996. ============================================================================== END OF MVPS PROOF ENVELOPE MATHEMATICAL PROOF ==============================================================================