/-
QSSLProofs.HybridKEM
Hybrid SPHINCS+/Falcon KEM construction properties.
SPHINCS+ provides long-term identity; Falcon-512 provides ephemeral signing.
Key results:
- hybrid_ciphertext_min — min ciphertext = 17937 bytes
- hybrid_fits_handshake — ciphertext fits MAX_HANDSHAKE_SIZE
- hybrid_exceeds_record — ciphertext needs TLS record fragmentation
- hybrid_provides_dual_auth — two distinct signature schemes in one KEM
Mirrors: quantum_native/sphincs_kem.rs SphincsKem.
Tier 3 verification (Kani → Verus → **Lean 4**).
-/
import Mathlib.Tactic.NormNum
namespace QSSLProofs.HybridKEM
/-! ## Component sizes -/
/-- Falcon-512 public key size: 897 bytes. -/
def FALCON_PK_SIZE : ℕ := 897
/-- Ephemeral secret size: 64 bytes (512-bit seed). -/
def EPHEMERAL_SIZE : ℕ := 64
/-- SPHINCS+-Haraka-128f signature size: 16976 bytes. -/
def SPHINCS_SIG_SIZE : ℕ := 16976
/-- Falcon-512 detached signature size: 658 bytes. -/
def FALCON_SIG_SIZE : ℕ := 658
/-- Maximum TLS record payload size. -/
def MAX_RECORD_SIZE : ℕ := 16384
/-- Maximum TLS handshake message size. -/
def MAX_HANDSHAKE_SIZE : ℕ := 65536
/-! ## Hybrid ciphertext structure -/
/-- Minimum hybrid ciphertext: falcon_pk(897) + ephemeral(64) + sphincs_sig(16976) = 17937 bytes.
This is the minimum wire size for a SPHINCS+ KEM exchange. -/
theorem hybrid_ciphertext_min :
FALCON_PK_SIZE + EPHEMERAL_SIZE + SPHINCS_SIG_SIZE = 17937 := by
norm_num [FALCON_PK_SIZE, EPHEMERAL_SIZE, SPHINCS_SIG_SIZE]
/-- The ciphertext has 3 components: falcon_pk + ephemeral + sphincs_sig. -/
theorem hybrid_components :
FALCON_PK_SIZE > 0 ∧ EPHEMERAL_SIZE > 0 ∧ SPHINCS_SIG_SIZE > 0 := by
norm_num [FALCON_PK_SIZE, EPHEMERAL_SIZE, SPHINCS_SIG_SIZE]
/-! ## TLS fitting -/
/-- Hybrid ciphertext fits within MAX_HANDSHAKE_SIZE: 17937 < 65536. -/
theorem hybrid_fits_handshake :
FALCON_PK_SIZE + EPHEMERAL_SIZE + SPHINCS_SIG_SIZE < MAX_HANDSHAKE_SIZE := by
norm_num [FALCON_PK_SIZE, EPHEMERAL_SIZE, SPHINCS_SIG_SIZE, MAX_HANDSHAKE_SIZE]
/-- Hybrid ciphertext exceeds MAX_RECORD_SIZE — needs fragmentation. -/
theorem hybrid_exceeds_record :
FALCON_PK_SIZE + EPHEMERAL_SIZE + SPHINCS_SIG_SIZE > MAX_RECORD_SIZE := by
norm_num [FALCON_PK_SIZE, EPHEMERAL_SIZE, SPHINCS_SIG_SIZE, MAX_RECORD_SIZE]
/-- Hybrid ciphertext requires exactly 2 TLS records.
Ceil(17937 / 16384) = 2. -/
theorem hybrid_fragments :
let ct := FALCON_PK_SIZE + EPHEMERAL_SIZE + SPHINCS_SIG_SIZE
(ct + MAX_RECORD_SIZE - 1) / MAX_RECORD_SIZE = 2 := by
norm_num [FALCON_PK_SIZE, EPHEMERAL_SIZE, SPHINCS_SIG_SIZE, MAX_RECORD_SIZE]
/-! ## Component dominance -/
/-- Ephemeral secret = 64 bytes = 512 bits of entropy. -/
theorem ephemeral_entropy : EPHEMERAL_SIZE * 8 = 512 := by
norm_num [EPHEMERAL_SIZE]
/-- Falcon-512 public key dominates ephemeral: 897 > 64. -/
theorem falcon_pk_dominates : FALCON_PK_SIZE > EPHEMERAL_SIZE := by
norm_num [FALCON_PK_SIZE, EPHEMERAL_SIZE]
/-- SPHINCS+ signature dominates both other components combined:
16976 > 897 + 64 = 961. -/
theorem sphincs_sig_dominates :
SPHINCS_SIG_SIZE > FALCON_PK_SIZE + EPHEMERAL_SIZE := by
norm_num [SPHINCS_SIG_SIZE, FALCON_PK_SIZE, EPHEMERAL_SIZE]
/-- Hybrid ciphertext is much larger than a pure Falcon-512 signature:
17937 > 658. -/
theorem hybrid_vs_pure_falcon :
FALCON_PK_SIZE + EPHEMERAL_SIZE + SPHINCS_SIG_SIZE > FALCON_SIG_SIZE := by
norm_num [FALCON_PK_SIZE, EPHEMERAL_SIZE, SPHINCS_SIG_SIZE, FALCON_SIG_SIZE]
end QSSLProofs.HybridKEM