Skip to content

🌊 trios-chat Wave-10: ratchet-forward-secrecy + MLS commit-reorder + Coq 60/0 + 900/900 falsifier #663

@gHashTag

Description

@gHashTag

Wave-10 sub-tracker. Closed by Wave-10 PR.

Lanes:

  • L-CHAT-2-rfs (R-CHAT-2): Ratchet forward-secrecy + post-compromise security falsifier suite. 5 RFS-XX tests in CR-CHAT-02 + 50 ratchet_forward_secrecy corpus entries. Coq INV-CHAT-40..43 + chain_step_increases.
  • L-CHAT-3-mls (R-CHAT-11): MLS commit-reorder + cross-group splice falsifier suite. 5 MCR-XX tests in CR-CHAT-03 + 50 mls_commit_reorder corpus entries. Coq INV-CHAT-44..46 + process_commit_advances_one.

Targets:

  • Tests: 149 → 161
  • Coq: 51 Qed (Wave-9) → 60 Qed / 0 Admitted
  • Falsifier: 800 → 900, 16 → 18 categories @ 100%
  • Clippy clean, e2e 25/25

Refs #648 #651 #632 trinity-fpga#28

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