Peter Schwabe
Max Planck Institute for Security and Privacy & Radboud University
9th January 2025, 4:00PM - 5:00PM (GST)
| Title: | End-to-end formal verification of ML-KEM |
| Abstract: | In 2021, the Formosa-Crypto project set out to build the next generation of cryptographic software with formal, computer-verified, guarantees of functional correctness and implementation security linked to reductionist proofs of security for (mostly) post-quantum primitives. As a first successful example of such cryptographic software this talk will consider ML-KEM (or CRYSTALS-Kyber), the only KEM that was selected for standardization by NIST in 2022. The "end-to-end" verification links highly optimized assembly code through a high-level machine-readable specification of ML-KEM to the IND-CCA security notion. We additionally prove protection of this optimized assembly code against traditional timing attacks and multiple classes of Spectre attacks. |
| Bio: | Peter Schwabe is scientific director at MPI-SP and professor at Radboud University. He graduated from RWTH Aachen University in computer science in 2006 and received a Ph.D. from the Faculty of Mathematics and Computer Science of Eindhoven University of Technology in 2011. He then worked as a postdoctoral researcher at the Institute for Information Science and the Research Center for Information Technology Innovation of Academia Sinica, Taiwan and at National Taiwan University. His research area is cryptographic engineering; in particular the security and performance of cryptographic software. He published more than 70 articles in journals and at international conferences presenting, for example, fast software for a variety of cryptographic primitives including AES, hash functions, elliptic-curve cryptography, and cryptographic pairings. He has also published articles on fast cryptanalysis, in particular attacks on the discrete-logarithm problem. In recent years he has focused in particular on post-quantum cryptography. He co-authored the "NewHope" and "NTRU-HRSS" lattice-based key-encapsulation schemes which were used in post-quantum TLS experiments by Google and he is co-submitter of seven proposals to the NIST post-quantum crypto project, all of which made it to the second round, five of which made it to the third round, and 3 of which were selected after round 3 for standardization. In 2021, he co-founded the Formosa-Crypto project, an effort by multiple research groups to build (post-quantum) cryptographic software with formal proofs of functional correctness and security. |