log in  |  register  |  feedback?  |  help  |  web accessibility
Logo
Formal verification of post-quantum cryptography
Dominique Unruh - University of Tartu
Wednesday, January 15, 2020, 11:00 am-12:15 pm Calendar
  • You are subscribed to this talk through .
  • You are watching this talk through .
  • You are subscribed to this talk. (unsubscribe, watch)
  • You are watching this talk. (unwatch, subscribe)
  • You are not subscribed to this talk. (watch, subscribe)
Abstract

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.

This talk is organized by Andrea F. Svejda