Email Gateway (Jul 07 2025 at 11:07): Email Gateway (Jul 07 2025 at 11:07):From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
there is yet another new AFP entry today:
The Oneway to Hiding Theorem
by Katharina Kreuzer and Dominique Unruh
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.
https://www.isa-afp.org/entries/Oneway2Hiding.html
Enjoy,
René
Last updated: Jul 26 2025 at 12:43 UTC