Security Invariants

This appendix defines security invariants that MUST hold at all times in any correct PALISADE implementation. Any implementation violating these invariants is non-compliant by definition, even if it appears to follow the wire protocol.

1. Core Security Invariants

PALISADE implementations MUST enforce the following core invariants:

Receiver sovereignty over epochs: Epoch changes occur only via explicit, ordered protocol steps. No packet—early or otherwise—may change what packets are acceptable next unless it is non-replayable.
Replayable data cannot steer state: Any replayable message (including early data) MUST be non-authoritative and MUST NOT cause durable state transitions.
Commit points are explicit: Migration/path binding updates MUST have an explicit commit step authenticated under normal traffic keys.
Fail-fast on ambiguity: Unknown flags, unrecognized frame types in early data, and key_phase mismatches outside TRANSITION MUST result in immediate packet drop, not search or retry.

Verification Guidance: Implementations SHOULD include tests verifying each invariant under adversarial conditions (replayed packets, reordered packets, forged headers).

2. Invariant Summary Table

Each row defines an invariant, along with:

Area – Handshake, key schedule, replay, migration, etc.
Invariant – The property that must always hold.
Enforced By – Mechanism(s) that enforce it.
Violation Impact – What can go wrong if broken.
Implementation Checks – Where to verify it in code.

Table 1 — Handshake & Key Schedule Invariants

#	Area	Invariant	Enforced By	Violation Impact	Implementation Checks
1	Handshake	Every accepted ServerHello MUST be uniquely bound to a single ClientHello transcript.	Transcript hash; HKDF inputs; signature over transcript.	Unknown key-share / MITM; identity misbinding.	Ensure transcript includes all CH/SH fields before KDF and signature verification.
2	Handshake	Version, KEM, SIG, and AEAD choices MUST be included in the transcript before keys are derived.	Transcript construction rules.	Downgrade attacks to weaker algorithms or versions.	Verify code always adds these parameters into the transcript prior to HKDF.
3	Handshake	Failed handshake verification MUST NOT lead to any application keys being installed or used.	Strict error handling paths.	Use of attacker-controlled keys; silent compromise.	Check that any failure leads to immediate abort and key wipe.
4	Key Schedule	Each epoch's keys MUST be derived from previous key material and fresh inputs (nonces, KEM secrets).	Defined HKDF key schedule.	Loss of forward secrecy; key reuse across epochs.	Confirm implementation uses correct HKDF labels and inputs per epoch.
5	Key Schedule	Long-term authentication keys MUST never be used directly as traffic keys.	Separation between auth keys and traffic keys.	Catastrophic key reuse; cryptanalytic exposure.	Verify auth keys are only used in signatures, never directly for AEAD or KEM.

Table 2 — Replay & Sequence Invariants

#	Area	Invariant	Enforced By	Violation Impact	Implementation Checks
6	Replay	Each `(epoch_id, seq)` pair MUST be used at most once for any AEAD encryption.	Sequence counters; send/recv state tracking.	AEAD nonce reuse; potential plaintext recovery or forgery.	Verify sequence increment is atomic and never rolls back; assert no reuse per epoch.
7	Replay	Received packets with `(epoch_id, seq)` at or below the accepted window MUST be rejected.	Replay window; receive filters.	Acceptance of replayed ciphertexts.	Implement sliding window / bitmap; unit test replay rejection logic.
8	Replay	Replay protection MUST remain effective solely using (epoch_id, seq), even if timestamps are absent, zero, or disabled.	Epoch/seq binding; AEAD integrity.	Time-based replay protections bypassed.	Confirm replay logic uses only epoch/seq, not timestamps.

Table 3 — Resumption & 0-RTT Invariants

#	Area	Invariant	Enforced By	Violation Impact	Implementation Checks
9	Resumption	Resumption tickets MUST be bound to the original authenticated server identity and parameters.	Ticket contents; transcript binding.	Ticket theft leading to cross-server abuse.	Ensure tickets encode server identity and are validated on resume.
10	Resumption	Servers MUST enforce `max_early_data_bytes` from the ticket, not from the client's offer.	Ticket semantics; 0-RTT enforcement rule.	0-RTT replay amplification; abuse as DoS tool.	Confirm server always reads limit from ticket and ignores client-supplied limits.
11	0-RTT	Early data MUST be treated as replayable, MUST be cryptographically isolated from application traffic keys, and MUST be restricted to idempotent or specially marked operations.	Reserved early-data epoch identifier; early-data-specific keys; application guidance; API design.	Logical or financial replay vulnerabilities.	Document and enforce separate APIs for early-data-safe operations.

