Modern communication systems depend on cryptography: before two devices can exchange private messages, they must agree on a secret key. Many widely used methods for doing this could be broken by sufficiently powerful quantum computers, so a transition towards “post-quantum” cryptography aims to design new methods that remain safe in that future.
This thesis studies how to build these new methods not only to be fast, but also to come with strong evidence that they are implemented correctly and securely. It uses formal methods, a way of checking software with mathematical proofs, to reduce reliance on manual review and conventional testing alone.
The main case study is ML-KEM, the new international standard for post-quantum key establishment, and Kyber, the scheme on which it is based. The thesis presents a formally verified, efficient implementation suitable for real-world use. It also explores alternative post-quantum approaches to key agreement and develops new techniques to automate parts of the verification process.
Miguel Quaresma is a Security and Cryptography Researcher and Engineer at Least Authority, where he conducts security audits of cryptographic and distributed applications, from design to implementation. From February 2021 to June 2025, he was a doctoral researcher at the Max Planck Institute for Security and Privacy, under the joint supervision of Gilles Barthe and Peter Schwabe. His doctoral research focused on high-assurance, high-performance implementations of post-quantum cryptography. Prior to his doctoral studies, he worked as a Cybersecurity Analyst at Goldman Sachs. He received his B.Sc. and M.Sc. degrees in computer engineering, specializing in cryptography, information security, and parallel and distributed computing, from the University of Minho. He completed his Master’s thesis, "TrustZone-based Attestation in Secure Runtime Verification for Embedded Systems", at the High-Assurance Software Laboratory (HASLab) under the supervision of José Carlos Bacelar Almeida.