Formal verification of post-quantum cryptography
January 15, 2020 - 11:00am
Speaker:
Dominique Unruh
Institution:
University of Tartu
I will present our recent advances in the formal verification of post-quantum security. Our framework includes a logic for reasoning about quantum programs (qRHL, quantum relational Hoare logic) and a tool for computer-aided verification in qRHL. We have used this framework to verify the post-quantum security of the Fujisaki-Okamoto transform for building encryption schemes. I will give an overview of the logical foundations and of our experiences when verifying a real-life cryptosystem.
PSC 3150