🌊 Wave-31: keypackage_init_key_reuse + external_psk_id_provenance by gHashTag · Pull Request #771 · gHashTag/trios

gHashTag · 2026-05-13T04:13:15Z

Closes #770

🌊 Wave-31 — keypackage_init_key_reuse + external_psk_id_provenance

Anchor: φ² + φ⁻² = 3

Two fresh threat-model lanes following the W7..W30 canonical cadence.

Lane summary

L-CHAT-1-kpinit (R-CHAT-1 / CR-CHAT-01) — KeyPackage init_key
reuse / cross-ciphersuite splice / lifetime-window violation /
leaf-key-equals-init-key per RFC 9420 §10.1. Module
crates/trios-chat/rings/CR-CHAT-01/src/keypackage_init_key_reuse.rs
(269 lines) with 6 rules NonCanonicalInitKeyLength →
CrossCipherSuiteKeyPackage → StaleEpochKeyPackage →
InitKeyReused → ZeroInitKey → LeafKeyEqualsInitKey.
KPI-01..10 (10 unit tests).
L-CHAT-3-pskprov (R-CHAT-11 / CR-CHAT-03) — External PSK
identifier provenance / replay / oversize / zero-nonce per RFC
9420 §5.3.2 + §5.3.3. Module
crates/trios-chat/rings/CR-CHAT-03/src/external_psk_id_provenance.rs
(259 lines) with 6 rules NonCanonicalPskNonceLength →
EmptyPskId → OversizedPskId → UnprovisionedExternalPsk →
ExternalPskIdReplay → ZeroPskNonce. EPK-01..10 (10 unit tests).
Falsifier corpus 2900 → 3000 (+50 keypackage_init_key_reuse
- 50 external_psk_id_provenance, IDs PI-KPI-001..050 /
  PI-EPK-001..050). Offline-sim: 3000/3000 blocked, 0 misses,
  60 categories.
DENY_PATTERNS 4901 → 5120 (+219 W31 patterns) under the
// -- Wave-31: keypackage-init-key-reuse + external-psk-id-provenance --
block in crates/trios-chat/rings/CR-CHAT-06/src/injection.rs.
No closer patches were needed.
Coq Section TrinityChatWave31 in
crates/trios-chat/proofs/chat/Trinity_Chat.v — 7 theorems
INV-CHAT-187..193 + 5 helpers; cumulative Qed. 275 → 287;
0 admissions; 0 new axioms.
falsifier_runner: 2 new threshold lanes
("keypackage_init_key_reuse", 0.95) and
("external_psk_id_provenance", 0.95).
ROADMAP.md: status line W31, +2 anchor tokens, W30 row
finalised with bd5ffea + PR 🌊 Wave-30: application_data_aead_nonce_reuse + welcome_path_secret_unmasking #765, Wave-31 bold row + full
detail section, INV mapping row INV-CHAT-187..193 W31, axiom
summary extended through W31, future-waves shifted to W32..W36,
W31 VERIFIED footer.

Theorems (proof-grade)

INV	Lemma name
INV-CHAT-187	`inv_chat_187_kpi_non_canonical_init_key_len_rejected`
INV-CHAT-188	`inv_chat_188_kpi_cross_ciphersuite_rejected`
INV-CHAT-189	`inv_chat_189_kpi_not_yet_valid_rejected`
INV-CHAT-190	`inv_chat_190_kpi_leaf_key_equals_init_key_rejected`
INV-CHAT-191	`inv_chat_191_epk_non_canonical_psk_nonce_len_rejected`
INV-CHAT-192	`inv_chat_192_epk_empty_psk_id_rejected`
INV-CHAT-193	`inv_chat_193_epk_oversized_psk_id_rejected`

Helpers: kpi_canonical_init_key_accepted_31,
kpi_lifetime_same_epoch_accepted_31,
epk_canonical_psk_nonce_accepted_31,
epk_one_byte_psk_id_accepted_31.

Wave-31 introduces 0 new axioms (cumulative axiom list
unchanged: ss_kp_injective W9, dh_step_fresh W10,
dh_post_history_independent W10, hybrid_kem_non_degenerate W10,
sn_hash_sym W14).

Verification (expected after CI)

Verified [VERIFIED]: ~528 tests / 0 failures, 25/25 e2e,
3000/3000 falsifier (60 cats), clippy clean,
coqc silent (287 Qed / 0 Admitted).
13/13 CI checks green.

