Nonce Uniqueness

Given:

• Nonce construction: nonce = IV ⊕ (epoch_id || seq)
• IV is a fixed 12-byte value per direction per epoch (derived from key schedule)
• epoch_id is a 32-bit unsigned integer (4 bytes)
• seq is a 64-bit unsigned integer (8 bytes)
• (epoch_id || seq) denotes concatenation: 4 bytes epoch_id followed by 8 bytes seq

Part 1: (epoch_id, seq) Pair Uniqueness

Section 9.4 (Sender Nonce State) requires that the sender MUST allocate (epoch_id, seq) pairs in a linearizable manner such that no pair is ever reused with the same epoch secret. Section 9.7 (Linearizability Requirements) defines linearizable operations including allocate_nonce(), which guarantees atomic allocation of unique (epoch_id, seq) pairs.

Section 9.5 (Nonce Uniqueness and Rekeying Rules) enforces that sequence counters MUST reset to 0 upon epoch increment, and that sequence numbers MUST NOT repeat within an epoch. The fail-closed recovery principle in Section 9.4 ensures that if state continuity cannot be proven across restart, the sender cannot reuse previously derived epoch secrets.

Therefore, by normative enforcement, no two packets in the same direction can share the same (epoch_id, seq) pair.

Part 2: IV Uniqueness Per Epoch

The key schedule (Section 6) derives distinct IVs for each direction and epoch. For a given direction, each epoch secret produces a unique c2s_iv or s2c_iv via HKDF expansion with distinct labels. Since epoch secrets are unique (derived from handshake secrets and epoch counters), and the key schedule is deterministic, each epoch-direction pair has a unique IV.

Therefore, for any two packets with different epoch_id values in the same direction, or any two packets in different directions, the IVs differ.

Part 3: Nonce Uniqueness via XOR Construction

By Parts 1 and 2, we have:

• Unique (epoch_id, seq) pairs per direction (Part 1)
• Unique IVs per epoch-direction pair (Part 2)

Consider two nonces: nonce₁ = IV₁ ⊕ (epoch_id₁ || seq₁) and nonce₂ = IV₂ ⊕ (epoch_id₂ || seq₂).

Case 1: Same epoch, different sequences

• If epoch_id₁ = epoch_id₂ and same direction, then IV₁ = IV₂
• By Part 1, seq₁ ≠ seq₂, so (epoch_id₁ || seq₁) ≠ (epoch_id₂ || seq₂)
• Since XOR is a bijection: nonce₁ ≠ nonce₂

Case 2: Different epochs

• If epoch_id₁ ≠ epoch_id₂, the first 4 bytes of (epoch_id₁ || seq₁) differ from (epoch_id₂ || seq₂)
• By Part 2, if same direction then IV₁ ≠ IV₂; if different directions, IVs also differ
• Since the first 4 bytes differ and XOR is a bijection: nonce₁ ≠ nonce₂

Therefore, distinct (epoch_id, seq) pairs produce distinct nonces.

Part 4: Key/Nonce Binding

Section 9.8 (Epoch State Coupling) establishes the Key/Nonce Coupling Invariant: no packet shall be encrypted using a nonce derived from epoch E unless it is also encrypted using the key material (AEAD key and base IV) derived from epoch E's secret.

Section 9.8 recommends bundling all epoch-dependent state into an immutable snapshot installed atomically. The encryption function MUST obtain nonce and key material from the same snapshot reference, and implementations MUST NOT advance epoch or sequence counters independently of key material installation.

Therefore, each nonce is cryptographically bound to its corresponding epoch's key material by normative enforcement.

Conclusion:

By Parts 1-3, no two packets transmitted in the same direction share the same nonce. By Part 4, each packet's nonce is used with the corresponding epoch's key material. Therefore, Theorem 1 holds under the condition that the implementation correctly follows Sections 9.4-9.9.

Assumptions:

1. Assumption 1 (Cryptographic): The key schedule (Section 6) correctly derives distinct IVs for each epoch-direction pair. This is a cryptographic property of the HKDF-based key derivation.
2. Assumption 2 (Implementation Correctness): The implementation correctly follows Sections 9.4-9.9. This is an implementation requirement, not a cryptographic assumption. Violations are detectable via Section 9.6 (Receiver-Side Detection) and manifest as authentication failures or duplicate detection.
3. Assumption 3 (Range Validity): Epoch and sequence values are within their valid ranges:
   • epoch_id ∈ [0, 2^32 - 1]
   • seq ∈ [0, 2^64 - 1]

Enforcement Mechanisms:

The proof relies on normative enforcement mechanisms rather than assumptions:

• Section 9.4 enforces linearizable nonce allocation and fail-closed recovery
• Section 9.5 enforces sequence counter reset on epoch increment and sequence uniqueness
• Section 9.6 provides receiver-side detection of duplicates and nonce reuse
• Section 9.7 defines linearizability requirements for epoch state operations
• Section 9.8 enforces key/nonce coupling via epoch snapshot pattern
• Section 9.9 enforces single-owner epoch mutation to prevent race conditions