Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Compressed Oracles


view this post on Zulip Email Gateway (Jan 16 2026 at 16:22):

From: Lawrence Paulson <lp15@cam.ac.uk>

I am happy to announce a new entry, Compressed Oracles, by Dominique Unruh.

Abstract
We formalize the compressed quantum random oracle methodology by Zhandry (Crypto 2019). This is a formalism for modeling quantum random oracles to make quantum cryptographic proofs feasible. Our definition of the compressed oracles is loosely based on the presentation from Unruh (arXiv 2021), but with a considerable amount of new definitions and results. In particular, we make extensive use of the quantum references formalism (Unruh, arXiv 2024, AFP 2025) to enable reasoning about queries on arbitrary subsystems, something which is left very informal in pen-and-paper formalizations of the compressed oracles. We use the developed formalism to prove that finding x with H(x)=0, and finding collisions in H, is hard for quantum adversaries with oracle access to a random function H.
https://www.isa-afp.org/entries/Compressed_Oracles.html

Larry


Last updated: Jan 31 2026 at 12:53 UTC