Files
proofs/universal-bridge-attestation-soundness.pdf
zeekayandHanzo Dev 9af352e0a1 proofs: universal bridge attestation soundness + M/T/F separation as a security boundary
New standalone proof (compiles, pdflatex clean) for the B-Chain o M-Chain
universal-bridge composition:

- Theorem "Bridge attestation soundness": destination D accepts a message m for
  event e only if m is the unique source-finalized message for e; wrongful
  acceptance reduces to a threshold-signature EUF-CMA forgery (< M honest
  M-Chain signers) OR a source-chain double-finalization (ruled out by the
  QuasarCert No-double-finalization theorem in quasar-cert-soundness.tex).
- Two disjoint honesty hypotheses on two chains (M-Chain threshold honesty +
  source stake honesty) — the "one concern, one chain" discipline.
- Lemma "Braiding enlarges the trusted surface" + Corollary "M/F separation is a
  security boundary": co-residing M-Chain signing shares with F-Chain FHE compute
  in one fault domain (the overloaded thresholdvm) adds an eps_FHE-leak term to
  the unforgeability bound; the LP-7100/LP-8200 split removes it.
- Implementation-status remark: genesis registry still has one overloaded T entry
  (no M/F rows); the split is the target posture (LP-7050 §8 tracks it).


Co-authored-by: Hanzo Dev <[email protected]>
2026-09-17 13:05:52 -07:00

223 KiB