Formal verification of post-quantum cryptography

QuICS Seminar

Speaker: 
Dominique Unruh (University of Tartu)
Time: 
Wednesday, January 15, 2020 - 11:00am
Location: 
PSC 3150

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.