Formalizing the One-way to Hiding Theorem

Watch a 24-minute conference talk from CPP 2025 where Katharina Heidler and Dominique Unruh present their work on formalizing the One-Way to Hiding (O2H) Theorem, a crucial component for security proofs against quantum attackers. Learn how the researchers used the Isabelle theorem prover to verify the semi-classical O2H Theorem in different variations, developed a novel proof for mixed states, and extended the theorem to non-terminating adversaries. This presentation provides foundational background for verification tools and security proofs in quantum settings, contributing to the growing need for computer-verified security proofs as post-quantum cryptography standardization advances. The talk was presented at the CPP 2025 conference, sponsored by ACM SIGPLAN and ACM SIGLOG.