Post-Quantum Verification of Fujisaki-Okamoto (AsiaCrypt 2020)
Dominique Unruh
[ eprint | official ]
We present a computer-verified formalization of the post-quantum security proof of the Fujisaki-Okamoto transform (as analyzed by [CITE pq-ake]). The formalization is done in quantum relational Hoare logic and checked in the qrhl-tool ([CITE qrhl]).