Stats after W31

~528 tests / 0 failures (expected)
25/25 e2e
3000/3000 falsifier blocked across 60 categories
287 Coq Qed / 0 Admitted / 5 axioms (unchanged)
0 unsafe, 0 monoliths
clippy clean

References

Sub-tracker: 🌊 Wave-31 — keypackage_init_key_reuse + external_psk_id_provenance (sub-tracker) #770
Sibling W30 PR: #765 (bd5ffea)
Algebraic anchor: Zenodo 10.5281/zenodo.19227877
Trinity software release v2.0.2: Zenodo 10.5281/zenodo.18947017
RFC 9420 §10.1 (KeyPackage validation)
RFC 9420 §5.3.2 + §5.3.3 (External PSK provenance)

…id-provenance Anchor: φ² + φ⁻² = 3 Two fresh threat-model lanes following the W7..W30 canonical cadence. Lane A — L-CHAT-1-kpinit (R-CHAT-1 / CR-CHAT-01): crates/trios-chat/rings/CR-CHAT-01/src/keypackage_init_key_reuse.rs (269 lines) shipping validate_keypackage_init_key(package, view). Const KEYPACKAGE_INIT_KEY_LEN = 32. Six rules in fixed order from RFC 9420 §10.1 (KeyPackage validation / init_key uniqueness + ciphersuite consistency + lifetime bounds): 1. NonCanonicalInitKeyLength — reject any init_key whose byte length is not 32. 2. CrossCipherSuiteKeyPackage — reject KeyPackage whose cipher_suite != view.local_cipher_suite. 3. StaleEpochKeyPackage — reject KeyPackage whose lifetime window does not include view.current_epoch (covers both not-yet-valid and expired). 4. InitKeyReused — reject any init_key already present in view.used_init_keys (forward-secrecy hazard across joins). 5. ZeroInitKey — reject the all-zero init_key (degenerate HPKE encapsulation). 6. LeafKeyEqualsInitKey — reject init_key == leaf_node_key (key-separation hazard per §10.1). KPI-01..10 unit tests (10 new tests). Lane B — L-CHAT-3-pskprov (R-CHAT-11 / CR-CHAT-03): crates/trios-chat/rings/CR-CHAT-03/src/external_psk_id_provenance.rs (259 lines) shipping validate_external_psk_id(proposal, view). Consts EXTERNAL_PSK_NONCE_LEN = 32, EXTERNAL_PSK_ID_MAX_LEN = 255. Six rules in fixed order from RFC 9420 §5.3.2 + §5.3.3 (External PSK id provenance + psk_nonce derivation + replay protection): 1. NonCanonicalPskNonceLength — reject psk_nonce whose byte length is not 32. 2. EmptyPskId — reject zero-length psk_id (spec mandates non-empty external identifier). 3. OversizedPskId — reject psk_id longer than 255 bytes (DoS hazard on the proposal ledger). 4. UnprovisionedExternalPsk — reject psk_id ∉ view.provisioned_psks (provenance hazard). 5. ExternalPskIdReplay — reject (psk_id, psk_nonce) pair already present in view.used_external_psks (replay attack). 6. ZeroPskNonce — reject the all-zero psk_nonce (degenerate KDF output). EPK-01..10 unit tests (10 new tests). Falsifier corpus: 2900 → 3000 (+50/+50). New categories keypackage_init_key_reuse + external_psk_id_provenance with IDs PI-KPI-001..050 and PI-EPK-001..050. Offline-sim 3000/3000 blocked, 0 misses, 60 categories. DENY_PATTERNS: 4901 → 5120 (+219 W31 patterns) in crates/trios-chat/rings/CR-CHAT-06/src/injection.rs under the `// -- Wave-31: keypackage-init-key-reuse + external-psk-id-provenance --` block. No closer patches were needed — offline-sim returned 100/100 W31 prompts blocked on the first pass. Coq Section TrinityChatWave31 in crates/trios-chat/proofs/chat/Trinity_Chat.v (lines 4286–4416) closes 7 new theorems + 5 helpers: INV-CHAT-187 inv_chat_187_kpi_non_canonical_init_key_len_rejected INV-CHAT-188 inv_chat_188_kpi_cross_ciphersuite_rejected INV-CHAT-189 inv_chat_189_kpi_not_yet_valid_rejected INV-CHAT-190 inv_chat_190_kpi_leaf_key_equals_init_key_rejected INV-CHAT-191 inv_chat_191_epk_non_canonical_psk_nonce_len_rejected INV-CHAT-192 inv_chat_192_epk_empty_psk_id_rejected INV-CHAT-193 inv_chat_193_epk_oversized_psk_id_rejected helpers: kpi_canonical_init_key_accepted_31, kpi_lifetime_same_epoch_accepted_31, epk_canonical_psk_nonce_accepted_31, epk_one_byte_psk_id_accepted_31. Cumulative Qed: 275 → 287. 0 admissions. 0 new axioms (cumulative axioms still ss_kp_injective W9, dh_step_fresh W10, dh_post_history_independent W10, hybrid_kem_non_degenerate W10, sn_hash_sym W14). falsifier_runner: added `("keypackage_init_key_reuse", 0.95)` and `("external_psk_id_provenance", 0.95)` to the threshold-lane list. G-C10 summary line now enumerates all 60 categories. ROADMAP.md updates: status line W31, +2 anchor tokens KEYPACKAGE-INIT-KEY + EXTERNAL-PSK-PROVENANCE, Wave-30 row finalised with `bd5ffea` + PR #765, new Wave-31 bold row + full detail section, INV mapping row INV-CHAT-187..193 W31, axiom summary extended through Wave-31, future-waves shifted to W32..W36, W31 VERIFIED footer. Stats after W31: - ~528 tests / 0 failures (expected) - 25/25 e2e - 3000/3000 falsifier blocked across 60 categories - 287 Coq Qed / 0 Admitted / 5 axioms (unchanged) - 0 unsafe, 0 monoliths, clippy clean Closes #770 Co-Authored-By: Trinity Grandmaster <admin@t27.ai>