Table 4 — Migration & Path Invariants (PALISADE-PLUS)

#	Area	Invariant	Enforced By	Violation Impact	Implementation Checks
12	Migration	Migration MUST NOT change the cryptographic identity of the peer (same keys, same identity).	Binding tokens; unchanged certificates/keys.	Path-based MITM or identity confusion.	Verify that migration only updates path metadata, not auth state.
13	Migration	New paths MUST be validated via authenticated encrypted traffic within the existing session or via resumption, before becoming primary.	Path validation mechanism.	Off-path injection; traffic diversion attacks.	Test that unvalidated paths never become primary for data traffic.
14	Migration	Failure of migration MUST NOT corrupt the existing stable tunnel state.	Clear separation of path state vs crypto state.	Loss of established tunnel; data interruption.	Ensure rollback to previous path leaves keys and epoch unchanged.

Table 5 — Certificate & Authentication Invariants

#	Area	Invariant	Enforced By	Violation Impact	Implementation Checks
15	Certificates	Only PQ-only certificates (as defined in PALISADE v1.1) MUST be accepted, unless a future extension is negotiated.	Certificate parsing and policy.	Weakened security through hybrid downgrade.	Ensure certificate validation rejects non-PQ or hybrid unless explicitly allowed.
16	Authentication	Server identity keys MUST be obtained through authenticated control-plane provisioning or pre-configured trust anchors, and the handshake MUST verify the server's signature against the expected public key.	Control plane authentication; key pinning; signature verification.	Connection to impersonated or unauthorized servers; MITM attacks.	Verify client rejects servers whose public key doesn't match the provisioned/expected key.
17	Authentication	Client authentication (if enabled) MUST bind client identity to the same transcript as the key exchange.	Client certificate + transcript binding.	Client-unknown key-share; identity confusion.	Check that client cert verification includes transcript-bound verification.

Table 6 — Parsing & Encoding Invariants

#	Area	Invariant	Enforced By	Violation Impact	Implementation Checks
18	Parsing	Any length field that would cause a message to exceed the global 128 KB limit MUST cause immediate rejection.	Global message size cap.	Buffer overflows; resource exhaustion; bugs.	Add size checks before any allocation; fuzz-test malformed inputs.
19	Parsing	All multi-byte integers MUST be fixed-width and big-endian; no varints are allowed.	Encoding rules; ABNF.	Divergent encodings; interop failures.	Validate encoders/decoders via cross-implementation tests.
20	Encoding	Canonical encoding MUST be deterministic given the same input parameters.	Fixed field order, padding rules, encoding rules.	Transcript mismatches; signature validation failures.	Ensure no random or conditional field reordering in serialization.

Table 7 — Padding & Traffic Invariants

#	Area	Invariant	Enforced By	Violation Impact	Implementation Checks
21	Padding	All padding bytes MUST be included in the AEAD-protected plaintext and MUST NOT affect protocol parsing or semantics.	Padding semantics in spec.	Non-deterministic encodings; parsing ambiguity.	Assert all padding-written bytes are zero; verify decryption discards padding correctly.
22	Traffic	Traffic shaping or padding features MUST NOT reveal secret-dependent patterns via control frames.	Application of padding independent of secrets.	Side-channel leakage through protocol metadata.	Review padding logic for secret-dependent conditions; run side-channel testing where feasible.

Table 8 — Error Handling & Key Lifecycle Invariants

#	Area	Invariant	Enforced By	Violation Impact	Implementation Checks
23	Error Handling	Any fatal protocol error MUST cause immediate key erasure and transition to a closed or abort state.	Error paths in state machines.	Continued use of compromised keys.	Ensure all fatal alerts pass through a common key-wipe and close path.
24	Key Lifecycle	Cryptographic keys MUST be zeroized in memory once no longer needed (per-epoch and on close).	Key management routines.	Long-lived sensitive data in memory.	Code review and tests for zeroization calls on all key lifetimes.
25	Logging	Logs MUST NOT contain raw keys, nonces, or plaintext application data.	Logging policies and redaction rules.	Sensitive data exposure through logs.	Review logging calls; enforce structured logging with strict redaction.

PALISADE Protocol Specification Draft 00

INFORMATIONAL