RSS icon
Twitter icon
Facebook icon
Vimeo icon
YouTube icon

Formal verification of post-quantum cryptography

January 15, 2020 - 11:00am
Dominique Unruh
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