Skip to content

🌊 Wave-32: welcome_encrypted_group_info_aead + proposal_ref_collision#773

Open
gHashTag wants to merge 1 commit into
mainfrom
feat/trios-chat-wave32
Open

🌊 Wave-32: welcome_encrypted_group_info_aead + proposal_ref_collision#773
gHashTag wants to merge 1 commit into
mainfrom
feat/trios-chat-wave32

Conversation

@gHashTag
Copy link
Copy Markdown
Owner

@gHashTag gHashTag commented May 13, 2026

Closes #772

🌊 Wave-32 β€” welcome_encrypted_group_info_aead + proposal_ref_collision

Anchor: φ² + φ⁻² = 3

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

Lane summary

  • L-CHAT-1-wegi (R-CHAT-1 / CR-CHAT-01) β€” Welcome
    encrypted_group_info AEAD envelope: non-canonical nonce length,
    short ciphertext, cross-group, stale epoch, AEAD nonce reuse, and
    zero-nonce per RFC 9420 Β§12.4.3. Module
    crates/trios-chat/rings/CR-CHAT-01/src/welcome_encrypted_group_info_aead.rs
    (268 lines) with 6 rules NonCanonicalAeadNonceLength β†’
    ShortAeadCiphertext β†’ CrossGroupAeadEnvelope β†’
    StaleEpochAeadEnvelope β†’ ReusedAeadNonce β†’ ZeroAeadNonce.
    WEGI-01..10 (10 unit tests).
  • L-CHAT-3-pref (R-CHAT-11 / CR-CHAT-03) β€” ProposalRef collision:
    non-canonical length, empty id, unknown ref, cross-group, stale
    epoch, replay, zero-ref per RFC 9420 Β§12.1.1. Module
    crates/trios-chat/rings/CR-CHAT-03/src/proposal_ref_collision.rs
    (265 lines) with 7 rules NonCanonicalProposalRefLength β†’
    EmptyProposalId β†’ UnknownProposalRef β†’ CrossGroupProposalRef β†’
    StaleEpochProposalRef β†’ ProposalRefReplay β†’ ZeroProposalRef.
    PREF-01..10 (10 unit tests).
  • Falsifier corpus 3000 β†’ 3100 (+50 welcome_encrypted_group_info_aead
    • 50 proposal_ref_collision, IDs PI-WEGI-001..050 /
      PI-PREF-001..050). Offline-sim: 3100/3100 blocked, 0 misses,
      62 categories.
  • DENY_PATTERNS 5120 β†’ 5321 (+201 W32 patterns) under the
    // -- Wave-32: welcome-encrypted-group-info-aead + proposal-ref-collision --
    block in crates/trios-chat/rings/CR-CHAT-06/src/injection.rs.
    No closer patches were needed.
  • Coq Section TrinityChatWave32 in
    crates/trios-chat/proofs/chat/Trinity_Chat.v β€” 7 theorems
    INV-CHAT-194..200 + 4 helpers; cumulative Qed. 288 β†’ 299;
    0 admissions; 0 new axioms.
  • falsifier_runner: 2 new threshold lanes
    ("welcome_encrypted_group_info_aead", 0.95) and
    ("proposal_ref_collision", 0.95).
  • ROADMAP.md: status line W32, +2 anchor tokens, W31 row
    finalised with 756cf35 + PR 🌊 Wave-31: keypackage_init_key_reuse + external_psk_id_provenance #771, Wave-32 bold row + full
    detail section, INV mapping row INV-CHAT-194..200 W32, axiom
    summary extended through W32, future-waves shifted to W33..W37,
    W32 VERIFIED footer.

Theorems (proof-grade)

INV Lemma name
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.

Wave-32 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]: ~548 tests / 0 failures, 25/25 e2e,
3100/3100 falsifier (62 cats), clippy clean,
coqc silent (299 Qed / 0 Admitted).
13/13 CI checks green.

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

References

🌊 feat(trios-chat) Wave-32: welcome-encrypted-group-info-aead + propo…
6b5dc44 
…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 gHashTag added grandmaster Trinity-grandmaster orchestrated mission (paper+Coq+Rust+army) one-shot ONE SHOT mission issue trios-chat wave-32 labels May 13, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

grandmaster Trinity-grandmaster orchestrated mission (paper+Coq+Rust+army) one-shot ONE SHOT mission issue trios-chat wave-32

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

🌊 Wave-32 β€” welcome_encrypted_group_info_aead + proposal_ref_collision (sub-tracker)

1 participant

@gHashTag