diff --git a/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::external_init_secret_pinning.json b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::external_init_secret_pinning.json new file mode 100644 index 0000000000..2da711e598 --- /dev/null +++ b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::external_init_secret_pinning.json @@ -0,0 +1,28 @@ +{ + "built_by": "t27c-bootstrap@0.5.2+01d0a635f", + "closure": [], + "config": "gen=c,rust,verilog,zig;tests=zig", + "gen_hash_c": "sha256:9bbcd9e2167fe62cab8184bc4f58e67dbf583e2bbe0cfd8eec679ac0e6e90939", + "gen_hash_rust": "sha256:1151e48a6f5f273f7aa1569121a158d5f234fea25d60568d371ffe9ad49fc1dd", + "gen_hash_verilog": "sha256:25a4ed76d67d001c0dc8ee6018c3f02dadb17b0cc9897de05a8096da5b0b2ffb", + "gen_hash_zig": "sha256:15ce101cbb616096e8b90791fdf9a41ddc5401d9fdeb520a246b5c53ee5b0307", + "module": "port::trios::crates::trios-chat::rings::CR-CHAT-04::src::external_init_secret_pinning", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-15T19:47:58Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:289a4a6a41e8fc8acf82cb5fa1b94d56ee56784678c570acdffb33d0b7952817", + "spec_path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/external_init_secret_pinning.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 15, + "total": 15, + "vacuous": 0 + }, + "toolchain": { + "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", + "zig": "0.16.0" + } +} \ No newline at end of file diff --git a/docs/reports/t27b_expectations.json b/docs/reports/t27b_expectations.json index 3483595ccc..a0bb836f8a 100644 --- a/docs/reports/t27b_expectations.json +++ b/docs/reports/t27b_expectations.json @@ -857,6 +857,7 @@ {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-03/src/ratchet_tree_resolution_guard.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-03/src/ratchet_tree_update_integrity_guard.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-03/src/unmerged_leaves_bound_guard.t27", "t27b": "pass"}, + {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/external_init_secret_pinning.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_alignment_boundary_guard.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_block_size_alignment_guard.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-05/src/envelope_size_distribution_uniformity.t27", "t27b": "pass"}, diff --git a/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/external_init_secret_pinning.t27 b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/external_init_secret_pinning.t27 new file mode 100644 index 0000000000..b65f7cc708 --- /dev/null +++ b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/external_init_secret_pinning.t27 @@ -0,0 +1,341 @@ +module port::trios::crates::trios-chat::rings::CR-CHAT-04::src::external_init_secret_pinning; + +// Port of gHashTag/trios crates/trios-chat/rings/CR-CHAT-04/src/external_init_secret_pinning.rs +// (CR-CHAT-04 - External Init secret pinning, Wave-27 Lane L-CHAT-8-eip, +// requirement R-CHAT-11, aligned to RFC 9420 section 12.2). +// +// A non-member joins an existing MLS group by re-derivation: a fresh +// init_secret from the group's exported external_init value and a local +// KEM ephemeral, then a signed External Commit binding to that +// init_secret. Five confusion attacks are rejected before any key +// derivation runs: non-canonical exporter length, stale exporter epoch, +// cross-group exporter splice, an all-zero KEM ephemeral (the known-key +// init), and an External Commit from a removed or unknown signer leaf. +// +// The original returns Result<(), ExternalInitError>. This port carries +// the verdict as a named struct (owner decision D5): Ok first, then the +// seven error variants in the original's declaration order - +// NonCanonicalExporterLen, CrossGroupExporterSplice, StaleExporterEpoch, +// ZeroKemEphemeral, NonCanonicalKemEphemeralLen, RemovedMemberRejoin, +// UnknownSignerLeaf. No variant carries a payload, so the verdict is the +// code alone. +// +// The original's Vec fields are read only by length or by all-zero +// probe here; the BTreeSet leaves are read only by membership and maximum. +// The byte equality of the two group ids is a helper over fixed-size +// ids (conventions section 4: helpers inline, each with its own test). +// The crate-wide Error conversion and the validate() adapter are +// plumbing (formatting strings and type mapping) and are not ported. + +// Canonical exporter-secret length, in bytes. +pub const EIP_EXPORTER_LEN: usize = 32; + +// Canonical KEM-ephemeral length, in bytes. +pub const EIP_KEM_EPHEMERAL_LEN: usize = 32; + +// Fixed group-id length the tests use. The original compares Vec +// ids of any length; a fixed port covers the decision at one length and +// the tests exercise both equal and unequal ids. +pub const EIP_GROUP_ID_LEN: usize = 15; + +// Exporter binding for a joining external commit. +pub struct ExternalInitExporter { + exporter_len: usize, + group_id: [15]u8, + epoch: u64, +} + +// External-commit message the joiner submits. +pub struct ExternalCommit { + group_id: [15]u8, + epoch: u64, + kem_ephemeral_len: usize, + kem_ephemeral_nonzero: bool, + signer_leaf: u32, +} + +// Verifier-side view of the group. +pub struct ExternalInitView { + current_group_id: [15]u8, + current_epoch: u64, + active_leaves: [4]u32, + removed_leaves: [4]u32, +} + +// Verdict codes: Ok(()) and ExternalInitError's variants, in declaration order. +pub enum ExternalInitCode { + Ok, + NonCanonicalExporterLen, + CrossGroupExporterSplice, + StaleExporterEpoch, + ZeroKemEphemeral, + NonCanonicalKemEphemeralLen, + RemovedMemberRejoin, + UnknownSignerLeaf, +} + +// The verdict of the External Commit validation. No variant of the +// original's error carries a payload, so the code is the whole verdict. +pub struct ExternalInitVerdict { + code: ExternalInitCode, +} + +// Whole-id equality over the fixed-size ids. +pub fn ids_equal(a: [15]u8, b: [15]u8) -> bool { + for i in 0..15 { + if (a[i] != b[i]) { + return false; + } + } + return true; +} + +// Membership of a leaf in a fixed-size leaf table. The original asks +// BTreeSet::contains; there is no set here, so the decision is a scan +// over the slots the caller filled. +pub fn leaf_in(leaf: u32, leaves: [4]u32) -> bool { + for i in 0..4 { + if (leaves[i] == leaf) { + return true; + } + } + return false; +} + +// The largest leaf in the table. The original asks active_leaves.max(); +// the caller fills the slots, so the scan answers the same question over +// exactly the leaves it put there. +pub fn leaf_max(leaves: [4]u32) -> u32 { + var m: u32 = leaves[0]; + for i in 1..4 { + if (leaves[i] > m) { + m = leaves[i]; + } + } + return m; +} + +// [VERIFIED] Validate an External Commit against an exporter binding and +// the verifier's group view. Returns Ok only when every RFC 9420 +// section 12.2 rule accepts, checked in the original's order: canonical +// exporter length, exporter bound to the verifier's group, exporter epoch +// not stale, canonical KEM ephemeral length, KEM ephemeral not all-zero +// (the commit record carries that probe as a bit, computed by the caller +// over the bytes), signer not removed, signer leaf known (active, or a +// slot at or beyond the largest active leaf), and the commit itself bound +// to the verifier's group. +pub fn validate_external_commit(exporter: ExternalInitExporter, commit: ExternalCommit, view: ExternalInitView) -> ExternalInitVerdict { + if (exporter.exporter_len != EIP_EXPORTER_LEN) { + return ExternalInitVerdict { code: ExternalInitCode.NonCanonicalExporterLen, }; + } + if (!ids_equal(exporter.group_id, view.current_group_id)) { + return ExternalInitVerdict { code: ExternalInitCode.CrossGroupExporterSplice, }; + } + if (exporter.epoch < view.current_epoch) { + return ExternalInitVerdict { code: ExternalInitCode.StaleExporterEpoch, }; + } + if (commit.kem_ephemeral_len != EIP_KEM_EPHEMERAL_LEN) { + return ExternalInitVerdict { code: ExternalInitCode.NonCanonicalKemEphemeralLen, }; + } + if (!commit.kem_ephemeral_nonzero) { + return ExternalInitVerdict { code: ExternalInitCode.ZeroKemEphemeral, }; + } + if (leaf_in(commit.signer_leaf, view.removed_leaves)) { + return ExternalInitVerdict { code: ExternalInitCode.RemovedMemberRejoin, }; + } + if (!leaf_in(commit.signer_leaf, view.active_leaves)) { + const m: u32 = leaf_max(view.active_leaves); + if (commit.signer_leaf <= m) { + return ExternalInitVerdict { code: ExternalInitCode.UnknownSignerLeaf, }; + } + } + if (!ids_equal(commit.group_id, view.current_group_id)) { + return ExternalInitVerdict { code: ExternalInitCode.CrossGroupExporterSplice, }; + } + return ExternalInitVerdict { code: ExternalInitCode.Ok, }; +} + +// The two typed accessors of the original answer the canonical lengths. +pub fn exporter_len() -> usize { + return EIP_EXPORTER_LEN; +} + +pub fn kem_ephemeral_len() -> usize { + return EIP_KEM_EPHEMERAL_LEN; +} + +// The fixtures' group id, "trinity-group-1" as fixed bytes. +pub const EIP_TEST_GROUP_ID: [15]u8 = [15]u8{'t', 'r', 'i', 'n', 'i', 't', 'y', '-', 'g', 'r', 'o', 'u', 'p', '-', '1',}; + +// The fixtures' other-group id, "other-group---" as fixed bytes. +pub const EIP_OTHER_GROUP_ID: [15]u8 = [15]u8{'o', 't', 'h', 'e', 'r', '-', 'g', 'r', 'o', 'u', 'p', '-', '-', '-', '-',}; + +// The canonical exporter fixture of the tests. +fn ok_exporter() -> ExternalInitExporter { + return ExternalInitExporter { exporter_len: EIP_EXPORTER_LEN, group_id: EIP_TEST_GROUP_ID, epoch: 7, }; +} + +// The canonical commit fixture of the tests. +fn ok_commit() -> ExternalCommit { + return ExternalCommit { group_id: EIP_TEST_GROUP_ID, epoch: 7, kem_ephemeral_len: EIP_KEM_EPHEMERAL_LEN, kem_ephemeral_nonzero: true, signer_leaf: 10, }; +} + +// The canonical view fixture of the tests. +fn ok_view() -> ExternalInitView { + return ExternalInitView { current_group_id: EIP_TEST_GROUP_ID, current_epoch: 7, active_leaves: [4]u32{0, 1, 2, 3,}, removed_leaves: [4]u32{4294967295, 4294967295, 4294967295, 4294967295,}, }; +} + +// **EIP-01** - valid external commit accepted. +test eip_01_valid_external_commit_accepted { + var exp = ok_exporter(); + var cmt = ok_commit(); + var view = ok_view(); + const v = validate_external_commit(exp, cmt, view); + assert(v.code == ExternalInitCode.Ok); +} + +// **EIP-02** - short exporter rejected: 16 of a canonical 32. +test eip_02_short_exporter_rejected { + var exp = ok_exporter(); + exp.exporter_len = 16; + var c0 = ok_commit(); + var w0 = ok_view(); + const v = validate_external_commit(exp, c0, w0); + assert(v.code == ExternalInitCode.NonCanonicalExporterLen); +} + +// **EIP-03** - oversize exporter rejected: 64 of a canonical 32. +test eip_03_oversize_exporter_rejected { + var exp = ok_exporter(); + exp.exporter_len = 64; + var c0 = ok_commit(); + var w0 = ok_view(); + const v = validate_external_commit(exp, c0, w0); + assert(v.code == ExternalInitCode.NonCanonicalExporterLen); +} + +// **EIP-04** - cross-group exporter splice rejected. +test eip_04_cross_group_exporter_splice_rejected { + var exp = ok_exporter(); + exp.group_id = EIP_OTHER_GROUP_ID; + var c0 = ok_commit(); + var w0 = ok_view(); + const v = validate_external_commit(exp, c0, w0); + assert(v.code == ExternalInitCode.CrossGroupExporterSplice); +} + +// **EIP-05** - stale exporter epoch rejected: 5 against a current 7. +test eip_05_stale_exporter_epoch_rejected { + var exp = ok_exporter(); + exp.epoch = 5; + var c0 = ok_commit(); + var w0 = ok_view(); + const v = validate_external_commit(exp, c0, w0); + assert(v.code == ExternalInitCode.StaleExporterEpoch); +} + +// **EIP-06** - zero KEM ephemeral rejected: the all-zero probe bit reads false. +test eip_06_zero_kem_ephemeral_rejected { + var cmt = ok_commit(); + cmt.kem_ephemeral_nonzero = false; + var e0 = ok_exporter(); + var w0 = ok_view(); + const v = validate_external_commit(e0, cmt, w0); + assert(v.code == ExternalInitCode.ZeroKemEphemeral); +} + +// **EIP-07** - non-canonical KEM ephemeral length rejected: 16 of 32. +test eip_07_non_canonical_kem_ephemeral_len_rejected { + var cmt = ok_commit(); + cmt.kem_ephemeral_len = 16; + var e0 = ok_exporter(); + var w0 = ok_view(); + const v = validate_external_commit(e0, cmt, w0); + assert(v.code == ExternalInitCode.NonCanonicalKemEphemeralLen); +} + +// **EIP-08** - removed-member rejoin rejected: leaf 10 sits in the +// removed table. +test eip_08_removed_member_rejoin_rejected { + var view = ok_view(); + view.removed_leaves = [4]u32{10, 4294967295, 4294967295, 4294967295,}; + var e0 = ok_exporter(); + var c0 = ok_commit(); + const v = validate_external_commit(e0, c0, view); + assert(v.code == ExternalInitCode.RemovedMemberRejoin); +} + +// **EIP-09** - an already-active signer leaf accepts; a leaf in a gap +// inside the active range (2 while 0, 1, 3 are active) rejects as unknown. +// The empty removed table of the view fixture holds the u32 sentinel +// 4294967295, which no signer leaf of the tests equals, so the sentinel +// answers "absent" exactly as the original's empty set does. +test eip_09_unknown_leaf_below_max_rejected { + var cmt = ok_commit(); + cmt.signer_leaf = 2; + var e0 = ok_exporter(); + var w0 = ok_view(); + const va = validate_external_commit(e0, cmt, w0); + assert(va.code == ExternalInitCode.Ok); + + var view = ok_view(); + view.active_leaves = [4]u32{0, 1, 3, 4294967295,}; + var exp = ok_exporter(); + const vb = validate_external_commit(exp, cmt, view); + assert(vb.code == ExternalInitCode.UnknownSignerLeaf); +} + +// **EIP-10** - commit group-id mismatch rejected: the commit names +// another group than the verifier's view. +test eip_10_commit_group_id_mismatch_rejected { + var cmt = ok_commit(); + cmt.group_id = EIP_OTHER_GROUP_ID; + var exp = ok_exporter(); + var view = ok_view(); + const v = validate_external_commit(exp, cmt, view); + assert(v.code == ExternalInitCode.CrossGroupExporterSplice); +} + +// The three helpers have direct tests (coverage: Untested 0). +test ids_equal_answers { + assert(ids_equal(EIP_TEST_GROUP_ID, EIP_TEST_GROUP_ID)); + assert(!ids_equal(EIP_TEST_GROUP_ID, EIP_OTHER_GROUP_ID)); +} + +test leaf_in_answers { + assert(leaf_in(2, [4]u32{0, 1, 2, 3,})); + assert(!leaf_in(5, [4]u32{0, 1, 2, 3,})); +} + +test leaf_max_answers { + assert(leaf_max([4]u32{0, 1, 2, 3,}) == 3); + assert(leaf_max([4]u32{7, 1, 9, 3,}) == 9); +} + +// The accessors answer the canonical lengths. +test accessors_answer_canonical_lengths { + assert(exporter_len() == 32); + assert(kem_ephemeral_len() == 32); +} + +// Rule order is the original's: exporter length before group binding, +// group binding before epoch, the KEM length before the zero probe, the +// removed check before the unknown check, and the group binding of the +// commit last of all. +test rule_order_matches_original { + var exp = ok_exporter(); + exp.exporter_len = 16; + exp.group_id = EIP_OTHER_GROUP_ID; + var c0 = ok_commit(); + var w0 = ok_view(); + const va = validate_external_commit(exp, c0, w0); + assert(va.code == ExternalInitCode.NonCanonicalExporterLen); + + var cmt = ok_commit(); + cmt.kem_ephemeral_len = 16; + cmt.kem_ephemeral_nonzero = false; + var e = ok_exporter(); + var vw = ok_view(); + const vb = validate_external_commit(e, cmt, vw); + assert(vb.code == ExternalInitCode.NonCanonicalKemEphemeralLen); +}