============================================================================== MVPS PERFORMANCE-SECURITY COUPLING -- MATHEMATICAL EXISTENCE PROOF Companion proof document for draft-melegassi-mvps-perfsec-coupling-00 Issued: 2026-05-27 Author: Leonardo Melegassi Authority: docs/draft-melegassi-mvps-perfsec-coupling-00.txt docs/MVPS_PERFSEC_COUPLING_AUDIT.txt docs/MVPS_MATHEMATICAL_EXISTENCE_PROOF_V4.txt (v4.0 catalogue) docs/MVPS_DETECTION_LATENCY_LEMMA.txt (L_DL) Receipts: evidence/perfsec_joint_cost_receipt.json evidence/perfsec_verification_dos_receipt.json evidence/mvps_cwt_overhead_receipt.json (constants source) Validator: scripts/validate_perfsec_coupling.py (12/12 PASS) ============================================================================== 0. PURPOSE AND DISCIPLINE ============================================================================== This document supplies the full proofs of the three theorems stated in draft-melegassi-mvps-perfsec-coupling-00 (PerfSec-Coupling, D-17): T-JCOST-1 Joint Cost Bound (Section 3 of the draft) T-VDOS-1 Verification-DoS Bound (Section 4 of the draft) T-RC-1 Replay-Counter Coherence (Section 5 of the draft) It also re-states the two derived corollaries (T-NIC-SUFF, T-COMP- SPLIT) and the two inheritance results (T-AUTH-INHERIT, T-VOLINV) for completeness of the validator catalogue. DISCIPLINE. Every proof step terminates either at a v4.0 catalogue theorem (cited verbatim from MVPS_MATHEMATICAL_EXISTENCE_PROOF_V4.txt), at a CWT proof theorem (T-AUTH-CWT-1, T-COAL-1, T-SPLIT-1, T-PARSE-1 from MVPS_CWT_MATHEMATICAL_PROOF.txt), at L_DL (the unified detection- latency lemma, MVPS_DETECTION_LATENCY_LEMMA.txt), or at an external RFC of well-known cryptographic strength (RFC 2104 HMAC-SHA256, RFC 5869 HKDF, RFC 8032 Ed25519). No new mathematics is introduced; PerfSec-Coupling is a composition profile, not a new theory. ============================================================================== 1. NOTATION AND HYPOTHESES ============================================================================== 1.1. Operating-point parameters N Number of admitted vantages. T_tick (ms) Control-tick period. M Detection multiplier (Coherence-BFD). q Witness quorum (CWT, default 2). cells_k Number of coherence cells. bundle_period_ticks Number of ticks per emitted MVPS bundle. PPS_t Telemetry packets per second per path at the broker = N * (1000 / T_tick_ms). bundles_per_sec cells_k / (bundle_period_ticks * T_tick_s). 1.2. Per-operation cost constants (microseconds) Pinned by evidence/mvps_cwt_overhead_receipt.json (Intel i7 12th gen, Python 3.12.1, payload 497 B, median over 200k iterations): c_json = 4.20 us c_bfd_parse = 0.30 us (binary, ~ 1/14 of JSON-decode) c_hmac = 2.10 us c_ed25519 = 78.80 us c_xdp = 0.05 us (eBPF/XDP per-packet hash-map lookup; conservative) Define c_path = c_json + c_bfd_parse + 2 * c_hmac. Substituting the constants: c_path = 4.20 + 0.30 + 2 * 2.10 = 8.70 us. 1.3. Hypotheses inherited from composed drafts H-CWT-TRUST H-TRUST-CWT, H-ADM, H-WIT of CWT Section 3. H-BFD-AUTH AuthHMAC-SHA256 hypothesis of Coherence-BFD 12. H-DDOS-INV Invariants I1, I2, I3 of DDoS-Resilience 3. H-V4 v4.0 catalogue (T1..T9) under f < N/2, MVPS-A4. 1.4. Profile-specific hypotheses H-RL Per-vantage rate-limit at NIC/XDP fast-path with parameters (rate_limit_factor, burst_factor) of draft Section 4.2; rate-limit decisions complete in c_xdp before HMAC verification. H-DUAL-MODE Collector publishes (D_minimax, D_max) and binds both into the cosigned checkpoint extra field per draft Section 7. H-HKDF-PS K_BFD_auth derived per draft Section 6 under shared K_op; otherwise the legacy Coherence-BFD AuthHMAC key derivation is used. ============================================================================== 2. THEOREM T-JCOST-1 (JOINT COST BOUND) ============================================================================== STATEMENT. Under H-DDOS-INV (invariants I1, I2, I3 hold) and H-CWT-TRUST + H-BFD-AUTH + H-HKDF-PS (composed authentication paths operate independently), the broker CPU cost (microseconds of CPU per second of wall-clock) required to ingest, parse, and verify all telemetry of a deployment with parameters (N, T_tick, q, bundle_period_ticks, cells_k) is exactly: JOINT(N, T_tick, q) = PPS_t * (c_json + c_hmac) (Path A: CWT) + PPS_t * (c_bfd_parse + c_hmac) (Path B: BFD) + bundles_per_sec * q * c_ed25519 (Path C: witness) where PPS_t = N * (1000 / T_tick_ms) and bundles_per_sec = cells_k / (bundle_period_ticks * T_tick_s). The bound is independent of the attack rate R. PROOF. Step 1 (NIC ingress, by H-DDOS-INV.I1 and Theorem D3 of D-4). By I1, the broker NIC receives only telemetry packets (no user-traffic L3 path). By Theorem D3 of D-4, NIC PPS is PPS_t = N * (1000 / T_tick_ms) regardless of R. Step 2 (Path-disjointness, by protocol specification). The CWT trust profile (CWT 6.3) wraps each snapshot in a TCP- bundle envelope. The Coherence-BFD protocol (Coh-BFD 4.1) transmits BFD AuthHMAC-protected control packets over UDP. These are DISJOINT packet streams at the same vantage tick rate; each contributes PPS_t per second. Step 3 (Path A cost). Each CWT-wrapped snapshot at the broker is JSON-decoded (c_json) and HMAC-verified (c_hmac, T-AUTH-CWT-1 of CWT Appendix C.2). Per-second cost: PPS_t * (c_json + c_hmac). Step 4 (Path B cost). Each Coherence-BFD push is binary-parsed (c_bfd_parse) and HMAC-verified (c_hmac, by H-BFD-AUTH). Path B HMAC uses K_BFD_auth which is independent of K_v_epoch by H-HKDF-PS; the verifier therefore performs a distinct HMAC computation rather than a shared one. Per-second cost: PPS_t * (c_bfd_parse + c_hmac). Step 5 (Path C cost). Each emitted bundle carries q witness cosignatures (CWT 8.3) over the bundle Merkle root and the Section 7 dual-mode extra (H-DUAL-MODE). Each cosignature is verified once at the broker using c_ed25519. Bundles are emitted at bundles_per_sec rate. Per-second cost: bundles_per_sec * q * c_ed25519. Step 6 (Composition). The three paths are independent (disjoint packet streams, independent crypto keys); their costs sum without overlap. The closed form of the statement follows. QED. NUMERICAL RECEIPT (Section 3.3 of the draft). evidence/perfsec_joint_cost_receipt.json five scale points; T-JCOST-1.A/B/C in scripts/validate_perfsec_coupling.py: PASS. CONSEQUENCE (Operator dimensioning rule). For any operating point (N, T_tick, q), the broker CPU+NIC budget MUST be at least JOINT(N, T_tick, q). The receipt reports the budget at five canonical scale points; the headline apples-to-apples scaling between the CWT abstract reference (1 Hz / N=1k, 0.88 % core) and Regime C (50 ms / N=10k, 174.25 % core) is ~ 198x. ============================================================================== 3. THEOREM T-VDOS-1 (VERIFICATION-DoS BOUND) ============================================================================== STATEMENT. Under H-RL with parameters (rate_limit_factor (R_L), burst_factor) and the cost constants of Section 1.2, an insider adversary controlling K admitted vantages and pushing at flood_factor F times the natural rate cannot drive the broker CPU above: JOINT_attacked(F, K) / JOINT_baseline(K) <= R_L + F * (c_xdp / c_path) where JOINT_baseline(K) is the legitimate cost of K vantages at natural rate (essentially K * (c_path) per natural period) and c_path = c_json + c_bfd_parse + 2 * c_hmac. In particular, for F large, the ratio grows SUBLINEARLY in F with slope c_xdp / c_path = 0.05 / 8.70 = 0.00575. Without H-RL (rate-limit absent), the ratio is exactly F (linear, unbounded). PROOF. Step 1 (NIC ingress under H-RL). Each compromised vantage attempts to push at F * (1/T_tick_s) packets per second. H-RL admits to the verifier at most R_L * (1/T_tick_s) packets per second (sustained, after the burst budget has decayed). Step 2 (Per-vantage cost decomposition). Per compromised vantage per second: accepted_pps <= R_L / T_tick_s dropped_pps = (F - R_L) / T_tick_s (large F) cost_accepted = accepted_pps * c_path cost_xdp_drops = (accepted_pps + dropped_pps) * c_xdp ~~ F / T_tick_s * c_xdp (large F) Sum over K vantages: JOINT_attacked = K * (cost_accepted + cost_xdp_drops) = K * (R_L * c_path + F * c_xdp) / T_tick_s Step 3 (Baseline). Baseline cost per vantage at natural rate (F = 1, no drops): cost_baseline = c_path / T_tick_s JOINT_baseline = K * c_path / T_tick_s Step 4 (Ratio). JOINT_attacked / JOINT_baseline = (R_L * c_path + F * c_xdp) / c_path = R_L + F * (c_xdp / c_path) For default R_L = 4 and the constants of Section 1.2: slope = 0.05 / 8.70 = 0.00575 F = 1024 -> ratio <= 4 + 1024 * 0.00575 = 9.89 Step 5 (Without rate-limit). Without H-RL, every flood packet enters the verifier: cost_per_v = F * (1/T_tick_s) * c_path ratio = F QED. NUMERICAL RECEIPT (Section 4.4 of the draft). evidence/perfsec_verification_dos_receipt.json 6 flood factors x 2 modes; T-VDOS-1 and T-VDOS-NEG in scripts/validate_perfsec_coupling.py: PASS. At F = 1024, with-rate-limit ratio = 10.0x; without = 1024x. CONSEQUENCE. H-RL converts an unbounded linear DoS surface into a near-constant + sublinear bounded one. The rate_limit_factor controls the constant; the slope is fixed by the platform (c_xdp / c_path ratio). ============================================================================== 4. THEOREM T-RC-1 (REPLAY-COUNTER COHERENCE) ============================================================================== STATEMENT. Define the joint acceptance predicate at the broker: Accept(packet) iff (a) bfd_seq(packet) > last_bfd_seq[vantage] AND (b) cwt_counter(packet) > last_cwt[vantage, epoch] AND (c) expires_at(packet) > now() Under H-CWT-TRUST + H-BFD-AUTH (both HMACs unforgeable), Accept ACCEPTS every legitimate honest packet AND REJECTS every replay, forge, or stale packet, except with negligible probability bounded by HMAC PRF security. PROOF. Step 1 (Forge resistance of (a) and (b)). Predicate (a) checks bfd_seq monotonicity under K_BFD_auth. Forging a packet with bfd_seq > last_bfd_seq[vantage] requires forging a valid BFD AuthHMAC tag, which under H-BFD-AUTH + RFC 2104 requires K_BFD_auth. Predicate (b) checks cwt_counter monotonicity under K_v_epoch. Forging a packet with cwt_counter > last_cwt[vantage, epoch] requires forging a valid CWT HMAC tag, which under H-CWT-TRUST + RFC 2104 requires K_v_epoch. Both keys are independent under H-HKDF-PS. Forgery of either predicate is therefore a HMAC PRF distinguisher and has negligible probability (~ 2^-128 for SHA-256 truncated to the 32-octet tag). Step 2 (Honest acceptance). A legitimate honest packet carries: bfd_seq = last_bfd_seq[vantage] + 1 cwt_counter = last_cwt[vantage, epoch] + 1 (within epoch) or = 0 (first packet of new epoch, by CWT 9.1) expires_at > now() (by CWT issuer policy) All three predicates evaluate true; Accept returns true. Step 3 (Replay rejection). A byte-identical replay carries: bfd_seq = old bfd_seq <= last_bfd_seq[vantage] (fail (a)) cwt_counter = old cwt_counter <= last_cwt[v, ep] (fail (b)) Predicate (a) AND (b) are independent failures; either causes rejection. Cross-epoch replay (replaying an old-epoch packet after epoch_id increment) fails (a) because BFD seq does NOT reset across epochs (by CWT 9 vs Coh-BFD 12). Step 4 (Stale rejection). A packet with expired wrapper fails (c) regardless of (a)(b). Step 5 (Negligible-probability complement). The only remaining case is a forged packet with both HMACs valid; this requires breaking HMAC PRF security on either K_BFD_auth or K_v_epoch. Probability ~ 2^-128; negligible. QED. NUMERICAL WITNESS (Section 5 of the draft). T-RC-1.A and T-RC-1.B in scripts/validate_perfsec_coupling.py exercise Steps 2-4 constructively: PASS for honest acceptance; PASS for byte-replay; PASS for cross-epoch-replay; PASS for forge-bfd-with-old-cwt; PASS for forge-cwt-with-old-bfd. ============================================================================== 5. THEOREM T-COMP-SPLIT (DUAL-MODE COSIG DETECTION) ============================================================================== STATEMENT. Under H-DUAL-MODE (dual-mode (D_minimax, D_max) bound into the cosigned checkpoint extra field per Section 7 of the draft) and the witness independence of H-CWT-TRUST.H-WIT, any collector that publishes inconsistent dual-mode aggregates to distinct consumers under the same (bundle_id, bundle_seq) is detected by any auditor querying any honest witness within one checkpoint window. PROOF. Step 1 (CWT T-SPLIT-1 inheritance). CWT Theorem T-SPLIT-1 establishes that two consumers presented with two distinct cosigned bundles for the same (bundle_id, bundle_seq) detect the inconsistency with probability at least 1 - (1 - 1/w)^q. Step 2 (Dual-mode inclusion in the signed body). By H-DUAL-MODE, the (D_minimax, D_max) values are part of the checkpoint "extra" field that is hashed into the cosignature input. Distinct (D_minimax, D_max) pairs produce distinct extra fields, hence distinct checkpoint bytes, hence (by Step 1) distinct cosignatures. Step 3 (Reduction). Consumer A receives bundle_extra_A with (D_min_A, D_max_A); consumer B receives bundle_extra_B with (D_min_B, D_max_B); if either component differs, the bytes differ. The witness, by the standard tlog-witness first-cosign-wins policy [C2SP-TLOG-WITNESS], cosigns at most one body per (bundle_id, bundle_seq). An auditor querying any honest witness sees at most one cosigned body and therefore detects the discrepancy when comparing with another consumer's view. This closes the joint failure mode of DDoS-Resilience Theorem D2 Case 2 (perfect Byzantine hiding) composed with a compromised collector; the byzantine-included view (D_max above threshold) and byzantine-excluded view (D_minimax silent) cannot both be cosigned by the same honest witness under the same (bundle_id, bundle_seq). QED. ============================================================================== 6. COROLLARIES AND INHERITANCE RESULTS ============================================================================== 6.1. T-NIC-SUFF (NIC sized for legitimate telemetry suffices) Under H-DDOS-INV.I1 + H-RL with rate_limit_factor R_L and burst_factor B_F, the broker NIC PPS budget required is at most: NIC_PPS = PPS_t * (R_L + B_F / duration_amortization) For default R_L = 4, B_F = 8, amortized over a 60-second window, NIC_PPS ~ 4.13 * PPS_t. Operators MAY size NIC at 5 * PPS_t to subsume burst. PROOF: by H-RL, no vantage exceeds R_L sustained + B_F burst; sum over N vantages is the bound. Independent of R by H-DDOS-INV.I1 (Theorem D3 of D-4). 6.2. T-VOLINV (joint cost independent of attack rate) JOINT(N, T_tick, q) does not depend on the attack rate R. PROOF: every term of the joint formula depends only on PPS_t (which is N * (1000 / T_tick) by T-NIC-SUFF / Theorem D3) or on bundles_per_sec (which depends on cells_k, bundle_period_ticks, T_tick). No term references R. QED. 6.3. T-AUTH-INHERIT (CWT HMAC unforgeability preserved) The CWT HMAC roundtrip (T-AUTH-CWT-1) is preserved when composed with the BFD path under H-HKDF-PS. PROOF: H-HKDF-PS guarantees independence of K_v_epoch and K_BFD_auth. The CWT verifier on Path A operates on K_v_epoch only; the BFD verifier on Path B operates on K_BFD_auth only. Neither can substitute for the other. T-AUTH-CWT-1 is therefore preserved verbatim on Path A. QED. ============================================================================== 7. FINITE CHAIN BACK TO v4.0 ============================================================================== Every theorem of this document terminates at one of the following imported results: Theorem 9 of v4.0 (geometric-median max-bias) Theorem D3 of D-4 (NIC sizing volume-independence) T-AUTH-CWT-1 of CWT (HMAC unforgeability) T-COAL-1 of CWT (coalition resistance) T-SPLIT-1 of CWT (split-view detection) T-PARSE-1 of CWT (parser bounds) L_DL (detection-latency unification) RFC 2104 (HMAC-SHA256 PRF security) RFC 5869 (HKDF-SHA256 KDF security) RFC 8032 (Ed25519 EUF-CMA) No new mathematical primitive is introduced. The PerfSec-Coupling profile is a pure composition over the v4.0 catalogue plus the CWT proof catalogue plus L_DL. ============================================================================== 8. VALIDATOR EXIT CODE ============================================================================== The script scripts/validate_perfsec_coupling.py implements constructive numerical witnesses for every theorem above: T-JCOST-1.A joint cost monotone; Regime C in [150%, 200%] T-JCOST-1.B two-path decomposition exact (sum == joint) T-JCOST-1.C CWT abstract ref recovered (0.21 % HMAC alone) T-VDOS-1 attacked-CPU bounded by R_L + F * c_xdp/c_path T-VDOS-NEG necessity: without rate-limit, F=64 saturates T-RC-1.A AND(BFD seq, CWT counter); replay/forge rejected T-RC-1.B epoch boundary handled correctly T-HKDF-PS K_BFD_auth and K_v_epoch independent under K_op T-COMP-SPLIT dual-mode cosig detects split-view T-VOLINV joint cost constant across 10^6..10^12 pps T-AUTH-INHERIT CWT HMAC roundtrip preserved T-NIC-SUFF NIC sized at (R_L + 1) * legit PPS Exit code 0 on 12/12 PASS; non-zero on any failure. Recorded receipts: evidence/perfsec_joint_cost_receipt.json evidence/perfsec_verification_dos_receipt.json These receipts re-use the per-op cost constants of evidence/mvps_cwt_overhead_receipt.json, ensuring that every numerical claim in the draft is a deterministic function of a single hardware-pinned measurement file. ============================================================================== END OF PROOF DOCUMENT ==============================================================================