Formalizing the One-way to Hiding Theorem
summary
Formalizes the One-way to Hiding (O2H) theorem inside Isabelle, proving the semi-classical O2H variants and providing a novel, simpler mixed-state proof while extending the result to non-terminating adversaries and infinite-dimensional Hilbert spaces. Implementation totals about 7,000 lines of Isabelle code, depends on existing quantum/Hilbert libraries, and exposes one main limitation: no support yet for parallel quantum queries. Work is ready to connect to the QRL tool once parallel-query encoding is solved.
AI-written summary · about
chapters (30)
- 0:00Introduction
- 0:20Quantum security motivation
- 1:03Quantum computing basics
- 2:30Quantum bits properties
- 4:18Cryptography security basics
- 4:59Indistinguishability under CPA
- 6:02Quantum security overview
- 6:22Quantum security landscape
- 7:28Random oracle model
- 8:10One-way to hiding theorem
- 8:30Formalizing in Isabelle
- 9:15Need for formal verification
- 10:00QRL tool context
- 10:20Intuition behind theorem
- 11:05Reprogramming in classical vs quantum settings
- 12:29Quantum random oracle challenges
- 13:09Theorem statement
- 13:53Theorem formalization
- 14:37Formalization complexities
- 15:21Contributions to theorem
- 16:48Generalizing to infinite dimensions
- 17:30Proof refinement process
- 17:53Limitations and future work
- 18:56Probability distributions
- 19:38Publication plans
- 20:00Dependencies and background libraries used
- 20:41Conclusion
- 21:27Q&A
- 21:48QRL tool integration
- 22:11Handling non-terminating adversaries
related talks
46mObfuscation of Unitary Quantum Programs
59mAn Introduction to Quantum Obfuscation
32mQuantum Obfuscation of Classical Circuits
12mOne-Way Functions Imply Secure Computation in a Quantum World
01h 03mFrom Program Obfuscation to Unclonable Cryptography
17mProofs of Quantumness from Trapdoor Permutations
01h 13mQuantum 3
52mIndistinguishability Obfuscation via Mathematical Proofs of Equivalence