Gamma

Informative

Draft 00

This appendix provides a Gamma-level security proof sketch for PALISADE v1.1. It is not a formal machine-checked proof, but a structured argument intended to:

  • Demonstrate that PALISADE fits within well-studied AKE security models
  • Make explicit which assumptions are relied upon
  • Show how attacks reduce to breaking underlying primitives

This proof sketch should be read in conjunction with:

  • The Formal Threat Model
  • The Security Invariants
  • The State Machine Diagrams
  • The Handshake Message Encodings

If discrepancies arise, the normative specification text takes precedence.

1. Proof Scope and Model

1.1 Security Model

PALISADE is analyzed as an authenticated key exchange (AKE) protocol in the spirit of:

  • SIGMA-I
  • KEMTLS
  • OPTLS
  • TLS 1.3 (for transcript binding and key schedule structure)

The adversary is modeled as a Dolev–Yao network attacker with full control over the network.

The following security properties are claimed:

  • Mutual authentication
  • Forward secrecy (post-quantum)
  • Key indistinguishability
  • Replay resistance
  • Downgrade resistance
  • Channel binding

1.2 Session Identifiers

Each PALISADE session is uniquely identified by:

  • The handshake transcript hash
  • The negotiated parameter set
  • The derived handshake secret

This identifier is used implicitly to prevent unknown key-share attacks.

2. Cryptographic Assumptions

The proof relies on the following assumptions:

  1. KEM Security
    The selected post-quantum KEM is IND-CCA secure.
  2. Signature Security
    The selected post-quantum signature scheme is EUF-CMA secure.
  3. AEAD Security
    The AEAD provides IND-CPA confidentiality and INT-CTXT integrity under unique nonces.
  4. Hash Function Security
    Hash functions used for transcripts and HKDF behave as random oracles (or PRFs where appropriate).
  5. HKDF Security
    HKDF is a secure pseudorandom function when instantiated with a secure hash.
  6. Randomness
    All nonces, ephemeral keys, and random inputs are unpredictable.

3. Handshake Security Argument

3.1 Key Agreement

Claim:
The shared handshake secret is indistinguishable from random to any PPT adversary.

Argument:
The handshake secret is derived from the output of a post-quantum KEM decapsulation. If an adversary can distinguish the handshake secret, it can distinguish the KEM shared secret, contradicting IND-CCA security.

3.2 Authentication

Claim:
An adversary cannot impersonate a legitimate endpoint.

Argument:
Authentication relies on post-quantum signatures over the handshake transcript. Forging a valid handshake transcript signature implies forging a signature under the EUF-CMA model.

3.3 Unknown Key-Share Prevention

Claim:
PALISADE prevents unknown key-share attacks.

Argument:
Endpoint identities, negotiated parameters, and handshake messages are bound into the transcript hash. Any attempt to cause two honest parties to derive the same key under different peer identities would require a collision in the transcript hash or a signature forgery.

4. Key Schedule Security

4.1 Key Separation

Claim:
Handshake keys, application keys, and rekeyed epoch keys are cryptographically independent.

Argument:
Each key is derived via HKDF with domain-separated labels and fresh inputs. Key reuse would imply breaking the PRF security of HKDF.

4.2 Forward Secrecy

Claim:
Compromise of long-term authentication keys does not reveal past session keys.

Argument:
Session keys depend on ephemeral KEM secrets that are erased after use. Recovering past keys would require recovering KEM shared secrets, contradicting KEM security.

5. Replay Resistance

Claim:
Replay of handshake or application data is infeasible.

Argument:

  • Handshake messages are bound to transcripts and verified once.
  • Application packets include (epoch_id, seq) pairs with monotonic enforcement.
  • AEAD integrity ensures that modified or replayed packets are rejected.

An adversary capable of replaying packets must either guess unused (epoch_id, seq) pairs or forge AEAD ciphertexts.

6. Downgrade Resistance

Claim:
Algorithm and version downgrade attacks are prevented.

Argument:
All negotiated parameters are included in the transcript hash before key derivation. Accepting downgraded parameters without detection would imply a transcript collision or signature forgery.

7. Resumption and 0-RTT

7.1 Ticket Security

Claim:
Resumption tickets cannot be used to impersonate endpoints or bypass authentication.

Argument:
Tickets are encrypted and authenticated by the server and bound to the original authenticated session. Using a stolen or modified ticket requires breaking AEAD security.

7.2 Early Data Limit Enforcement

Claim:
Early data replay amplification is prevented.

Argument:
Servers enforce max_early_data_bytes from the ticket. An adversary exceeding this limit cannot cause additional side effects beyond the allowed bound.

8. Migration Security

Claim:
Migration does not allow session hijacking.

Argument:
Migration frames are authenticated and bound to existing session keys. Accepting an attacker-controlled path would require forging migration authentication tokens.

9. Error Handling and Fail-Closed Behavior

Claim:
Protocol failures do not lead to key leakage or undefined states.

Argument:
All fatal errors transition the protocol to a closed state and trigger key erasure. Continuing operation would contradict enforced state machine transitions.

10. Limitations and Non-Goals

This proof sketch does not claim:

  • Resistance to endpoint compromise
  • Side-channel resistance
  • Denial-of-service resistance
  • Anonymity guarantees
  • Post-compromise key healing

These are explicitly outside the PALISADE v1.1 threat model.

11. Conclusion

Under the stated assumptions and threat model, PALISADE v1.1 achieves:

  • Authenticated key exchange security
  • Post-quantum forward secrecy
  • Replay and downgrade resistance
  • Safe extensibility and rekeying

Any attack violating these properties would imply a break of the underlying cryptographic primitives or assumptions.