Post-Quantum Verification of Fujisaki-Okamoto

Dominique Unruh

Paper 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. MINOR revision.
Keywords: Formal verification post-quantum cryptography public-key encryption
Contact author(s): unruh @ ut ee
History: 2020-08-11: received
Short URL: https://ia.cr/2020/962
License: CC BY

BibTeX

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