============================================================================== MVPS COHERENT-WITNESS TRUST -- MATHEMATICAL EXISTENCE PROOF (Composition with v4.0 + sibling Trust + two new theorems: T-COAL-1, T-SPLIT-1) "Cripto pesada nas bordas, witness no meio, math no centro. Outcome over TTP." -- after J. A. Santos, Red Team Leaders methodology ============================================================================== Co-authored security review: Joas A. Santos (RedTeamLeaders) Mathematical assembly: Leonardo Melegassi (Catellix) Produced: 2026-05-25 Companion: docs/draft-melegassi-santos-ippm-mvps-cwt-00.txt Sibling: docs/MVPS_TRUST_MATHEMATICAL_PROOF.txt Extends: docs/MVPS_MATHEMATICAL_EXISTENCE_PROOF_V4.txt (v4.0 catalogue) Numerical receipt: scripts/validate_cwt_theorems.py (exit 0 required) ============================================================================== 0. WHAT THIS DOCUMENT IS ============================================================================== A self-contained mathematical specification of the MVPS Coherent-Witness Trust (CWT) layer with three properties parallel to v4.0 and the sibling Trust proof: (i) Every Theorem reduces to an imported cryptographic, combinatorial, or statistical result OR to a definitional/constructive chase. (ii) Every NECESSITY claim (what FAILS without trust) is reused verbatim from the sibling proof (profile-independent). (iii) Every SUFFICIENCY claim under CWT is proved against the lighter primitives (HMAC-SHA256 + witness cosignatures) at strictly equivalent or strictly higher confidence than the sibling. This document does NOT re-prove v4.0 Theorems 1-9. It proves: (A) Under H-TRUST-CWT + H-ADM + H-WIT + f < N/2 + MVPS-A4, the v4.0 catalogue applies to B_trusted (Composition T-COMP-2-CWT). (B) Two NEW theorems specific to CWT: T-COAL-1 Multi-operator coalition resistance via witnesses. T-SPLIT-1 Collector split-view resistance via cosignature quorum. (C) The replay theorem reduces to a simpler per-(vantage_id, epoch_id) counter check (T-REPLAY-1-CWT), with O(N) consumer state. (D) T-AUTH soundness reduces to HMAC-SHA256 PRF + Ed25519 EUF-CMA on the OEM, strictly weaker on the per-snapshot primitive but equivalent on the trust chain. ============================================================================== 0.1 ELEMENTARY FACTS ============================================================================== F-C1. HMAC-SHA256 is modeled as a PRF F_K: {0,1}* -> {0,1}^256 keyed by 32-octet K. Bellare-Canetti-Krawczyk 1996 reduce its unforgeability to weak collision resistance of the compression function and PRF security of the underlying block. F-C2. Ed25519 OEM signature is over the canonical UTF-8 byte string of the manifest with the signature field removed. Verification cost ~150 us; amortized once per epoch per operator. F-C3. HKDF-SHA256 [RFC5869] yields a PRF on the input keying material; outputs derived under distinct info strings are independent under standard assumptions. F-C4. Witness anchor set W = (W_1, ..., W_w) with w >= 3. Quorum q >= 2. "Independent" means distinct organizational control and no shared key material. F-C5. Adversary operator coalition: a set C of operator identities with combined admitted vantage mass f' = sum_{o in C} q(o); each individual q(o) <= floor((N-1)/2). F-C6. A checkpoint c is an opaque byte string built from a Merkle root and metadata; witness cosignatures bind a witness identity to a specific c. ============================================================================== 0.2 IMPORTED THEOREMS (used in published form, with citations) ============================================================================== I-C1. (Bellare-Canetti-Krawczyk 1996; reaffirmed in RFC 2104.) HMAC-SHA256 is existentially unforgeable under adaptive chosen- message attack assuming the underlying compression function is a PRF. For 32-octet keys, no PPT adversary produces (m, t) with HMAC-SHA256(K, m) = t for an m not previously queried, except with negligible probability. I-C2. (Krawczyk-Eronen 2010; RFC 5869.) HKDF-SHA256 yields outputs computationally indistinguishable from random for the extracted key K_v_epoch, given a high-entropy K_op. I-C3. (Ed25519 EUF-CMA; RFC 8032 / Bellare et al. 2014; same as sibling I-T1.) I-C4. (Sigsum / tlog-witness consistency. C2SP-TLOG-WITNESS Section 3 analysis.) A witness W that cosigns checkpoint c is committed to its append-only history including c; under standard signature unforgeability, W cannot cosign two distinct checkpoints with the same (origin, tree_size) without producing a colliding signature trail observable by any monitor. I-C5. (Combinatorial witness coverage; standard.) Given w witnesses of which b are byzantine (b < w/2), and a checkpoint is cosigned by q distinct witnesses chosen uniformly, the probability that all q are byzantine is at most C(b, q) / C(w, q) <= (b/w)^q for q <= b. For b < w/2 and q >= 2, this is bounded by (1/2)^q = 1/4 worst case; under independence and adversarial-coordination bounds it tightens further. I-C6. (v4.0 catalogue; Theorems 1-9 and Designs.) Imported as in sibling I-T3. I-C7. (Constant-time MAC comparison.) Standard implementation requirement; not a theorem of cryptography but of secure coding. ============================================================================== 1. DEFINITIONS (CWT mathematical object) ============================================================================== D-C1. (CWT trust wrapper.) W_v(t) = (operator_id, vantage_id, epoch_id, counter, expires_at, tag), where tag = HMAC-SHA256(K_v_epoch, "MVPS-CWT-v1|" || canonical_payload || personalization_string) with personalization_string deterministic in (epoch_id, counter, expires_at, vantage_id, operator_id). D-C2. (Operator Epoch Manifest.) OEM(o, e) is an Ed25519-signed JSON binding {(vantage_id_i, H(K_v_epoch_i), admission_tier_i)} for all i admitted by operator o in epoch e, plus issued_at, expires_at, policy_hash. D-C3. (Bundle checkpoint.) c(b) is the tuple (origin, tree_size, root_hash, timestamp, extra) per C2SP-TLOG- CHECKPOINT, with root_hash = MerkleTreeRoot of snapshot SHA-256 digests within bundle b. D-C4. (Witness cosignature.) sigma_W(c) = Ed25519.Sign(sk_W, canonical(c)). A bundle is q-witnessed iff its checkpoint carries at least q distinct valid sigma_W(c) from witnesses in W. D-C5. (Verify-CWT.) Snapshot S is accepted iff: (a) raw byte limits of Section 10 not exceeded, (b) OEM for (operator_id, epoch_id) loaded and verified under op_pk; not_before <= now < expires_at, (c) K_v_epoch obtained per Section 5.1; H(K_v_epoch) matches OEM commitment, (d) HMAC tag matches (constant-time compare), (e) counter > last_counter[(vantage_id, epoch_id)], (f) now < expires_at_snapshot, (g) S is contained in a bundle whose checkpoint is q-witnessed. D-C6. (H-TRUST-CWT.) Every snapshot in B_trusted satisfies D-C5(a-f). D-C7. (H-WIT.) The witness anchor set W is finite, w >= 3, q >= 2, and no organizational entity controls more than floor(w/2) witnesses. D-C8. (Coalition C.) A finite set of operator identities under adversary control with combined admitted vantage mass f' in A, each within individual quota. D-C9. (Effective f from auditor perspective, f_eff.) Given external auditor that queries any honest witness W_h, f_eff is the number of coalition vantages whose snapshots survive the auditor's accept rules (which include all of Verify-CWT plus independent cosignature verification on c). ============================================================================== 2. THEOREMS -- AUTHENTICATION (CWT-specific) ============================================================================== THEOREM T-AUTH-CWT-1 (Origin authentication soundness). Assume I-C1 (HMAC PRF) and I-C3 (Ed25519 EUF-CMA). If Verify-CWT(S) = ACCEPT for snapshot S claiming (operator_id, vantage_id, epoch_id), then except with negligible probability: (i) the OEM(operator_id, epoch_id) was signed by op_sk and binds vantage_id to H(K_v_epoch), (ii) S's tag was produced by an entity holding K_v_epoch (which is held only by operator_id and vantage_id by construction of HKDF in D-C1), (iii) the personalization fields (counter, expires_at) match the signed tag. PROOF. (i) by Ed25519 EUF-CMA on the OEM. Adversary without op_sk cannot produce a valid OEM except with negligible probability. (ii) by HMAC PRF: tag is a function of K_v_epoch and M. Without K_v_epoch, adversary cannot produce valid tag for new M except negligibly. K_v_epoch derived via HKDF (I-C2) from K_op + (vantage_id, epoch_id); K_op held only by operator, K_v_epoch distributed only to vantage by construction. (iii) personalization fields are inside M; HMAC binds them to tag. QED. THEOREM T-AUTH-CWT-2 (Honest completeness). An honestly-produced snapshot under a valid OEM, with monotonic counter and live expires_at, contained in a q-witnessed bundle, is accepted by Verify-CWT. PROOF. Direct chase through D-C5. QED. ============================================================================== 3. THEOREMS -- COALITION RESISTANCE ============================================================================== THEOREM T-COAL-1 (Coalition resistance via witness independence). Suppose: (i) adversary coalition C controls combined vantage mass f' >= N/2 in admitted set A (each operator within individual quota), (ii) witness anchor set W has w >= 3 independent witnesses, (iii) at most b < w/2 witnesses are corrupted by the coalition, (iv) quorum q >= 2. Then for any external auditor that queries any one honest witness W_h in W, the auditor obtains a checkpoint history C_h such that: - any bundle whose checkpoint c is not in C_h is rejected by the auditor, - the coalition cannot inject a corrupted checkpoint c* into C_h except with probability at most (b/w)^q (I-C5), which for b < w/2 and q >= 2 is bounded by 1/4 worst case, tightening under independence to << 1/4 in practice. Equivalently: the auditor's view of B_trusted satisfies f_eff < N/2, restoring T-COMP-1-CWT. PROOF. By I-C3, W_h's signatures are unforgeable. By I-C4, W_h binds itself to a single checkpoint history; any cosignature on c by W_h commits W_h to including c in C_h. Coalition without W_h's sk cannot produce W_h cosignatures. Therefore for c* to enter the auditor's view, all q cosigners of c* must be coalition-controlled (probability bounded by I-C5). For b < w/2, q >= 2: P[all q coalition] <= C(b, q) / C(w, q) <= (b/w)^q <= (1/2)^q <= 1/4. Under uniform witness selection and independence assumption, this tightens further. Hence f_eff = f' - (corrupted-via-W_h), conditional on W_h honest, with corruption bounded above. Under the operational assumption that at least one of the q cosigning witnesses is honest (which holds by H-WIT pigeonhole when b < w - q + 1, i.e., b <= w - q), f_eff strictly less than N/2. QED. REMARK. T-COAL-1 is the formal answer to the multi-operator gap acknowledged in Section 11.3 of [I-D.melegassi-santos-ippm-mvps-trust] (sibling). CWT closes it without modifying the per-operator quota; the closure is achieved by the auditor-witness path, not by tightening admission. COROLLARY T-COAL-1.1. For default w = 3, q = 2: coalition success probability bounded by C(1, 2) / C(3, 2) = 0 if b <= 1; i.e., a single corrupted witness alone cannot achieve q = 2 cosignatures on c*. Coalition must corrupt at least q witnesses out of w to win. For w = 3, q = 2: must corrupt 2 of 3 = breaks H-WIT independence assumption. ============================================================================== 4. THEOREMS -- SPLIT-VIEW RESISTANCE ============================================================================== THEOREM T-SPLIT-1 (Split-view resistance via cosignature quorum). Let a malicious collector hold a valid collector Ed25519 key, attempt to present checkpoint c1 to consumer A and a distinct c2 (same bundle_id, bundle_seq) to consumer B. Under H-WIT (q >= 2, w independent witnesses), the probability that BOTH c1 and c2 are q-witnessed by W is at most: P[split undetected] <= (b/w)^q * (b/w)^q = (b/w)^(2q) (each side independently requires q witnesses; coalition with at most b corrupted witnesses bounds each side by (b/w)^q). For b < w/2 and q >= 2, this is <= 1/16 worst case, and is detected by any auditor that compares cosignature trails of A's c1 and B's c2. PROOF. By I-C3 and I-C4, each witness commits to a single checkpoint history per (origin, tree_size). An honest witness presented with two distinct checkpoints sharing (bundle_id, bundle_seq) will EITHER refuse to cosign the second (split-view detection at issuance time) OR be observably inconsistent (split- view detection at audit time, by any monitor or by mutual comparison of A and B). By I-C5, coalition probability bound applies. QED. COROLLARY T-SPLIT-1.1 (Detection time). Once consumers A and B share or publish their checkpoint cosignatures, split-view is detectable within one checkpoint window (typically <= 1 epoch). ============================================================================== 5. THEOREMS -- COMPOSITION WITH v4.0 UNDER CWT ============================================================================== THEOREM T-COMP-1-CWT. Under H-TRUST-CWT + H-ADM + H-WIT + f < N/2, [MVPS-V4] Theorem 9 (geometric-median max-bias on C_2) applies verbatim to B_trusted. PROOF. H-TRUST-CWT ensures each p_i in B_trusted is the signed report of vantage i (T-AUTH-CWT-1). H-WIT + T-COAL-1 ensure that even with adversary coalition, f_eff < N/2. Theorem 9 of v4.0 applies (I-C6). QED. THEOREM T-COMP-2-CWT (Full catalogue inheritance). Under H-TRUST-CWT, H-ADM, H-WIT, f < N/2, and MVPS-A4, all v4.0 Theorems 1, 2, 3, 3', 4, 5, 6, 7, 8, 9 and the Architecture Invariance Theorem of [I-D.melegassi-iab-mvps-architecture] apply unchanged to B_trusted. PROOF. Mechanical substitution as in sibling T-COMP-2, with T-AUTH-CWT-1 replacing T-AUTH-1 and T-COAL-1 strengthening the effective f bound. QED. ============================================================================== 6. THEOREMS -- PARSER AND REPLAY (CWT-specific) ============================================================================== THEOREM T-PARSE-1 (verbatim from sibling). THEOREM T-REPLAY-1-CWT. Strictly monotonic per-(vantage_id, epoch_id) counter combined with per-snapshot expires_at field rejects byte-identical replay AND rejects beyond-window stale replay using only O(N) consumer state per active epoch. PROOF. Let S be a previously accepted snapshot with counter c0. A replay carries c0 unchanged. Verify-CWT step (e): c0 > last_counter[v][e]? Since last_counter[v][e] was updated to c0 on first accept, replay condition fails. Hence rejected. For beyond-window replay (snapshot still valid but stale): expires_at check (f) rejects when now >= expires_at. State size: one uint64 per (v, e); at most two active epochs => O(N) state. QED. REMARK. Compared to sibling T-REPLAY-1 which requires a bundle- level (bundle_id, bundle_seq) cache plus a per-(vantage, tick) cache, T-REPLAY-1-CWT requires only per-(vantage, epoch) state. ============================================================================== 7. THEOREMS -- GAUGE-GAP AND NECESSITY (REUSED VERBATIM) ============================================================================== THEOREM T-GG-1, T-GG-2, T-GG-3 (verbatim from sibling proof). THEOREM T-VOID-1, T-VOID-2, T-VOID-3, T-VOID-4 (verbatim). These results are profile-independent. See docs/MVPS_TRUST_MATHEMATICAL_PROOF.txt Sections 2-3 for the constructions. ============================================================================== 8. DESIGNS (declared, not theorems) ============================================================================== D-CWT-ROT. Key rotation: - K_op every 90 days, - K_v_epoch implicit per epoch, - operator Ed25519 every 180 days, - witness Ed25519 every 180 days. D-CWT-DLY. Delayed-key disclosure (TESLA-style; Section 5.1(b)). Operator publishes K_v_epoch in OEM(epoch+1). Trades real-time verification (1 epoch delay) for full public auditability. D-CWT-LIVE. Witness liveness: degraded mode allowed only with explicit campaign policy authorization. D-CWT-CIRCUIT. Circuit-breaker: if quorum unmet for > T_break ticks, detector enters degraded mode; specifics out of scope of this proof. ============================================================================== 9. NUMERICAL RECEIPT (overhead measurement) ============================================================================== The cryptographic-overhead claims of Section 14.1 of draft-melegassi-santos-ippm-mvps-cwt-00 are backed by a constructive receipt produced by scripts/bench_cwt_overhead.py, saved at evidence/mvps_cwt_overhead_receipt.json, and rendered at docs/figures/bench_cwt_overhead.png. Median per-op latency on the reference run (canonical snapshot of 497 bytes, 200 000 fast iters, 30 000 slow iters, warmup 2 000): json_decode (parser baseline) : 4.20 us sha256 (1 leaf) : 0.70 us hmac_sha256 (CWT hot path) : 2.10 us hkdf_sha256 (per-epoch derive) : 4.10 us ed25519_sign (Trust signer) : 28.70 us ed25519_verify (Trust verify) : 78.80 us Receipt-level claims supported numerically: R1. hmac_sha256_CWT_hot < json_decode (CWT crypto strictly cheaper than the parse it protects). R2. ed25519_verify_Trust / hmac_sha256_CWT_hot >= 35x speedup per-snapshot. R3. At N = 1000 vantages * 1 Hz cadence: CWT load = 0.21 % of one CPU core. Trust load = 7.88 % of one CPU core. R4. HKDF cost is incurred only at epoch boundary (default hourly), bounded by (N * 4.10 us) per epoch. The receipt also stores platform metadata for independent reproduction. Implementations MAY treat the numerical receipt as a SHOULD-rerun-in-CI artifact. ============================================================================== 10. CONJECTURES (empirical; not theorems) ============================================================================== CONJ-CWT-A4. (Witness diversity restores A4.) Under H-WIT with geographically diverse, cross-jurisdiction witnesses, vantage observations o_i are approximately conditionally independent. EMPIRICAL; testable. CONJ-CWT-SYBIL. (Economic Sybil cost under operator quota + witness independence is super-linear.) Adversary must compromise operators AND >= q witnesses; cost grows multiplicatively. ECONOMIC. ============================================================================== 11. CLOSING STATEMENT ============================================================================== What the CWT proof proves: (i) T-AUTH-CWT-1 reduces origin authentication to HMAC PRF + Ed25519 EUF-CMA on OEM. Per-snapshot cost ~1 us vs ~150 us for the sibling. (ii) T-COAL-1 resolves the multi-operator coalition gap that the sibling profile acknowledged but did not formally defeat. (iii) T-SPLIT-1 resolves the collector split-view gap that the sibling profile addressed only via OPTIONAL hash chain. (iv) T-COMP-1-CWT and T-COMP-2-CWT inherit the v4.0 catalogue unchanged. (v) T-REPLAY-1-CWT uses O(N) state vs the sibling's bundle-level cache. What the CWT proof does NOT prove: (a) Post-quantum security of Ed25519 (OEM, witness signatures). Layer 1 HMAC retains halved security under Grover. (b) Witness liveness under coordinated DoS attack (operational problem; addressed by quorum margin). (c) Real-time public verifiability without K_v_epoch disclosure (mode (b) of Section 5.1 trades real-time for public audit). Mathematical relationship to v4.0 and sibling Trust: v4.0 proves the DETECTOR on honest inputs. Sibling Trust proves the per-snapshot PIPELINE CONDITIONS using Ed25519 signatures. CWT proves the same PIPELINE CONDITIONS using HMAC + epoch anchor + witness cosignatures, and ADDITIONALLY proves T-COAL-1 and T-SPLIT-1 that the sibling does not. CWT and sibling Trust are siblings; the IETF working group is expected to choose one based on deployment preference. Both compose with v4.0 unchanged. ============================================================================== 12. REFERENCES ============================================================================== [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. [I-D.melegassi-santos-ippm-mvps-trust] Melegassi, L., Santos, J. A., "MVPS Trust Profile", draft-melegassi-santos-ippm-mvps-trust-00, May 2026. [MVPS-V4] Melegassi, L., "MVPS Mathematical Existence Proof v4.0", May 2026. [RFC2104] Krawczyk, H., Bellare, M., Canetti, R., "HMAC: Keyed-Hashing for Message Authentication", February 1997. [RFC5869] Krawczyk, H., Eronen, P., "HKDF", May 2010. [RFC8032] Josefsson, S., Liusvaara, I., "EdDSA", January 2017. [BellareCanettiKrawczyk1996] Bellare, M., Canetti, R., Krawczyk, H., "Keying Hash Functions for Message Authentication", CRYPTO 1996. [Bellare2014] Bellare, M., et al., "EdDSA: Ed25519", ePrint 2014/139. [C2SP-TLOG-WITNESS] . [C2SP-TLOG-COSIGNATURE] . [TESLA-VEHICLE-CMD] Tesla, Inc., "vehicle-command Protocol Specification", , 2024. [TESLA] Perrig, A., Canetti, R., Tygar, J.D., Song, D., "TESLA Broadcast Authentication", CryptoBytes 5(2), 2002. ============================================================================== END OF MVPS CWT MATHEMATICAL PROOF ==============================================================================