Quantum Cryptography
Toward a formal theory of quantum cryptographic security
Quantum cryptography promises unconditional security grounded in the laws of physics — but the proofs that underpin this promise are among the most intricate in all of quantum information science. Security arguments for quantum key distribution, error correction, and related protocols chain together entropy bounds, channel properties, and sampling arguments in ways where subtle errors can compromise the entire guarantee. Our goal is to advance the theory of quantum cryptographic security: proving new theorems, establishing tighter bounds, and building a formally verified body of results that can be trusted, extended, and built upon with confidence.
Security That Must Be Machine Verified
Quantum cryptographic security proofs are long chains of analytical arguments where each step must be exactly right for the guarantee to hold. A single gap in an entropy bound or a subtle error in a channel argument can invalidate an entire security claim. As protocols grow more sophisticated and security models more nuanced, the need for machine-checkable verification becomes not just convenient but essential.
This project builds on the verified mathematical infrastructure developed in our Quantum Information project — using its entropy theory, channel characterizations, and distance bounds as the foundation for rigorous cryptographic security proofs.
Proving New Theorems in Quantum Security
Tighter Bounds on Information Leakage
Quantum cryptographic security rests on limiting what an adversary can learn. We are working to prove new, tighter bounds on information leakage — refining entropy-based arguments and extending guarantees to regimes where existing results leave gaps.
Error Correction and Privacy Amplification
Error correction and privacy amplification are the two stages that turn a noisy, partially compromised raw key into a final secure key. We aim to prove new theorems about both — tighter distance bounds for quantum codes, stronger privacy amplification guarantees, and a rigorous understanding of how these stages interact under realistic conditions.
Device-Independent QKD
Device-independent quantum key distribution promises security that relies on the laws of physics alone, with no assumptions about the internal workings of quantum devices. We are pursuing formally verified device-independent security proofs, where Bell inequality violations certify that communication is secure.
New Protocol Design
The frontier of quantum key distribution has moved well beyond BB84. We are interested in proving security for state-of-the-art protocol families — including high-dimensional QKD, decoy-state protocols, and twin-field QKD — where higher key rates, longer distances, and stronger noise tolerance demand new theoretical tools and tighter analytical arguments.
End-to-End Experimental Verification
Theoretical security proofs and laboratory implementations are often separated by a gap of modeling assumptions. We aim to bridge this gap by developing formally verified analyses of experimental quantum cryptographic demonstrations — ensuring that security guarantees extend from theory to practice.
What We Aim to Prove
Building from First Principles
Formally verified results establishing the methodology for a broader program of cryptographic security.