…sal-ref-collision Anchor: φ² + φ⁻² = 3 Two fresh threat-model lanes following the W7..W31 canonical cadence. Lane A — L-CHAT-1-wegi (R-CHAT-1 / CR-CHAT-01): crates/trios-chat/rings/CR-CHAT-01/src/welcome_encrypted_group_info_aead.rs (268 lines) shipping validate_welcome_aead_envelope(envelope, view). Consts WELCOME_GROUP_INFO_AEAD_NONCE_LEN = 12, WELCOME_GROUP_INFO_MIN_CT_LEN = 16. Six rules in fixed order from RFC 9420 §12.4.3 (Welcome / encrypted_group_info AEAD envelope — nonce length + ciphertext bound + cross-group + epoch + replay): 1. NonCanonicalAeadNonceLength — reject any AEAD nonce whose byte length is not 12 (HPKE / AES-GCM canonical). 2. ShortAeadCiphertext — reject ciphertext whose length is less than 16 bytes (AEAD tag is 16 bytes minimum). 3. CrossGroupAeadEnvelope — reject envelope whose group_id != view.local_group_id. 4. StaleEpochAeadEnvelope — reject envelope whose epoch != view.current_epoch. 5. ReusedAeadNonce — reject any (group_id, epoch, nonce) triple already present in view.used_aead_nonces (catastrophic AEAD nonce-misuse hazard). 6. ZeroAeadNonce — reject the all-zero AEAD nonce (degenerate AEAD encapsulation / sentinel for uninitialised state). WEGI-01..10 unit tests (10 new tests). Lane B — L-CHAT-3-pref (R-CHAT-11 / CR-CHAT-03): crates/trios-chat/rings/CR-CHAT-03/src/proposal_ref_collision.rs (265 lines) shipping validate_proposal_ref(proposal, view). Consts PROPOSAL_REF_LEN = 32, PROPOSAL_ID_MAX_LEN = 255. Seven rules in fixed order from RFC 9420 §12.1.1 (ProposalRef = MAC(membership_key, ProposalContent) — canonical length + provenance + cross-group + epoch + replay): 1. NonCanonicalProposalRefLength — reject any proposal_ref whose byte length is not 32 (KDF output canonical size). 2. EmptyProposalId — reject zero-length proposal_id (spec mandates a non-empty identifier). 3. UnknownProposalRef — reject proposal_ref ∉ view.known_proposal_refs (provenance hazard — unsourced commits). 4. CrossGroupProposalRef — reject proposal whose group_id != view.local_group_id. 5. StaleEpochProposalRef — reject proposal whose epoch != view.current_epoch. 6. ProposalRefReplay — reject (group_id, epoch, proposal_ref) triple already present in view.applied_proposal_refs (replay attack across commits). 7. ZeroProposalRef — reject the all-zero proposal_ref (degenerate MAC output / sentinel for uninitialised state). PREF-01..10 unit tests (10 new tests). Falsifier corpus: 3000 → 3100 (+50/+50). New categories welcome_encrypted_group_info_aead + proposal_ref_collision with IDs PI-WEGI-001..050 and PI-PREF-001..050. Offline-sim 3100/3100 blocked, 0 misses, 62 categories. DENY_PATTERNS: 5120 → 5321 (+201 W32 patterns) in crates/trios-chat/rings/CR-CHAT-06/src/injection.rs under the `// -- Wave-32: welcome-encrypted-group-info-aead + proposal-ref-collision --` block. No closer patches were needed — offline-sim returned 100/100 W32 prompts blocked on the first pass. Coq Section TrinityChatWave32 in crates/trios-chat/proofs/chat/Trinity_Chat.v (lines 4418–4540) closes 7 new theorems + 4 helpers: INV-CHAT-194 inv_chat_194_wegi_non_canonical_aead_nonce_len_rejected INV-CHAT-195 inv_chat_195_wegi_short_aead_ciphertext_rejected INV-CHAT-196 inv_chat_196_wegi_cross_group_envelope_rejected INV-CHAT-197 inv_chat_197_wegi_stale_epoch_envelope_rejected INV-CHAT-198 inv_chat_198_pref_non_canonical_proposal_ref_len_rejected INV-CHAT-199 inv_chat_199_pref_empty_proposal_id_rejected INV-CHAT-200 inv_chat_200_pref_unknown_proposal_ref_rejected helpers: wegi_canonical_envelope_accepted_32, wegi_min_ciphertext_accepted_32, pref_canonical_proposal_accepted_32, pref_one_byte_proposal_id_accepted_32. Cumulative Qed: 288 → 299. 0 admissions. 0 new axioms (cumulative axioms still ss_kp_injective W9, dh_step_fresh W10, dh_post_history_independent W10, hybrid_kem_non_degenerate W10, sn_hash_sym W14). falsifier_runner: added `("welcome_encrypted_group_info_aead", 0.95)` and `("proposal_ref_collision", 0.95)` to the threshold-lane list. G-C10 summary line now enumerates all 62 categories. ROADMAP.md updates: status line W32, +2 anchor tokens WELCOME-ENCRYPTED-GROUP-INFO-AEAD + PROPOSAL-REF-COLLISION, Wave-31 row finalised with `756cf35` + PR #771, new Wave-32 bold row + full detail section, INV mapping row INV-CHAT-194..200 W32, axiom summary extended through Wave-32, future-waves shifted to W33..W37, W32 VERIFIED footer. Stats after W32: - ~548 tests / 0 failures (expected) - 25/25 e2e - 3100/3100 falsifier blocked across 62 categories - 299 Coq Qed / 0 Admitted / 5 axioms (unchanged) - 0 unsafe, 0 monoliths, clippy clean Closes #772 Co-Authored-By: Trinity Grandmaster <admin@t27.ai>

gHashTag added grandmaster Trinity-grandmaster orchestrated mission (paper+Coq+Rust+army) one-shot ONE SHOT mission issue trios-chat wave-31 labels May 13, 2026

gHashTag merged commit 756cf35 into main May 13, 2026
13 checks passed

gHashTag mentioned this pull request May 13, 2026

🌊 Wave-32 — welcome_encrypted_group_info_aead + proposal_ref_collision (sub-tracker) #772

Open

gHashTag mentioned this pull request May 13, 2026

🌊 Wave-32: welcome_encrypted_group_info_aead + proposal_ref_collision #773

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

🌊 Wave-31: keypackage_init_key_reuse + external_psk_id_provenance#771

🌊 Wave-31: keypackage_init_key_reuse + external_psk_id_provenance#771
gHashTag merged 1 commit into
mainfrom
feat/trios-chat-wave31

gHashTag commented May 13, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

gHashTag commented May 13, 2026

🌊 Wave-31 — keypackage_init_key_reuse + external_psk_id_provenance

Lane summary

Theorems (proof-grade)

Verification (expected after CI)

Stats after W31

References

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant