CLH MAX: A Post-Quantum Key Encapsulation Mechanism over Z_q[X]/Φ₂₅₇(X) with Machine-Checked Security

Abstract

This repository contains the official implementation, machine-checked security proofs, and academic manuscript for CLH MAX, a Post-Quantum Key Encapsulation Mechanism (KEM). Technical SpecificationsCLH MAX is designed over the polynomial ring Z_q[X]/Φ₂₅₇(X). By explicitly utilizing the cyclotomic polynomial modulus Φ₂₅₇(X), the architecture systematically eliminates vulnerabilities to subfield attacks present in other lattice-based constructions. Formal Verification in Lean 4The IND-CPA security reduction of the KEM has been rigorously formalized in Lean 4 (using Mathlib). The proof bounds the adversary's advantage against the Decision Ring Learning With Errors (DRLWE) problem.- Structured as a monadic three-game-hopping sequence (Game0, Game1, Game2) utilizing the Probability Mass Function (PMF) monad.- Verification Status: The main reduction theorem compiles perfectly with 1 axiom and 0 sorry placeholders. Licensing ModelThis project strictly enforces a transparent, dual-licensing model:- Software and Source Code: Licensed under the GNU Affero General Public License v3.0 (AGPL-3.0) to ensure full source-code disclosure even in SaaS and cloud deployments.- Academic Manuscript: The paper and LaTeX source files are licensed under Creative Commons Attribution 4.0 International (CC BY 4.0).