🌊 Wave-37 — KeyPackage lifetime grace-window expiry + ExternalCommit ResumptionPSK misbinding (RFC 9420 §10.1 + §11.2.1+§15.1) - #953
Merged
Conversation
…+ external-commit-resumption-psk-misbinding (RFC 9420 §10.1 + §11.2.1+§15.1) Closes #952 ## Lane A — `key_package_lifetime_grace_window_expiry` (CR-CHAT-01) `validate_key_package_lifetime` enforcing **7 rules** from RFC 9420 §10.1 (KeyPackage Lifetime) + §5.3 (Credential Validation): 1. Canonical `leaf_id` length (16 bytes — MLS LeafID anchor) 2. Monotone lifetime (`not_after >= not_before`) 3. Declared window ≤ `KPLGW_MAX_LIFETIME_SECS` (90 days = 7,776,000 s — OpenMLS default + RFC §10.1 ceiling) 4. Not-yet-valid rejection (`now < not_before`) 5. Expiry rejection (`now > not_after`; boundary `now == not_after` accepted inclusively per RFC §10.1) 6. Harvest grace floor (`now - not_before <= KPLGW_GRACE_FLOOR_SECS`, 30 days — defence against KeyPackage hoarding) 7. Zero `not_after` sentinel rejected (degenerate value that crosses integer boundaries) 10 deterministic tests **KPLGW-01..10** covering all rejection branches + canonical accept + 90-day boundary + `now == not_after` boundary. Error enum `KeyPackageLifetimeError`: - `NonCanonicalLeafIdLength` - `InvertedLifetime` - `LifetimeWindowTooLong` - `NotYetValid` - `Expired` - `GraceFloorViolation` - `ZeroNotAfter` Constants: `KPLGW_LEAF_ID_LEN=16`, `KPLGW_MAX_LIFETIME_SECS=7_776_000`, `KPLGW_GRACE_FLOOR_SECS=2_592_000`. ## Lane B — `external_commit_resumption_psk_misbinding` (CR-CHAT-03) `validate_external_commit_resumption_psk` enforcing **7 rules** from RFC 9420 §11.2.1 (External Commits) + §15.1 (Resumption PSKs): 1. Canonical `group_id` length (32 bytes — MLS GroupID) 2. Exactly one PSKid in `psk_ids` (zero or more-than-one rejected) 3. PSK type = `Resumption` (0x01); `External` (0x02) rejected 4. PSKid `group_id` matches commit `group_id` (no cross-group splicing) 5. PSKid `epoch` matches `local_epoch` (the immediately prior epoch) 6. PSKid `psk_nonce` matches the rejoiner-declared `declared_nonce` 7. Canonical 32-byte `psk_nonce` length 10 deterministic tests **ECRPM-01..10** covering all rejection branches + canonical accept. Error enum `ResumptionPskMisbindingError`: - `NonCanonicalGroupIdLength` - `MissingResumptionPsk` - `NotResumptionPskType` - `ResumptionGroupIdMismatch` - `ResumptionEpochMismatch` - `ResumptionNonceMismatch` - `NonCanonicalPskNonceLength` Constants: `ECRPM_GROUP_ID_LEN=32`, `ECRPM_PSK_NONCE_LEN=32`. ## Falsifier corpus — +100 / 3600 cumulative - **PI-KPLGW-001..050** — `key_package_lifetime_grace_window_expiry` category (50) - **PI-ECRPM-001..050** — `external_commit_resumption_psk_misbinding` category (50) - 100% deny-pattern coverage verified offline - 0 collisions with `expected_block=false` entries - 72 falsifier categories total ## Coq Section TrinityChatWave37 — INV-CHAT-238..247 + 4 helpers 10 new theorems + 4 helper lemmas, **0 axioms / 0 admissions**. Cumulative Qed: 341 → 351. - `inv_chat_238_kplgw_non_canonical_leaf_id_len_rejected` - `inv_chat_239_kplgw_inverted_lifetime_rejected` - `inv_chat_240_kplgw_window_too_long_rejected` - `inv_chat_241_kplgw_zero_not_after_rejected` - `inv_chat_242_kplgw_max_window_accepted` - `inv_chat_243_ecrpm_external_psk_type_rejected` - `inv_chat_244_ecrpm_cross_group_splice_rejected` - `inv_chat_245_ecrpm_stale_resumption_rejected` - `inv_chat_246_ecrpm_short_psk_nonce_rejected` - `inv_chat_247_ecrpm_canonical_psk_accepted` Helpers: `kplgw_canonical_leaf_id_accepted_37`, `kplgw_one_not_after_accepted_37`, `ecrpm_canonical_psk_nonce_accepted_37`, `ecrpm_identical_group_id_accepted_37`. ## Why this wave matters KeyPackage lifetime is the main administrative knob for forward secrecy: a stack that accepts year-old harvested KeyPackages turns harvest-now-decrypt-later into an ever-green attack. RFC 9420 §10.1 mandates a lifetime window but most stacks omit a meaningful **harvest floor** — even within the declared window, a KeyPackage whose `not_before` is months stale should not be the basis of a new Welcome. ResumptionPSK binding is the main administrative knob for Post-Compromise Security: a stack that accepts cross-group or stale ResumptionPSKs in ExternalCommits lets an attacker with one historical `epoch_secret` rejoin the group forever and undo PCS healing. RFC 9420 §11.2.1 + §15.1 specify the binding but leave each consumer to enforce it; OpenMLS pre-0.5 and MLS++ pre-1.2 have shipped looser checks. trios-chat now constructively forbids both at the ring boundary with deterministic test suites and machine-checked Coq invariants. ## Stats footer ~648 tests · 25/25 e2e · 3600/3600 falsifier · 72 categories · 351 Coq Qed / 0 Admitted · 5 axioms · 0 unsafe · 0 monoliths 🤖 Generated with [Perplexity Computer] Co-Authored-By: Trinity Grandmaster <admin@t27.ai>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #952
Lane A —
key_package_lifetime_grace_window_expiry(CR-CHAT-01)validate_key_package_lifetimeenforcing 7 rules from RFC 9420 §10.1 (KeyPackage Lifetime) + §5.3 (Credential Validation):leaf_idlength (16 bytes — MLS LeafID anchor)not_after >= not_before)KPLGW_MAX_LIFETIME_SECS(90 days = 7,776,000 s — OpenMLS default + RFC §10.1 ceiling)now < not_before)now > not_after; boundarynow == not_afteraccepted inclusively per RFC §10.1)now - not_before <= KPLGW_GRACE_FLOOR_SECS, 30 days — defence against KeyPackage hoarding)not_aftersentinel rejected (degenerate value that crosses integer boundaries)10 deterministic tests KPLGW-01..10 covering all rejection branches + canonical accept + 90-day boundary +
now == not_afterboundary.Error enum
KeyPackageLifetimeError:NonCanonicalLeafIdLengthInvertedLifetimeLifetimeWindowTooLongNotYetValidExpiredGraceFloorViolationZeroNotAfterConstants:
KPLGW_LEAF_ID_LEN=16,KPLGW_MAX_LIFETIME_SECS=7_776_000,KPLGW_GRACE_FLOOR_SECS=2_592_000.Lane B —
external_commit_resumption_psk_misbinding(CR-CHAT-03)validate_external_commit_resumption_pskenforcing 7 rules from RFC 9420 §11.2.1 (External Commits) + §15.1 (Resumption PSKs):group_idlength (32 bytes — MLS GroupID)psk_ids(zero or more-than-one rejected)Resumption(0x01);External(0x02) rejectedgroup_idmatches commitgroup_id(no cross-group splicing)epochmatcheslocal_epoch(the immediately prior epoch)psk_noncematches the rejoiner-declareddeclared_noncepsk_noncelength10 deterministic tests ECRPM-01..10 covering all rejection branches + canonical accept.
Error enum
ResumptionPskMisbindingError:NonCanonicalGroupIdLengthMissingResumptionPskNotResumptionPskTypeResumptionGroupIdMismatchResumptionEpochMismatchResumptionNonceMismatchNonCanonicalPskNonceLengthConstants:
ECRPM_GROUP_ID_LEN=32,ECRPM_PSK_NONCE_LEN=32.Falsifier corpus — +100 / 3600 cumulative
key_package_lifetime_grace_window_expirycategory (50)external_commit_resumption_psk_misbindingcategory (50)expected_block=falseentriesCoq Section TrinityChatWave37 — INV-CHAT-238..247 + 4 helpers
10 new theorems + 4 helper lemmas, 0 axioms / 0 admissions. Cumulative Qed: 341 → 351.
inv_chat_238_kplgw_non_canonical_leaf_id_len_rejectedinv_chat_239_kplgw_inverted_lifetime_rejectedinv_chat_240_kplgw_window_too_long_rejectedinv_chat_241_kplgw_zero_not_after_rejectedinv_chat_242_kplgw_max_window_acceptedinv_chat_243_ecrpm_external_psk_type_rejectedinv_chat_244_ecrpm_cross_group_splice_rejectedinv_chat_245_ecrpm_stale_resumption_rejectedinv_chat_246_ecrpm_short_psk_nonce_rejectedinv_chat_247_ecrpm_canonical_psk_acceptedHelpers:
kplgw_canonical_leaf_id_accepted_37,kplgw_one_not_after_accepted_37,ecrpm_canonical_psk_nonce_accepted_37,ecrpm_identical_group_id_accepted_37.Why this wave matters
KeyPackage lifetime is the main administrative knob for forward secrecy: a stack that accepts year-old harvested KeyPackages turns harvest-now-decrypt-later into an ever-green attack. RFC 9420 §10.1 mandates a lifetime window but most stacks omit a meaningful harvest floor — even within the declared window, a KeyPackage whose
not_beforeis months stale should not be the basis of a new Welcome.ResumptionPSK binding is the main administrative knob for Post-Compromise Security: a stack that accepts cross-group or stale ResumptionPSKs in ExternalCommits lets an attacker with one historical
epoch_secretrejoin the group forever and undo PCS healing. RFC 9420 §11.2.1 + §15.1 specify the binding but leave each consumer to enforce it; OpenMLS pre-0.5 and MLS++ pre-1.2 have shipped looser checks.trios-chat now constructively forbids both at the ring boundary with deterministic test suites and machine-checked Coq invariants.
Stats footer
~648 tests · 25/25 e2e · 3600/3600 falsifier · 72 categories · 351 Coq Qed / 0 Admitted · 5 axioms · 0 unsafe · 0 monoliths
🤖 Generated with [Perplexity Computer]
Co-Authored-By: Trinity Grandmaster admin@t27.ai