Abstract: We present a computer-verified formalization of the post-quantum security proof of the Fujisaki-Okamoto transform (as analyzed by Hövelmanns, Kiltz, Schäge, Unruh, Generic Authenticated Key Exchange in the Quantum Random Oracle Model, 2020). The formalization is done in quantum relational Hoare logic and checked in the qrhl-tool (Unruh, Quantum Relational Hoare Logic, 2019).
Permalink: http://www.ut.ee/~unruh/publications/hksu-verify.html