Maor Ben Shahar

We formalize the security proof chain of the BB84 quantum key distribution protocol in Lean 4, an interactive theorem prover. The development covers IID security, collective attacks, the quantum de Finetti theorem, and the reduction from general attacks to collective attacks. Every deduction is verified by the Lean proof kernel, ensuring that all assumptions and preconditions are explicit and mechanically checked. The project also introduces a reusable quantum information theory library supporting entropy inequalities, quantum channels, and representation-theoretic tools required for QKD security proofs. The resulting development establishes a Lean framework for machine-verified quantum cryptographic security proofs.