Skip to content

🌊 trios-chat Wave-5: prekey hardening + MLS state machine + ML-KEM-768 wire-up + 400-falsifier #638

@gHashTag

Description

@gHashTag

Wave-5 hardening of the trios-chat ring stack delivered in PR #636 (Wave-3+4).

Refs #632 (EPIC) · Refs #637 (Wave-3+4) · Refs trinity-fpga#28 · Refs trinity-fpga#37

Scope (this issue closeable by Wave-5 PR)

  • L-CHAT-1 hardening — prekey-bundle 5-mutation falsifier (flipped sig, swapped order, expired, replay, foreign CA) in CR-CHAT-01
  • L-CHAT-2 forward secrecy + PCS gates — INV-CHAT proofs + CR-CHAT-02 unit tests for FS (compromise → past msg unreadable) and PCS (compromise → recover after one DH step)
  • L-CHAT-3 full MLS state machine — Welcome → Add → Update → Remove → Commit chain in CR-CHAT-03 (currently skeleton)
  • L-CHAT-8 ML-KEM-768 hybrid — actual KEM wired into CR-CHAT-01 prekey + CR-CHAT-02 ratchet step (currently only MLKEM_PUB_LEN/SEC_LEN placeholder constants)
  • Coq additionsforward_secrecy, post_compromise_security, prekey_uniqueness ⇒ 12 → 15 Defined, 0 Admitted
  • Falsifier 300 → 400 — +50 PQ-downgrade attacks, +50 group-state-rollback attacks; maintain 100% block per category
  • Verification — all chat-crate tests green + e2e 25/25 + falsifier 400/400 + clippy clean + Coq compiles

Anchor: φ² + φ⁻² = 3 · TRINITY · CHAT · ZERO-METADATA · PQ-HYBRID

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions