============================================================================== MVPS OPERATIONAL LOG FORMAT -- MATHEMATICAL PROOF (Append-only, hash-chained, externally-anchored, audit-grade logging for the MVPS family. Companion to draft-melegassi-opsawg-mvps-logging-00.) "Auditable means: anyone can detect a lie about the past. A log that the writer can silently edit is not a log; it is a draft." ============================================================================== Mathematical assembly: Leonardo Melegassi (Catellix) Produced: 2026-05-28 Companion: docs/draft-melegassi-opsawg-mvps-logging-00.txt Authority: docs/MVPS_TEN_COMMANDMENTS.txt (Commandment V: traceability) Anchors: docs/draft-melegassi-santos-ippm-mvps-cwt-00.txt (CWT checkpoint) docs/draft-melegassi-ippm-mvps-proof-envelope-00.txt (D-14) Numerical receipt: scripts/validate_logging_format.py (exit 0, 8/8) evidence/logging_format_receipt.json ============================================================================== 0. SCOPE AND HONEST FRAMING ============================================================================== This document specifies the tamper-EVIDENCE properties of the MVPS operational log. It proves what a hash chain DOES guarantee (no silent edit, reorder, or interior deletion of recorded events) and is explicit about what it does NOT guarantee (a bare chain cannot prove its own completeness; confidentiality is not provided). Per the methodology (D-16), every statement below is classified: [T] Theorem -- proved from an imported cryptographic result, [D] Design -- an explicit format/operational choice, [C] Conjecture -- empirical, with a falsification protocol. ============================================================================== 0.1 IMPORTED RESULTS (crypto basis, distinct from the statistical I1..I12 of v4.0) ============================================================================== J1. (Merkle 1989; Damgard 1989.) A collision-resistant compression function H: {0,1}* -> {0,1}^256 (SHA-256) is computationally binding: finding x != x' with H(x) = H(x') costs ~2^128 work (birthday: ~2^85 for a free collision; ~2^256 / 2^128 with Grover for a quantum preimage). J2. (Haber-Stornetta 1991.) Linked timestamping: if each record commits to the digest of its predecessor, then the head digest is a binding commitment to the entire ordered prefix; altering any element forces a collision in H. J3. (RFC 8785, JCS.) A deterministic canonicalization canon(.) of a JSON value exists and is independent of key insertion order. J4. (RFC 9162; C2SP tlog cosignature.) A witnessed checkpoint binds a (tree-size, root) pair under witness EUF-CMA, giving a publicly verifiable external anchor. A claim that cannot reduce to J1..J4 (for crypto) or to the v4.0 basis (for statistics) is not a theorem here. ============================================================================== 1. DEFINITIONS ============================================================================== F-L1. RECORD. r_i = { seq: i, prev_hash: p_i, ts, event, record_hash } where event is an arbitrary structured payload. F-L2. LEAF HASH. leaf(r_i) = H(canon(r_i \ {record_hash})), i.e. the digest of the canonical record body with its own record_hash field removed. F-L3. CHAIN LINK. p_0 = GENESIS (0^64); for i >= 1, p_i = leaf(r_{i-1}). record_hash_i = leaf(r_i). F-L4. HEAD. head(L) = record_hash of the last record (GENESIS if empty). F-L5. VALID LOG. L = (r_0,...,r_{n-1}) is valid iff for all i: seq_i = i, p_i = (GENESIS if i=0 else record_hash_{i-1}), and record_hash_i = leaf(r_i). F-L6. ANCHOR. a = (head_hash, count), optionally carried inside a CWT checkpoint (J4) or bound by the Proof Envelope (D-14). ============================================================================== 2. THEOREMS ============================================================================== ------------------------------------------------------------------------------ T-LOG-CHAIN-1 [T]. (Soundness.) The build/verify procedures of F-L3/F-L5 are mutually consistent: a log produced by appending records with correct links is VALID. ------------------------------------------------------------------------------ Proof. Immediate by construction: build sets p_i and record_hash_i exactly as F-L5 requires; verify recomputes leaf(r_i) and compares. By determinism of canon (J3) the recomputation matches. [] Validator: T-LOG-CHAIN-1 (exit 0). ------------------------------------------------------------------------------ T-LOG-EDIT-1 [T]. (No silent edit.) Let L be valid and let L' differ from L in the event or ts of exactly one record r_k (k arbitrary), with all other fields and the record_hash fields copied verbatim. Then L' is INVALID, unless the edit induced an H-collision. ------------------------------------------------------------------------------ Proof. Verification recomputes record_hash_k = leaf(r_k). Since the body of r_k changed, leaf(r_k) must change unless H collided (J1). The stored record_hash_k (copied from L) therefore mismatches, so verify fails at k. By contrapositive, passing verification after an edit yields an explicit H-collision, contradicting J1. [] Validator: T-LOG-EDIT-1 (exit 0). ------------------------------------------------------------------------------ T-LOG-REORDER-1 [T]. (No silent reorder.) Swapping two records at positions j < k of a valid log yields an INVALID log (absent a collision). ------------------------------------------------------------------------------ Proof. After the swap, the record now at position j carries seq != j (its original seq), failing the seq_i = i clause; even ignoring seq, its prev_hash no longer equals record_hash_{j-1}, so the link clause fails. Restoring both would require recomputing every downstream record_hash, i.e. rebuilding the chain -- which an honest verifier with the anchored head will then reject by T-LOG-ANCHOR-1. [] Validator: T-LOG-REORDER-1 (exit 0). ------------------------------------------------------------------------------ T-LOG-DELETE-1 [T]. (No silent interior deletion.) Deleting record r_k (0 < k < n-1) without rebuilding yields an INVALID log. ------------------------------------------------------------------------------ Proof. The record formerly at k+1 now sits at index k but still carries seq = k+1 (seq gap) and prev_hash = record_hash_k, which no longer equals record_hash_{k-1}; the link clause fails. [] Validator: T-LOG-DELETE-1 (exit 0). ------------------------------------------------------------------------------ T-LOG-TRUNC-1 [T] + HONEST NON-CLAIM. (Truncation needs an anchor.) A tail-truncated prefix L[:m] of a valid log L is ITSELF a valid log. Therefore tail truncation is NOT self-detectable from the chain alone. It IS detectable iff an external anchor a = (head(L), n) is available: then head(L[:m]) != head(L) or m != n. ------------------------------------------------------------------------------ Proof. Validity (F-L5) is a prefix-closed predicate: every clause for i < m holds in L[:m] exactly as in L. Hence L[:m] is valid; no internal witness distinguishes it from a complete log -- this is the honest non-claim. Given anchor a, J2 makes head a binding commitment to the full prefix, and J1 forbids a different prefix with the same head; so any m < n is exposed by head/count mismatch. [] Validator: T-LOG-TRUNC-1 (exit 0). This theorem is WHY Section 6 of the draft makes external anchoring REQUIRED for completeness guarantees. ------------------------------------------------------------------------------ T-LOG-ANCHOR-1 [T]. (Exact-prefix binding.) An anchor a = (h*, c*) accepts a log L iff head(L) = h* and |L| = c*; under J1/J2 at most one prefix satisfies a. ------------------------------------------------------------------------------ Proof. head is a function of the prefix; equality of head and count pins the prefix up to an H-collision (J1). Witness cosignature (J4) makes the anchor itself unforgeable. [] Validator: T-LOG-ANCHOR-1 (exit 0). ------------------------------------------------------------------------------ T-LOG-REDACT-1 [T] + [D]. (Redaction-compatible commitment.) Replacing a sensitive value v in an event by a salted commitment c = H(salt || v) (retaining salt) keeps the record verifiable: a holder of v reproduces c and the chain still binds, while a party without v learns nothing beyond c. This is binding (J1), not hiding in the IND sense -- it is a design trade, not encryption. ------------------------------------------------------------------------------ Proof. leaf(r) is computed over the committed form, so verification is unchanged. Reproduction: given (salt, v) recompute c; mismatch on any v' != v except under an H-collision (J1). [] Validator: T-LOG-REDACT-1 (exit 0). ============================================================================== 3. DESIGNS (explicit, not falsifiable) ============================================================================== D-LOG-SCHEMA. Records are JSON objects with the fixed top-level fields of F-L1; the event payload is open but RECOMMENDED to carry a "kind" taxonomy token and a "sev" severity in {debug, info, notice, warn, error, audit}. D-LOG-SEV. "audit" severity marks records that MUST survive retention and MUST be covered by an anchor. D-LOG-CBOR. A CBOR profile (RFC 8949) MAY replace JSON on constrained links (shared with the IoT/maritime profiles); canon(.) then follows CBOR deterministic encoding. Same theorems hold (H is byte-oriented). D-LOG-ANCHOR-CADENCE. Operators choose an anchoring cadence (per N records or per T seconds). Completeness is guaranteed only up to the most recent anchored head (T-LOG-TRUNC-1). ============================================================================== 4. CONJECTURES (with falsification protocol) ============================================================================== C-LOG-RATE. CONJECTURE: at sustained 10^4 records/s on commodity hardware, per-record chaining overhead (one SHA-256 over a < 1 KiB body) stays below 5% of total log-write cost. (a) observable: CPU time fraction in leaf()/H vs total write path; (b) data source: a load generator emitting the SAMPLE_EVENTS mix; (c) test: paired benchmark, report 95% CI, falsified if CI lower bound > 0.05; (d) current blocker: none -- a microbenchmark can run today; the claim is held as [C] until that receipt is added. ============================================================================== 5. WHAT THIS PROVES / DOES NOT PROVE ============================================================================== Proves: (i) recorded events cannot be silently edited, reordered, or interior-deleted (T-LOG-EDIT/REORDER/DELETE-1); (ii) with an external anchor, the exact log prefix is pinned and truncation is exposed (T-LOG-TRUNC-1, T-LOG-ANCHOR-1); (iii) redaction is compatible with verification (T-LOG-REDACT-1). Does NOT prove / explicitly disclaims: (a) completeness without an anchor (impossible by T-LOG-TRUNC-1); (b) confidentiality of payloads (the chain is binding, not hiding); (c) availability or non-repudiation of the WRITER beyond what the anchor's witness set provides. ============================================================================== 6. REFERENCES ============================================================================== [I-D.melegassi-opsawg-mvps-logging] this document's companion draft. [CWT] draft-melegassi-santos-ippm-mvps-cwt-00 (checkpoint anchor). [D-14] draft-melegassi-ippm-mvps-proof-envelope-00 (artifact binding). [HS91] Haber, S., Stornetta, W., "How to Time-Stamp a Digital Document", J. Cryptology, 1991. [RFC8785] Rundgren et al., "JSON Canonicalization Scheme (JCS)", 2020. [RFC9162] Laurie et al., "Certificate Transparency Version 2.0", 2021. [RFC5424] Gerhards, R., "The Syslog Protocol", 2009. ============================================================================== END OF MVPS LOGGING FORMAT MATHEMATICAL PROOF ==============================================================================