/-
QSSLProofs.CipherSuite
Cipher suite enumeration and classification for qssl.
12 cipher suites: 5 patent-free (SPHINCS+ KEM) + 7 deprecated (Kyber-based).
Key results:
- cipher_suite_count — Fintype.card = 12
- patent_free_count — 5 SPHINCS+ KEM suites are patent-free
- suite_codes_injective — all u16 codes are distinct
- default_suite_patent_free — default suite (0x0011) is patent-free
Mirrors: crypto/mod.rs CipherSuite enum.
Tier 3 verification (Kani → Verus → **Lean 4**).
-/
import Mathlib.Tactic.NormNum
import Mathlib.Data.Fintype.Card
namespace QSSLProofs.CipherSuite
/-! ## Cipher suite enumeration -/
/-- The 12 cipher suites supported by qssl. -/
inductive Suite where
-- Patent-free SPHINCS+ KEM suites (0x0010–0x0014)
| SphincsKemFalcon512Aes128
| SphincsKemFalcon512Aes256
| SphincsKemFalcon1024Aes256
| SphincsKemSphincs256fAes256
| SphincsKemFalcon512ChaCha20
-- Deprecated Kyber-based suites (0x0001–0x0007)
| Kyber512Falcon512Aes128
| Kyber768Falcon512Aes256
| Kyber1024Falcon1024Aes256
| Kyber512Sphincs128fAes128
| Kyber768Sphincs256fAes256
| Kyber1024Dilithium3Aes256
| Kyber768Falcon512ChaCha20
deriving DecidableEq
/-- Wire code (u16) for each cipher suite. -/
def suite_code : Suite → ℕ
| .SphincsKemFalcon512Aes128 => 0x0010
| .SphincsKemFalcon512Aes256 => 0x0011
| .SphincsKemFalcon1024Aes256 => 0x0012
| .SphincsKemSphincs256fAes256 => 0x0013
| .SphincsKemFalcon512ChaCha20 => 0x0014
| .Kyber512Falcon512Aes128 => 0x0001
| .Kyber768Falcon512Aes256 => 0x0002
| .Kyber1024Falcon1024Aes256 => 0x0003
| .Kyber512Sphincs128fAes128 => 0x0004
| .Kyber768Sphincs256fAes256 => 0x0005
| .Kyber1024Dilithium3Aes256 => 0x0006
| .Kyber768Falcon512ChaCha20 => 0x0007
/-- Whether a suite is patent-free (SPHINCS+ KEM based). -/
def is_patent_free : Suite → Bool
| .SphincsKemFalcon512Aes128 => true
| .SphincsKemFalcon512Aes256 => true
| .SphincsKemFalcon1024Aes256 => true
| .SphincsKemSphincs256fAes256 => true
| .SphincsKemFalcon512ChaCha20 => true
| _ => false
/-- Whether a suite uses AES-256-GCM. -/
def uses_aes256 : Suite → Bool
| .SphincsKemFalcon512Aes256 => true
| .SphincsKemFalcon1024Aes256 => true
| .SphincsKemSphincs256fAes256 => true
| .Kyber768Falcon512Aes256 => true
| .Kyber1024Falcon1024Aes256 => true
| .Kyber768Sphincs256fAes256 => true
| .Kyber1024Dilithium3Aes256 => true
| _ => false
/-- Whether a suite uses Falcon-512. -/
def uses_falcon512 : Suite → Bool
| .SphincsKemFalcon512Aes128 => true
| .SphincsKemFalcon512Aes256 => true
| .SphincsKemFalcon512ChaCha20 => true
| .Kyber512Falcon512Aes128 => true
| .Kyber768Falcon512Aes256 => true
| .Kyber768Falcon512ChaCha20 => true
| _ => false
/-! ## Fintype instance -/
instance : Fintype Suite where
elems := { .SphincsKemFalcon512Aes128, .SphincsKemFalcon512Aes256,
.SphincsKemFalcon1024Aes256, .SphincsKemSphincs256fAes256,
.SphincsKemFalcon512ChaCha20,
.Kyber512Falcon512Aes128, .Kyber768Falcon512Aes256,
.Kyber1024Falcon1024Aes256, .Kyber512Sphincs128fAes128,
.Kyber768Sphincs256fAes256, .Kyber1024Dilithium3Aes256,
.Kyber768Falcon512ChaCha20 }
complete := by intro x; cases x <;> simp
/-! ## Cardinality theorems -/
/-- There are exactly 12 cipher suites. -/
theorem cipher_suite_count : Fintype.card Suite = 12 := by
native_decide
/-- 5 patent-free + 7 deprecated = 12 total (partition is complete). -/
theorem patent_free_plus_deprecated : 5 + 7 = 12 := by norm_num
/-! ## Suite code properties -/
/-- All cipher suite codes are distinct (injective mapping). -/
theorem suite_codes_injective : Function.Injective suite_code := by
intro a b h
cases a <;> cases b <;> simp [suite_code] at h <;> rfl
/-- Patent-free suite codes are in range [0x0010, 0x0014]. -/
theorem sphincs_kem_range :
suite_code .SphincsKemFalcon512Aes128 = 0x0010 ∧
suite_code .SphincsKemFalcon512ChaCha20 = 0x0014 := by
simp [suite_code]
/-- Kyber suite codes are in range [0x0001, 0x0007]. -/
theorem kyber_range :
suite_code .Kyber512Falcon512Aes128 = 0x0001 ∧
suite_code .Kyber768Falcon512ChaCha20 = 0x0007 := by
simp [suite_code]
/-! ## Classification theorems -/
/-- The default cipher suite (SphincsKemFalcon512Aes256 = 0x0011) is patent-free. -/
theorem default_suite_patent_free :
is_patent_free .SphincsKemFalcon512Aes256 = true := by rfl
/-- Default suite code is 0x0011. -/
theorem default_suite_code :
suite_code .SphincsKemFalcon512Aes256 = 0x0011 := by rfl
/-- Patent-free suite count: exactly 5 suites have is_patent_free = true. -/
theorem patent_free_count :
is_patent_free .SphincsKemFalcon512Aes128 = true ∧
is_patent_free .SphincsKemFalcon512Aes256 = true ∧
is_patent_free .SphincsKemFalcon1024Aes256 = true ∧
is_patent_free .SphincsKemSphincs256fAes256 = true ∧
is_patent_free .SphincsKemFalcon512ChaCha20 = true := by
simp [is_patent_free]
/-- Deprecated suite count: all 7 Kyber suites have is_patent_free = false. -/
theorem deprecated_count :
is_patent_free .Kyber512Falcon512Aes128 = false ∧
is_patent_free .Kyber768Falcon512Aes256 = false ∧
is_patent_free .Kyber1024Falcon1024Aes256 = false ∧
is_patent_free .Kyber512Sphincs128fAes128 = false ∧
is_patent_free .Kyber768Sphincs256fAes256 = false ∧
is_patent_free .Kyber1024Dilithium3Aes256 = false ∧
is_patent_free .Kyber768Falcon512ChaCha20 = false := by
simp [is_patent_free]
/-- Falcon-512 is used in 6 cipher suites. -/
theorem falcon512_suites :
uses_falcon512 .SphincsKemFalcon512Aes128 = true ∧
uses_falcon512 .SphincsKemFalcon512Aes256 = true ∧
uses_falcon512 .SphincsKemFalcon512ChaCha20 = true ∧
uses_falcon512 .Kyber512Falcon512Aes128 = true ∧
uses_falcon512 .Kyber768Falcon512Aes256 = true ∧
uses_falcon512 .Kyber768Falcon512ChaCha20 = true := by
simp [uses_falcon512]
/-- AES-256-GCM is used in 7 cipher suites. -/
theorem aes256_suites :
uses_aes256 .SphincsKemFalcon512Aes256 = true ∧
uses_aes256 .SphincsKemFalcon1024Aes256 = true ∧
uses_aes256 .SphincsKemSphincs256fAes256 = true ∧
uses_aes256 .Kyber768Falcon512Aes256 = true ∧
uses_aes256 .Kyber1024Falcon1024Aes256 = true ∧
uses_aes256 .Kyber768Sphincs256fAes256 = true ∧
uses_aes256 .Kyber1024Dilithium3Aes256 = true := by
simp [uses_aes256]
end QSSLProofs.CipherSuite