Email Gateway (Jun 26 2025 at 13:32): Email Gateway (Jun 26 2025 at 13:32):From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
and of course I stay happy, since there is yet another new AFP entry.
The Hidden Number Problem
by Sage Binder, Eric Ren and Katherine Kosaian
In this entry, we formalize the Hidden Number Problem (HNP), originally
introduced by Boneh and Venkatesan in 1996. Intuitively, the HNP involves
demonstrating the existence of an algorithm (the ``adversary'') which can
compute (with high probability) a hidden number alpha given access to a
bit-leaking oracle. Originally developed to establish the security of
Diffie--Hellman key exchange, the HNP has since been used not only for protocol
security but also in cryptographic attacks, including notable ones on DSA and
ECDSA. Additionally, the HNP makes use of an instance of Babai's nearest plane
algorithm, which solves the approximate closest vector problem. Thus, building
on the LLL algorithm (which has already been formalized), we formalize Babai's
algorithm, which itself is of independent interest. Our formalizations of
Babai's algorithm and the HNP adversary are executable, setting up potential
future work, e.g. in developing formally verified instances of cryptographic
attacks. Note, our formalization of Babai's algorithm here is an updated version
of a previous AFP entry of ours. The updates include a tighter error bound,
which is required for our HNP proof.
https://www.isa-afp.org/entries/Hidden_Number_Problem.html
Enjoy,
René
P.S.: No further announcements from my side for today.
Last updated: Jul 02 2025 at 08:30 UTC