Cryptology ePrint Archive: Report 2020/962

Post-Quantum Verification of Fujisaki-Okamoto

Dominique Unruh

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, and Unruh, PKC 2020). The formalization is done in quantum relational Hoare logic and checked in the qrhl-tool (Unruh, POPL 2019).

Category / Keywords: public-key cryptography / Formal verification, post-quantum cryptography, public-key encryption

Date: received 6 Aug 2020, last revised 6 Aug 2020

Contact author: unruh at ut ee

Available format(s): PDF | BibTeX Citation

Version: 20200811:114020 (All versions of this report)

Short URL:

[ Cryptology ePrint archive ]