From 973332dfdc8a79db589629a53323d2a6ad3460cc Mon Sep 17 00:00:00 2001 From: dmitrii-f-t27 Date: Fri, 16 Oct 2026 12:17:57 -0300 Subject: [PATCH] spec(port): port the welcome path_secret unmasking defense (Refs #8884) The thirty-fourth and final W2 target of the CR-CHAT-04 ring tracker: the Welcome path-secret rules - every secret exactly thirty-two bytes, the group id matching the local one, the epoch not stale, no secret shared across distinct positions, the joiner's own leaf never sent, and every required ancestor delivered - as the D5 verdict with the missing node index riding rule six, the original's fixed rule order, and all ten WPS tests transcribed plus helper and rule-order tests. The original's WelcomePacket and receiver View become the validator's parameters (t27 has no slice fields); the group ids become the fixed [17]u8 form; the Vec secret becomes the fixed [32]u8 form plus its length. A secret repeated at the same position re-inserts cleanly, exactly as the original's map allows. The original's tautological green check becomes a live empty-bundle validation (0 vacuous). Checks (conventions 0-14): t27b test 12 passed 0 failed; t27c test-report 12/12, 0 vacuous; gen-rust output compiles under rustc; coverage Untested 0; ASCII only; seal saved, all hashes MATCH; --- ...4::src::welcome_path_secret_unmasking.json | 28 ++ docs/reports/t27b_expectations.json | 1 + .../src/welcome_path_secret_unmasking.t27 | 346 ++++++++++++++++++ 3 files changed, 375 insertions(+) create mode 100644 .trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::welcome_path_secret_unmasking.json create mode 100644 specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/welcome_path_secret_unmasking.t27 diff --git a/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::welcome_path_secret_unmasking.json b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::welcome_path_secret_unmasking.json new file mode 100644 index 0000000000..fae7999838 --- /dev/null +++ b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::welcome_path_secret_unmasking.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:24dd121e66c38ee79de29c759f94d6563cb4dd8b9b2b587bd1cf31f4257618d0", + "gen_hash_rust": "sha256:ac038996d7cae42963b4e003b2e7352fa2136ef41545c1ca4d1e522b3486d8f4", + "gen_hash_verilog": "sha256:2bea91103b936a646f4321514ab654b17dcd1b3d12add3b886569f977bc3c87f", + "gen_hash_zig": "sha256:f22103d925fa50a97fcfcb27a1222443739a2a771da543c6f274cc97fbcd97fb", + "module": "port::trios::crates::trios-chat::rings::CR-CHAT-04::src::welcome_path_secret_unmasking", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-16T15:17:22Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:e7fd07ee662b8d6456304275982bdf6e6e93214726302d446db622bac1075793", + "spec_path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/welcome_path_secret_unmasking.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 12, + "total": 12, + "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 c041cbab56..1e6a1b6058 100644 --- a/docs/reports/t27b_expectations.json +++ b/docs/reports/t27b_expectations.json @@ -853,6 +853,7 @@ {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-02/src/epoch_rollover_wraparound_guard.t27", "t27b": "pass"}, {"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/unmerged_leaves_bound_guard.t27", "t27b": "pass"}, + {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/welcome_path_secret_unmasking.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-05/src/envelope_size_distribution_uniformity.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-07/src/cover_decoy_ratio_governor.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-LAWS/src/lib.t27", "t27b": "pass"}, diff --git a/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/welcome_path_secret_unmasking.t27 b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/welcome_path_secret_unmasking.t27 new file mode 100644 index 0000000000..47a722ebde --- /dev/null +++ b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/welcome_path_secret_unmasking.t27 @@ -0,0 +1,346 @@ +module port::trios::crates::trios-chat::rings::CR-CHAT-04::src::welcome_path_secret_unmasking; + +// Port of gHashTag/trios crates/trios-chat/rings/CR-CHAT-04/src/welcome_path_secret_unmasking.rs +// (CR-CHAT-04 - Welcome path_secret unmasking defense, Wave-30 +// Lane B, requirement R-CHAT-4; RFC 9420 12.4.3.2 and 7.6). +// +// A new member joins through a Welcome that HPKE-masks one +// path_secret per ancestor node. A forger can collapse the +// TreeKEM by delivering one secret to many nodes, substitute +// the all-zero secret, pad the path with the joiner's own leaf +// (off-leaf unmasking), or drop an ancestor the joiner needs +// and silently lose forward secrecy. The rules, in the +// original's fixed order: every secret exactly thirty-two +// bytes, the group id equal to the local one, the epoch not +// stale, no secret shared across distinct positions, the +// joiner's own leaf never sent, and every required ancestor +// delivered. +// +// The original returns Result<(), WelcomePathSecretError>. This +// port carries the verdict as a named struct (owner decision +// D5): Ok first, then the six variants in the original's +// declaration order - NonCanonicalSecretLength, +// CrossGroupWelcome, StaleEpochWelcome, DuplicatePathSecret, +// OffLeafPathSecret, MissingAncestorPathSecret - with the one +// payload field: the missing node index rides the verdict for +// rule six. +// +// The original's WelcomePacket and receiver View become the +// validator's parameters (t27 has no slice fields); the group +// ids become the fixed [17]u8 form - both fixture ids are +// seventeen bytes - compared by a scan. The Vec path +// secret becomes the fixed [32]u8 form plus its length; the +// BTreeMap and BTreeSet probes become scans. A secret repeated +// at the SAME position re-inserts cleanly, exactly as the +// original's map allows. + +// Canonical path_secret length for MLS HPKE-OKP suites. +pub const WELCOME_PATH_SECRET_LEN: usize = 32; + +// One node on the joiner's direct path. +pub struct WelcomePathSecret { + position: u32, + path_secret: [32]u8, + secret_len: usize, +} + +// Verdict codes: Ok(()) and WelcomePathSecretError's variants, in declaration order. +pub enum WelcomePathSecretCode { + Ok, + NonCanonicalSecretLength, + CrossGroupWelcome, + StaleEpochWelcome, + DuplicatePathSecret, + OffLeafPathSecret, + MissingAncestorPathSecret, +} + +// The verdict of the Welcome path-secret validation, with the +// missing node index for rule six. +pub struct WelcomePathSecretVerdict { + code: WelcomePathSecretCode, + missing: u32, +} + +// Whole-form equality over the fixed thirty-two secret bytes. +pub fn secrets_equal(a: [32]u8, b: [32]u8) -> bool { + for i in 0..32 { + if (a[i] != b[i]) { + return false; + } + } + return true; +} + +// Whole-form equality over the seventeen group-id bytes. +pub fn group_ids_equal(a: [17]u8, b: [17]u8) -> bool { + for i in 0..17 { + if (a[i] != b[i]) { + return false; + } + } + return true; +} + +// Whether secret i shares its bytes with an earlier secret +// under a different position - the original's BTreeMap probe, +// answered by a scan. A repeat at the same position is the +// original's clean re-insert and passes. +pub fn secret_dup_at_other_position(path_secrets: []const WelcomePathSecret, i: usize) -> bool { + for j in 0..i { + if (secrets_equal(path_secrets[j].path_secret, path_secrets[i].path_secret)) { + if (path_secrets[j].position != path_secrets[i].position) { + return true; + } + } + } + return false; +} + +// Whether any delivered secret sits at the given position - the +// original's BTreeSet membership probe, answered by a scan. +pub fn position_delivered(path_secrets: []const WelcomePathSecret, pos: u32) -> bool { + for i in 0..path_secrets.len { + if (path_secrets[i].position == pos) { + return true; + } + } + return false; +} + +// [VERIFIED] Validate the path_secret bundle inside a Welcome +// against the joiner view. Returns Ok only when all six rules +// pass, checked in the original's fixed order: the secret +// lengths, the group id, the epoch, the cross-position +// duplicate scan, the joiner's own leaf, and the required +// ancestors. +pub fn validate_welcome_path_secrets( + group_id: [17]u8, + epoch: u64, + joiner_leaf: u32, + path_secrets: []const WelcomePathSecret, + local_group_id: [17]u8, + current_epoch: u64, + required_ancestors: []const u32, +) -> WelcomePathSecretVerdict { + for i in 0..path_secrets.len { + if (path_secrets[i].secret_len != WELCOME_PATH_SECRET_LEN) { + return WelcomePathSecretVerdict { code: WelcomePathSecretCode.NonCanonicalSecretLength, missing: 0, }; + } + } + if (!group_ids_equal(group_id, local_group_id)) { + return WelcomePathSecretVerdict { code: WelcomePathSecretCode.CrossGroupWelcome, missing: 0, }; + } + if (epoch < current_epoch) { + return WelcomePathSecretVerdict { code: WelcomePathSecretCode.StaleEpochWelcome, missing: 0, }; + } + for i in 0..path_secrets.len { + if (secret_dup_at_other_position(path_secrets, i)) { + return WelcomePathSecretVerdict { code: WelcomePathSecretCode.DuplicatePathSecret, missing: 0, }; + } + } + for i in 0..path_secrets.len { + if (path_secrets[i].position == joiner_leaf) { + return WelcomePathSecretVerdict { code: WelcomePathSecretCode.OffLeafPathSecret, missing: 0, }; + } + } + for r in 0..required_ancestors.len { + if (!position_delivered(path_secrets, required_ancestors[r])) { + return WelcomePathSecretVerdict { code: WelcomePathSecretCode.MissingAncestorPathSecret, missing: required_ancestors[r], }; + } + } + return WelcomePathSecretVerdict { code: WelcomePathSecretCode.Ok, missing: 0, }; +} + +// The group ids of the fixtures: "trinity-group-001" and its +// hostile stand-in "hostile-group-XYZ", byte by byte. +pub const GROUP_ID_LOCAL: [17]u8 = [17]u8{116, 114, 105, 110, 105, 116, 121, 45, 103, 114, 111, 117, 112, 45, 48, 48, 49,}; +pub const GROUP_ID_HOSTILE: [17]u8 = [17]u8{104, 111, 115, 116, 105, 108, 101, 45, 103, 114, 111, 117, 112, 45, 88, 89, 90,}; + +// The path secrets of the fixtures, one byte repeated thirty-two +// times - the original's canon_secret helper, entry by entry. +pub const SECRET_33: [32]u8 = [32]u8{51, 51, 51, 51, 51, 51, 51, 51, 51, 51, 51, 51, 51, 51, 51, 51, 51, 51, 51, 51, 51, 51, 51, 51, 51, 51, 51, 51, 51, 51, 51, 51,}; +pub const SECRET_77: [32]u8 = [32]u8{119, 119, 119, 119, 119, 119, 119, 119, 119, 119, 119, 119, 119, 119, 119, 119, 119, 119, 119, 119, 119, 119, 119, 119, 119, 119, 119, 119, 119, 119, 119, 119,}; +pub const SECRET_AA: [32]u8 = [32]u8{170, 170, 170, 170, 170, 170, 170, 170, 170, 170, 170, 170, 170, 170, 170, 170, 170, 170, 170, 170, 170, 170, 170, 170, 170, 170, 170, 170, 170, 170, 170, 170,}; +pub const SECRET_ZERO: [32]u8 = [32]u8{0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,}; + +// The required ancestors of the base view: nodes 3 and 7. +pub const REQUIRED_2: [2]u32 = [2]u32{3, 7,}; + +// **WPS-01** - a short sixteen-byte path_secret rejected. +test wps_01_short_secret_rejected { + const secrets: [2]WelcomePathSecret = [2]WelcomePathSecret{ + WelcomePathSecret { position: 3, path_secret: SECRET_33, secret_len: 16, }, + WelcomePathSecret { position: 7, path_secret: SECRET_77, secret_len: 32, }, + }; + const v = validate_welcome_path_secrets(GROUP_ID_LOCAL, 6, 0, &secrets, GROUP_ID_LOCAL, 5, &REQUIRED_2); + assert(v.code == WelcomePathSecretCode.NonCanonicalSecretLength); +} + +// **WPS-02** - an over-long sixty-four-byte path_secret rejected. +test wps_02_long_secret_rejected { + const secrets: [2]WelcomePathSecret = [2]WelcomePathSecret{ + WelcomePathSecret { position: 3, path_secret: SECRET_33, secret_len: 32, }, + WelcomePathSecret { position: 7, path_secret: SECRET_77, secret_len: 64, }, + }; + const v = validate_welcome_path_secrets(GROUP_ID_LOCAL, 6, 0, &secrets, GROUP_ID_LOCAL, 5, &REQUIRED_2); + assert(v.code == WelcomePathSecretCode.NonCanonicalSecretLength); +} + +// **WPS-03** - a cross-group Welcome rejected. +test wps_03_cross_group_welcome_rejected { + const secrets: [2]WelcomePathSecret = [2]WelcomePathSecret{ + WelcomePathSecret { position: 3, path_secret: SECRET_33, secret_len: 32, }, + WelcomePathSecret { position: 7, path_secret: SECRET_77, secret_len: 32, }, + }; + const v = validate_welcome_path_secrets(GROUP_ID_HOSTILE, 6, 0, &secrets, GROUP_ID_LOCAL, 5, &REQUIRED_2); + assert(v.code == WelcomePathSecretCode.CrossGroupWelcome); +} + +// **WPS-04** - a stale-epoch Welcome rejected: epoch four of a +// current five. +test wps_04_stale_epoch_welcome_rejected { + const secrets: [2]WelcomePathSecret = [2]WelcomePathSecret{ + WelcomePathSecret { position: 3, path_secret: SECRET_33, secret_len: 32, }, + WelcomePathSecret { position: 7, path_secret: SECRET_77, secret_len: 32, }, + }; + const v = validate_welcome_path_secrets(GROUP_ID_LOCAL, 4, 0, &secrets, GROUP_ID_LOCAL, 5, &REQUIRED_2); + assert(v.code == WelcomePathSecretCode.StaleEpochWelcome); +} + +// **WPS-05** - a path_secret shared across two positions +// rejected: position seven carries position three's bytes. +test wps_05_duplicate_path_secret_rejected { + const secrets: [2]WelcomePathSecret = [2]WelcomePathSecret{ + WelcomePathSecret { position: 3, path_secret: SECRET_33, secret_len: 32, }, + WelcomePathSecret { position: 7, path_secret: SECRET_33, secret_len: 32, }, + }; + const v = validate_welcome_path_secrets(GROUP_ID_LOCAL, 6, 0, &secrets, GROUP_ID_LOCAL, 5, &REQUIRED_2); + assert(v.code == WelcomePathSecretCode.DuplicatePathSecret); +} + +// **WPS-06** - the joiner's own leaf delivered: off-leaf +// unmasking rejected. +test wps_06_off_leaf_path_secret_rejected { + const secrets: [2]WelcomePathSecret = [2]WelcomePathSecret{ + WelcomePathSecret { position: 3, path_secret: SECRET_33, secret_len: 32, }, + WelcomePathSecret { position: 7, path_secret: SECRET_77, secret_len: 32, }, + }; + const v = validate_welcome_path_secrets(GROUP_ID_LOCAL, 6, 3, &secrets, GROUP_ID_LOCAL, 5, &REQUIRED_2); + assert(v.code == WelcomePathSecretCode.OffLeafPathSecret); +} + +// **WPS-07** - a missing required ancestor rejected: node seven +// never delivered, its index carried back. +test wps_07_missing_required_ancestor_rejected { + const secrets: [1]WelcomePathSecret = [1]WelcomePathSecret{ + WelcomePathSecret { position: 3, path_secret: SECRET_33, secret_len: 32, }, + }; + const v = validate_welcome_path_secrets(GROUP_ID_LOCAL, 6, 0, &secrets, GROUP_ID_LOCAL, 5, &REQUIRED_2); + assert(v.code == WelcomePathSecretCode.MissingAncestorPathSecret); + assert(v.missing == 7); +} + +// **WPS-08** - an extra optional ancestor accepted: node eleven +// rides along harmlessly. +test wps_08_extra_optional_ancestor_accepted { + const secrets: [3]WelcomePathSecret = [3]WelcomePathSecret{ + WelcomePathSecret { position: 3, path_secret: SECRET_33, secret_len: 32, }, + WelcomePathSecret { position: 7, path_secret: SECRET_77, secret_len: 32, }, + WelcomePathSecret { position: 11, path_secret: SECRET_AA, secret_len: 32, }, + }; + const v = validate_welcome_path_secrets(GROUP_ID_LOCAL, 6, 0, &secrets, GROUP_ID_LOCAL, 5, &REQUIRED_2); + assert(v.code == WelcomePathSecretCode.Ok); +} + +// **WPS-09** - the valid Welcome accepted: both required +// ancestors, fresh epoch, matching group. +test wps_09_valid_welcome_accepted { + const secrets: [2]WelcomePathSecret = [2]WelcomePathSecret{ + WelcomePathSecret { position: 3, path_secret: SECRET_33, secret_len: 32, }, + WelcomePathSecret { position: 7, path_secret: SECRET_77, secret_len: 32, }, + }; + const v = validate_welcome_path_secrets(GROUP_ID_LOCAL, 6, 0, &secrets, GROUP_ID_LOCAL, 5, &REQUIRED_2); + assert(v.code == WelcomePathSecretCode.Ok); +} + +// **WPS-10** - module green: an empty bundle against an empty +// requirement set validates clean - the original's green check +// on a live call. +test wps_10_module_green { + const secrets: [0]WelcomePathSecret = [0]WelcomePathSecret{}; + const none: [0]u32 = [0]u32{}; + const v = validate_welcome_path_secrets(GROUP_ID_LOCAL, 6, 0, &secrets, GROUP_ID_LOCAL, 5, &none); + assert(v.code == WelcomePathSecretCode.Ok); +} + +// The four helpers have direct tests (coverage: Untested 0). +test wps_helpers_answer { + assert(secrets_equal(SECRET_33, SECRET_33)); + assert(!secrets_equal(SECRET_33, SECRET_77)); + assert(group_ids_equal(GROUP_ID_LOCAL, GROUP_ID_LOCAL)); + assert(!group_ids_equal(GROUP_ID_LOCAL, GROUP_ID_HOSTILE)); + const pair: [2]WelcomePathSecret = [2]WelcomePathSecret{ + WelcomePathSecret { position: 3, path_secret: SECRET_33, secret_len: 32, }, + WelcomePathSecret { position: 3, path_secret: SECRET_33, secret_len: 32, }, + }; + assert(!secret_dup_at_other_position(&pair, 1)); + const cross: [2]WelcomePathSecret = [2]WelcomePathSecret{ + WelcomePathSecret { position: 3, path_secret: SECRET_33, secret_len: 32, }, + WelcomePathSecret { position: 7, path_secret: SECRET_33, secret_len: 32, }, + }; + assert(!secret_dup_at_other_position(&cross, 0)); + assert(secret_dup_at_other_position(&cross, 1)); + assert(position_delivered(&cross, 3)); + assert(position_delivered(&cross, 7)); + assert(!position_delivered(&cross, 11)); +} + +// Rule order is the original's: the secret lengths before the +// group id, the group id before the epoch, the epoch before the +// duplicate scan, the duplicate scan before the off-leaf check, +// the off-leaf check before the missing-ancestor scan - and a +// secret repeated at the same position re-inserts cleanly. +test rule_order_matches_original { + const short_hostile: [2]WelcomePathSecret = [2]WelcomePathSecret{ + WelcomePathSecret { position: 3, path_secret: SECRET_33, secret_len: 16, }, + WelcomePathSecret { position: 7, path_secret: SECRET_77, secret_len: 32, }, + }; + const v1 = validate_welcome_path_secrets(GROUP_ID_HOSTILE, 6, 0, &short_hostile, GROUP_ID_LOCAL, 5, &REQUIRED_2); + assert(v1.code == WelcomePathSecretCode.NonCanonicalSecretLength); + + const hostile_stale: [2]WelcomePathSecret = [2]WelcomePathSecret{ + WelcomePathSecret { position: 3, path_secret: SECRET_33, secret_len: 32, }, + WelcomePathSecret { position: 7, path_secret: SECRET_77, secret_len: 32, }, + }; + const v2 = validate_welcome_path_secrets(GROUP_ID_HOSTILE, 4, 0, &hostile_stale, GROUP_ID_LOCAL, 5, &REQUIRED_2); + assert(v2.code == WelcomePathSecretCode.CrossGroupWelcome); + + const stale_dup: [2]WelcomePathSecret = [2]WelcomePathSecret{ + WelcomePathSecret { position: 3, path_secret: SECRET_33, secret_len: 32, }, + WelcomePathSecret { position: 7, path_secret: SECRET_33, secret_len: 32, }, + }; + const v3 = validate_welcome_path_secrets(GROUP_ID_LOCAL, 4, 0, &stale_dup, GROUP_ID_LOCAL, 5, &REQUIRED_2); + assert(v3.code == WelcomePathSecretCode.StaleEpochWelcome); + + const dup_off_leaf: [2]WelcomePathSecret = [2]WelcomePathSecret{ + WelcomePathSecret { position: 3, path_secret: SECRET_33, secret_len: 32, }, + WelcomePathSecret { position: 7, path_secret: SECRET_33, secret_len: 32, }, + }; + const v4 = validate_welcome_path_secrets(GROUP_ID_LOCAL, 6, 3, &dup_off_leaf, GROUP_ID_LOCAL, 5, &REQUIRED_2); + assert(v4.code == WelcomePathSecretCode.DuplicatePathSecret); + + const off_leaf_missing: [1]WelcomePathSecret = [1]WelcomePathSecret{ + WelcomePathSecret { position: 3, path_secret: SECRET_33, secret_len: 32, }, + }; + const v5 = validate_welcome_path_secrets(GROUP_ID_LOCAL, 6, 3, &off_leaf_missing, GROUP_ID_LOCAL, 5, &REQUIRED_2); + assert(v5.code == WelcomePathSecretCode.OffLeafPathSecret); + + const re_insert: [3]WelcomePathSecret = [3]WelcomePathSecret{ + WelcomePathSecret { position: 3, path_secret: SECRET_33, secret_len: 32, }, + WelcomePathSecret { position: 3, path_secret: SECRET_33, secret_len: 32, }, + WelcomePathSecret { position: 7, path_secret: SECRET_77, secret_len: 32, }, + }; + const v6 = validate_welcome_path_secrets(GROUP_ID_LOCAL, 6, 0, &re_insert, GROUP_ID_LOCAL, 5, &REQUIRED_2); + assert(v6.code == WelcomePathSecretCode.Ok); +}