🌊 Wave-38 — sub-tracker
Direction: Welcome init-secret KDF label confusion + PSK secret extraction chain order mismatch.
RFC anchors: RFC 9420 §8.4 (Key Schedule / ExpandWithLabel) + §9.2 (Welcome Messages) + §15.1.1 (Computing the PSK Secret).
Lane A — welcome_init_secret_kdf_label_confusion (CR-CHAT-02)
Constructive guard at the joiner against KDF label confusion in the init_secret derivation. Per RFC 9420 §8.4:
init_secret = ExpandWithLabel(epoch_secret, "init", "", KDF.Nh)
The literal 4-byte ASCII string "init" is mandatory. Loose stacks have been caught using "INIT", "Init", "epoch", "init\0", UTF-8 homoglyph variants, or skipping ExpandWithLabel entirely. Result: silent two-party key divergence — every application packet decrypts to garbage and the failure mode masquerades as "decryption error" without any obvious attribution.
trios-chat enforces 6 rules: canonical 4-byte label length, every label byte in printable ASCII range 0x20..=0x7e, byte-for-byte equality with b"init", canonical 32-byte epoch_secret length, empty context (per RFC §8.4), canonical 32-byte declared output length.
Tests WISKLC-01..10. Error enum InitSecretKdfLabelError.
Constants: WISKLC_INIT_LABEL = b"init", WISKLC_KDF_NH = 32.
Lane B — psk_secret_extraction_chain_order_mismatch (CR-CHAT-05)
Constructive guard at the receiver against PSK chain reorder attacks. Per RFC 9420 §15.1.1, the psk_secret derivation is order-sensitive: PSKLabel(i, n) encodes both position i and total count n, so reordering psk_ids, swapping label.count, or duplicating PSKids all produce a different psk_secret. Loose stacks have been caught sorting psk_ids by hash, accepting duplicates, accepting PSKLabel.count != psk_ids.len(), or accepting non-monotonic indices — any one yielding a covert DoS where two endpoints derive divergent secrets.
trios-chat enforces 7 rules: canonical 32-byte PSKid length, non-empty list, list length ≤ 8 (OpenMLS cap), label.count == list.len(), label.index < label.count, label.index == position (strict monotonic), and no duplicate PSKids.
Tests PSCOM-01..10. Error enum PskChainOrderError.
Constants: PSCOM_PSKID_LEN = 32, PSCOM_MAX_PSK_COUNT = 8.
Coq Section TrinityChatWave38
10 new theorems INV-CHAT-248..257 + 4 helper lemmas, 0 new axioms / 0 admissions. Cumulative Qed: 351 → 361.
| Lane |
INV |
Theorem |
| WISKLC |
248 |
inv_chat_248_wisklc_non_canonical_label_len_rejected |
| WISKLC |
249 |
inv_chat_249_wisklc_non_printable_label_byte_rejected |
| WISKLC |
250 |
inv_chat_250_wisklc_non_canonical_epoch_secret_len_rejected |
| WISKLC |
251 |
inv_chat_251_wisklc_non_empty_context_rejected |
| WISKLC |
252 |
inv_chat_252_wisklc_canonical_output_len_accepted |
| PSCOM |
253 |
inv_chat_253_pscom_empty_list_rejected |
| PSCOM |
254 |
inv_chat_254_pscom_list_too_long_rejected |
| PSCOM |
255 |
inv_chat_255_pscom_label_count_desync_rejected |
| PSCOM |
256 |
inv_chat_256_pscom_index_not_monotonic_rejected |
| PSCOM |
257 |
inv_chat_257_pscom_singleton_accepted |
Falsifier corpus
+100 entries: PI-WISKLC-001..050 (welcome_init_secret_kdf_label_confusion) + PI-PSCOM-001..050 (psk_secret_extraction_chain_order_mismatch). Cumulative: 3600 → 3700/3700, 72 → 74 categories. 100% deny-pattern coverage; 0 collisions with expected_block=false.
Why this wave matters
KDF label binding is the single thinnest layer protecting MLS from cross-implementation key divergence: the entire epoch keying tree hangs off a 4-byte ASCII string, and most stacks treat this string as opaque. RFC 9420 §8.4 hard-codes the exact byte sequence; trios-chat checks it constructively before any keys are derived.
PSK chain order is the equivalent for multi-PSK Commits/Welcomes: an attacker who can dictate either side's psk_ids ordering or label encoding forces silent key divergence. Most stacks today ship one or more of: alphabetical-by-hash sort, count-mismatch tolerance, or duplicate PSKid acceptance. trios-chat now refuses all such inputs at the ring boundary.
Stats footer
~668 tests · 25/25 e2e · 3700/3700 falsifier · 74 categories · 361 Coq Qed / 0 Admitted · 5 axioms · 0 unsafe · 0 monoliths
Definition of done
🌊 Wave-38 — sub-tracker
Direction: Welcome init-secret KDF label confusion + PSK secret extraction chain order mismatch.
RFC anchors: RFC 9420 §8.4 (Key Schedule / ExpandWithLabel) + §9.2 (Welcome Messages) + §15.1.1 (Computing the PSK Secret).
Lane A —
welcome_init_secret_kdf_label_confusion(CR-CHAT-02)Constructive guard at the joiner against KDF label confusion in the
init_secretderivation. Per RFC 9420 §8.4:The literal 4-byte ASCII string
"init"is mandatory. Loose stacks have been caught using"INIT","Init","epoch","init\0", UTF-8 homoglyph variants, or skipping ExpandWithLabel entirely. Result: silent two-party key divergence — every application packet decrypts to garbage and the failure mode masquerades as "decryption error" without any obvious attribution.trios-chat enforces 6 rules: canonical 4-byte label length, every label byte in printable ASCII range
0x20..=0x7e, byte-for-byte equality withb"init", canonical 32-byte epoch_secret length, empty context (per RFC §8.4), canonical 32-byte declared output length.Tests WISKLC-01..10. Error enum
InitSecretKdfLabelError.Constants:
WISKLC_INIT_LABEL = b"init",WISKLC_KDF_NH = 32.Lane B —
psk_secret_extraction_chain_order_mismatch(CR-CHAT-05)Constructive guard at the receiver against PSK chain reorder attacks. Per RFC 9420 §15.1.1, the
psk_secretderivation is order-sensitive:PSKLabel(i, n)encodes both positioniand total countn, so reorderingpsk_ids, swapping label.count, or duplicating PSKids all produce a differentpsk_secret. Loose stacks have been caught sortingpsk_idsby hash, accepting duplicates, acceptingPSKLabel.count != psk_ids.len(), or accepting non-monotonic indices — any one yielding a covert DoS where two endpoints derive divergent secrets.trios-chat enforces 7 rules: canonical 32-byte PSKid length, non-empty list, list length ≤ 8 (OpenMLS cap),
label.count == list.len(),label.index < label.count,label.index == position(strict monotonic), and no duplicate PSKids.Tests PSCOM-01..10. Error enum
PskChainOrderError.Constants:
PSCOM_PSKID_LEN = 32,PSCOM_MAX_PSK_COUNT = 8.Coq Section TrinityChatWave38
10 new theorems INV-CHAT-248..257 + 4 helper lemmas, 0 new axioms / 0 admissions. Cumulative Qed: 351 → 361.
inv_chat_248_wisklc_non_canonical_label_len_rejectedinv_chat_249_wisklc_non_printable_label_byte_rejectedinv_chat_250_wisklc_non_canonical_epoch_secret_len_rejectedinv_chat_251_wisklc_non_empty_context_rejectedinv_chat_252_wisklc_canonical_output_len_acceptedinv_chat_253_pscom_empty_list_rejectedinv_chat_254_pscom_list_too_long_rejectedinv_chat_255_pscom_label_count_desync_rejectedinv_chat_256_pscom_index_not_monotonic_rejectedinv_chat_257_pscom_singleton_acceptedFalsifier corpus
+100 entries: PI-WISKLC-001..050 (
welcome_init_secret_kdf_label_confusion) + PI-PSCOM-001..050 (psk_secret_extraction_chain_order_mismatch). Cumulative: 3600 → 3700/3700, 72 → 74 categories. 100% deny-pattern coverage; 0 collisions withexpected_block=false.Why this wave matters
KDF label binding is the single thinnest layer protecting MLS from cross-implementation key divergence: the entire epoch keying tree hangs off a 4-byte ASCII string, and most stacks treat this string as opaque. RFC 9420 §8.4 hard-codes the exact byte sequence; trios-chat checks it constructively before any keys are derived.
PSK chain order is the equivalent for multi-PSK Commits/Welcomes: an attacker who can dictate either side's
psk_idsordering or label encoding forces silent key divergence. Most stacks today ship one or more of: alphabetical-by-hash sort, count-mismatch tolerance, or duplicate PSKid acceptance. trios-chat now refuses all such inputs at the ring boundary.Stats footer
~668 tests · 25/25 e2e · 3700/3700 falsifier · 74 categories · 361 Coq Qed / 0 Admitted · 5 axioms · 0 unsafe · 0 monolithsDefinition of done