{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:05:22Z","timestamp":1750309522949,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":39,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T00:00:00Z","timestamp":1736467200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"ERC consolidator grant CerQuS","award":["819317"],"award-info":[{"award-number":["819317"]}]},{"name":"Estonian Centre of Excellence in IT","award":["EXCITE, TK148"],"award-info":[{"award-number":["EXCITE, TK148"]}]},{"name":"Estonian Centre of Excellence Foundations of the Universe","award":["TK202"],"award-info":[{"award-number":["TK202"]}]},{"name":"Estonian Research Council PRG grant Secure Quantum Technology","award":["PRG946"],"award-info":[{"award-number":["PRG946"]}]},{"name":"German Research Foundation research training group CanVeY","award":["GRK 2428"],"award-info":[{"award-number":["GRK 2428"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,1,10]]},"DOI":"10.1145\/3703595.3705887","type":"proceedings-article","created":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T21:23:16Z","timestamp":1736544196000},"page":"243-256","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Formalizing the One-Way to Hiding Theorem"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4621-734X","authenticated-orcid":false,"given":"Katharina","family":"Heidler","sequence":"first","affiliation":[{"name":"TU Munich, Munich, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8965-1931","authenticated-orcid":false,"given":"Dominique","family":"Unruh","sequence":"additional","affiliation":[{"name":"RWTH Aachen, Aachen, Germany"},{"name":"University of Tartu, Tartu, Estonia"}]}],"member":"320","published-online":{"date-parts":[[2025,1,10]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-26951-7_10"},{"key":"e_1_3_2_2_2_1","unstructured":"Roberto Maria Avanzi Joppe W. Bos L\u00e9o Ducas Eike Kiltz Tancr\u00e8de Lepoint Vadim Lyubashevsky John M. Schanck Peter Schwabe Gregor Seiler and Damien Stehl\u00e9. 30\/03\/2019. CRYSTALS-Kyber Algorithm Specifications And Supporting Documentation (version 2.0)."},{"key":"e_1_3_2_2_3_1","unstructured":"Roberto Maria Avanzi Joppe W. Bos L\u00e9o Ducas Eike Kiltz Tancr\u00e8de Lepoint Vadim Lyubashevsky John M. Schanck Peter Schwabe Gregor Seiler and Damien Stehl\u00e9. 30\/11\/2017. CRYSTALS-Kyber Algorithm Specifications And Supporting Documentation."},{"volume-title":"Types for Proofs and Programs","author":"Ballarin Clemens","key":"e_1_3_2_2_4_1","unstructured":"Clemens Ballarin. 2004. Locales and Locale Expressions in Isabelle\/Isar. In Types for Proofs and Programs, Stefano Berardi, Mario Coppo, and Ferruccio Damiani (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 34\u201350."},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484567"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10082-1_6"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-019-09341-z"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/168588.168596"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-36033-7_3"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2007.1005"},{"key":"e_1_3_2_2_11_1","unstructured":"Bruno Blanchet. 2024. CryptoVerif: Cryptographic protocol verifier in the computational model. urlhttps:\/\/bblanche.gitlabpages.inria.fr\/CryptoVerif\/ accessed: 2024-07-17"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF61375.2024.00050"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25385-0_3"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2018.00032"},{"key":"e_1_3_2_2_15_1","unstructured":"Jos\u00e9 Manuel Rodr\u00edguez Caballero and Dominique Unruh. 2021. Complex Bounded Operators. Archive of Formal Proofs September issn:2150-914x https:\/\/isa-afp.org\/entries\/Complex_Bounded_Operators.html"},{"key":"e_1_3_2_2_16_1","unstructured":"Jan Czajkowski Christian Majenz Christian Schaffner and Sebastian Zur. 2019. Quantum Lazy Sampling and Game-Playing Proofs for Quantum Indifferentiability. Cryptology ePrint Archive Paper 2019\/428. https:\/\/eprint.iacr.org\/2019\/428"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-72565-9_13"},{"key":"e_1_3_2_2_18_1","unstructured":"Manuel Eberl et al.. 2024. Archive of Formal Proofs. https:\/\/www.isa-afp.org\/"},{"key":"e_1_3_2_2_19_1","volume-title":"computer security resource center","author":"National Institute for Standards and Technology","year":"2024","unstructured":"National Institute for Standards and Technology: computer security resource center. 2024. Post-Quantum Cryptography. https:\/\/csrc.nist.gov\/projects\/post-quantum-cryptography"},{"key":"e_1_3_2_2_20_1","unstructured":"GitHub. 2022. EasyCrypt. https:\/\/github.com\/EasyCrypt\/easycrypt"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","unstructured":"Katharina Heidler and Dominique Unruh. 2024. One-way to Hiding Formalization \u2013 Formalizing the O2H Theorem in Isabelle. https:\/\/doi.org\/10.5281\/zenodo.14278513 last accessed: 2024-12-04 to be published at AFP 10.5281\/zenodo.14278513","DOI":"10.5281\/zenodo.14278513"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11232-011-0010-5"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96878-0_4"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","unstructured":"Florian Kamm\u00fcller Markus Wenzel and Lawrence Paulson. 1999. Locales A Sectioning Concept for Isabelle. 839\u2013839. isbn:978-3-540-66463-5 https:\/\/doi.org\/10.1007\/3-540-48256-3_11 10.1007\/3-540-48256-3_11","DOI":"10.1007\/3-540-48256-3_11"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45727-3_24"},{"key":"e_1_3_2_2_26_1","unstructured":"Andreas Lochbihler. 2017. CryptHOL. Archive of Formal Proofs May issn:2150-914x https:\/\/isa-afp.org\/entries\/CryptHOL.html"},{"key":"e_1_3_2_2_27_1","unstructured":"Technische Universit\u00e4t M\u00fcnchen and Cambridge University. 2022. Isabelle. https:\/\/isabelle.in.tum.de\/index.html"},{"key":"e_1_3_2_2_28_1","volume-title":"Chuang","author":"Nielsen Michael A.","year":"2010","unstructured":"Michael A. Nielsen and Isaac L. Chuang. 2010. Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press."},{"volume-title":"Concrete Semantics with Isabelle\/HOL","author":"Nipkow Tobias","key":"e_1_3_2_2_29_1","unstructured":"Tobias Nipkow and Gerwin Klein. 2014. Concrete Semantics with Isabelle\/HOL. Springer. http:\/\/concrete-semantics.org"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow Lawrence Paulson and Markus Wenzel. 2002. Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic (LNCS Vol. 2283). Springer.","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44381-1_1"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-55220-5_8"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46803-6_25"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290346"},{"key":"e_1_3_2_2_35_1","unstructured":"Dominique Unruh. 2021. Quantum and Classical Registers. Archive of Formal Proofs October issn:2150-914x https:\/\/isa-afp.org\/entries\/Registers.html"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","unstructured":"Dominique Unruh. 2021. Quantum references. https:\/\/doi.org\/10.48550\/ARXIV.2105.10914 10.48550\/ARXIV.2105.10914","DOI":"10.48550\/ARXIV.2105.10914"},{"key":"e_1_3_2_2_37_1","unstructured":"Dominnique Unruh. 2024. Hilbert Space Tensor Product. https:\/\/github.com\/dominique-unruh\/afp\/tree\/unruh-edits\/thys\/Hilbert_Space_Tensor_Product"},{"key":"e_1_3_2_2_38_1","unstructured":"Dominique Unruh. 2024. qrhl-tool. https:\/\/github.com\/dominique-unruh\/qrhl-tool"},{"key":"e_1_3_2_2_39_1","volume-title":"The Theory of Quantum Information","author":"Watrous John","year":"1805","unstructured":"John Watrous. 2018. The Theory of Quantum Information. Cambridge University Press. isbn:9781107180567"}],"event":{"name":"CPP '25: 14th ACM SIGPLAN International Conference on Certified Programs and Proofs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG"],"location":"Denver CO USA","acronym":"CPP '25"},"container-title":["Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3703595.3705887","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3703595.3705887","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:18:08Z","timestamp":1750295888000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3703595.3705887"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,10]]},"references-count":39,"alternative-id":["10.1145\/3703595.3705887","10.1145\/3703595"],"URL":"https:\/\/doi.org\/10.1145\/3703595.3705887","relation":{},"subject":[],"published":{"date-parts":[[2025,1,10]]},"assertion":[{"value":"2025-01-10","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}