spec(port): port the welcome path_secret unmasking defense (Refs #8884)

.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"
+  }
+}

docs/reports/t27b_expectations.json

@@ -901,6 +901,7 @@
   {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_length_distribution_guard.t27", "t27b": "pass"},
   {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_oracle_timing_sidechannel.t27", "t27b": "pass"},
   {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/safety_number.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/blind_signature_sender_token.t27", "t27b": "pass"},
   {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-07/src/cover_decoy_ratio_governor.t27", "t27b": "pass"},

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<u8> 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);
+}