Post-Quantum Verification of Fujisaki-Okamoto

Dominique Unruh

Paper 2020/962 Original: eprint.iacr.org/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).

Metadata

Available format(s): PDF
Category: Public-key cryptography
Publication info: Preprint.
History: 2020-08-11: last updated; 2020-08-11: published
Short URL: https://ia.cr/2020/962
License: https://creativecommons.org/licenses/by/4.0/

BibTeX

@misc{cryptoeprint:2020/962,
      author = {Dominique Unruh},
      title = {Post-Quantum Verification of Fujisaki-Okamoto},
      howpublished = {Cryptology {ePrint} Archive, Paper 2020/962},
      year = {2020},
      url = {https://eprint.iacr.org/2020/962}
}