The Oneway to Hiding Theorem

Katharina Kreuzer 📧 and Dominique Unruh 🌐

June 27, 2025

Abstract

As the standardization process for post-quantum cryptography progresses, the need for computer-verified security proofs against classical and quantum attackers increases. Even though some tools are already tackling this issue, none are foundational. We take a first step in this direction and present a complete formalization of the One-way to Hiding (O2H) Theorem, a central theorem for security proofs against quantum attackers. With this new formalization, we build more secure foundations for proof-checking tools in the quantum setting. Using the theorem prover Isabelle, we verify the semi-classical O2H Theorem by Ambainis, Hamburg and Unruh (Crypto 2019) in different variations. We also give a novel (and for the formalization simpler) proof to the O2H Theorem for mixed states and extend the theorem to non-terminating adversaries. This work provides a theoretical and foundational background for several verification tools and for security proofs in the quantum setting.

License

BSD License

Topics

Related publications

  • Heidler, K., & Unruh, D. (2025). Formalizing the One-Way to Hiding Theorem. Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, 243–256. https://doi.org/10.1145/3703595.3705887

Session Oneway2Hiding