Skip to content

🌊 trios-chat Wave-9: KEM-key-confusion + AAD-context-confusion + Coq 47/0 + 800/800 falsifier #650

@gHashTag

Description

@gHashTag

Refs #632 #636 #639 #643 #646 #648 trinity-fpga#28 trinity-fpga#37

🌊 Wave-9 mission

Stacks on Wave-8 (#648, merged as e991cec). Two new falsifier lanes; Coq +6; corpus 700β†’800.

Lanes

  • L-CHAT-1-conf β€” KEM-key-confusion (R-CHAT-1). Attacker substitutes another recipient's ml_kem_pk (or its ciphertext) and gets the sender to derive the wrong shared secret, then learn auth or content via cross-recipient confusion. Falsifier ring: CR-CHAT-01. Coq: INV-CHAT-34..36.
  • L-CHAT-5-aad β€” AAD-context-confusion (R-CHAT-1 / L-CHAT-5). At-rest AEAD wrap with mismatched / swapped AAD context (e.g., recipient_id swapped between rows), enabling cross-row replay or row-swap forgery. Falsifier ring: CR-CHAT-05. Coq: INV-CHAT-37..39.

Deliverables

  • 5 falsifier tests + 1 green-summary test per lane (12 new tests total)
  • 6 new Coq theorems β†’ 47 Qed / 0 Admitted
  • 100 new corpus payloads (50 kem_key_confusion + 50 aad_context_confusion) β†’ 800/800
  • Two new threshold lanes in falsifier_runner (β‰₯95%) β†’ 16 categories
  • Verification: ~150 tests Β· e2e 25/25 Β· falsifier 800/800 Β· clippy clean Β· Coq silent

Constitution

  • L1 (no .sh) βœ…
  • L2 (PR body starts with Closes) βœ…
  • L-ARCH-001 (rings only) βœ…

Anchor: φ² + φ⁻² = 3 Β· TRINITY Β· CHAT Β· ZERO-METADATA Β· POST-QUANTUM Β· UNLINKABLE Β· COVER-TIMING Β· AT-REST-AEAD Β· BOT-PARTIAL-MLS Β· KEM-KEY-CONFUSION Β· AAD-CONTEXT

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