{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,7]],"date-time":"2026-03-07T00:07:16Z","timestamp":1772842036251,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":57,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,11,13]],"date-time":"2021-11-13T00:00:00Z","timestamp":1636761600000},"content-version":"vor","delay-in-days":1,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"AFOSR","award":["FA95502110094"],"award-info":[{"award-number":["FA95502110094"]}]},{"DOI":"10.13039\/100000001","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["NSF-CCF-1942837"],"award-info":[{"award-number":["NSF-CCF-1942837"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,11,12]]},"DOI":"10.1145\/3460120.3484567","type":"proceedings-article","created":{"date-parts":[[2021,11,13]],"date-time":"2021-11-13T12:05:27Z","timestamp":1636805127000},"page":"2564-2586","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":23,"title":["EasyPQC: Verifying Post-Quantum Cryptography"],"prefix":"10.1145","author":[{"given":"Manuel","family":"Barbosa","sequence":"first","affiliation":[{"name":"University of Porto (FCUP) and INESC TEC, Porto, Portugal"}]},{"given":"Gilles","family":"Barthe","sequence":"additional","affiliation":[{"name":"MPI-SP and IMDEA Software Institute, Bochum, Germany"}]},{"given":"Xiong","family":"Fan","sequence":"additional","affiliation":[{"name":"Algorand, Inc., Boston, MA, USA"}]},{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[{"name":"INRIA, Sophia-Antipolis, France"}]},{"given":"Shih-Han","family":"Hung","sequence":"additional","affiliation":[{"name":"University of Texas, Austin, TX, USA"}]},{"given":"Jonathan","family":"Katz","sequence":"additional","affiliation":[{"name":"University of Maryland, College Park, MD, USA"}]},{"given":"Pierre-Yves","family":"Strub","sequence":"additional","affiliation":[{"name":"\u00c9cole Polytechnique, Paris, France"}]},{"given":"Xiaodi","family":"Wu","sequence":"additional","affiliation":[{"name":"University of Maryland, College Park, MD, USA"}]},{"given":"Li","family":"Zhou","sequence":"additional","affiliation":[{"name":"MPI-SP, Bochum, Ghana"}]}],"member":"320","published-online":{"date-parts":[[2021,11,13]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3-030--26951--7_10"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00078"},{"key":"e_1_3_2_1_3_1","unstructured":"Manuel Barbosa Gilles Barthe Karthik Bhargavan Bruno Blanchet Cas Cremers Kevin Liao and Bryan Parno. 2019. SoK: Computer-Aided Cryptography. Cryptology ePrint Archive Report 2019\/1393. (2019). https:\/\/eprint.iacr.org\/2019\/1393."},{"key":"e_1_3_2_1_4_1","first-page":"156","article-title":"Mechanized Proofs of Adversarial Complexity and Application to Universal Composability","volume":"2021","author":"Barbosa Manuel","year":"2021","unstructured":"Manuel Barbosa, Gilles Barthe, Benjamin Gr\u00e9 goire, Adrien Koutsos, and Pierre-Yves Strub. 2021. Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. IACR Cryptol. ePrint Arch., Vol. 2021 (2021), 156. https:\/\/eprint.iacr.org\/2021\/156","journal-title":"IACR Cryptol. ePrint Arch."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3--319--10082--1_6"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3--662--48899--7_27"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243825"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3--642--22792--9_5"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371089"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/168588.168596"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/3--540--68339--9_34"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3-030--36033--7_3"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2006.1"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25385-0_3"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/3--540--44647--8_13"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3--642--38348--9_35"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-020-09584--7"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.04.003"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Kai-Min Chung Serge Fehr Yu-Hsuan Huang and Tai-Ning Liao. 2021. On the Compressed-Oracle Technique and Post-Quantum Security of Proofs of Sequential Work. (2021). arxiv: quant-ph\/2010.11658","DOI":"10.1007\/978-3-030-77886-6_21"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/3--540--44598--6_14"},{"key":"e_1_3_2_1_22_1","volume-title":"Quantum logic. Handbook of philosophical logic","author":"Dalla Chiara Maria Luisa","unstructured":"Maria Luisa Dalla Chiara. 1986. Quantum logic. Handbook of philosophical logic. Springer, 427--469."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005251"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3-030--26951--7_13"},{"key":"e_1_3_2_1_25_1","unstructured":"Yuan Feng and Mingsheng Ying. 2020. Quantum Hoare logic with classical variables. (2020). arxiv: cs.LO\/2008.06812"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1374376.1374407"},{"key":"e_1_3_2_1_27_1","unstructured":"Kesha Hietala Robert Rand Shih-Han Hung Liyi Li and Michael Hicks. 2020. Proving Quantum Programs Correct. (2020). arxiv: cs.PL\/2010.01240"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434318"},{"key":"e_1_3_2_1_29_1","volume-title":"Symbolic Abstractions for Quantum Protocol Verification. CoRR","author":"Hirschi Lucca","year":"2019","unstructured":"Lucca Hirschi. 2019. Symbolic Abstractions for Quantum Protocol Verification. CoRR, Vol. abs\/1904.04186 (2019). arxiv: 1904.04186 http:\/\/arxiv.org\/abs\/1904.04186"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290344"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10622-4_7"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0219025716500120"},{"key":"e_1_3_2_1_33_1","unstructured":"Yangjia Li and Dominique Unruh. 2019. Quantum Relational Hoare Logic with Expectations. (2019). arxiv: cs.LO\/1903.08357"},{"key":"e_1_3_2_1_34_1","volume-title":"Lectures on the coupling method","author":"Lindvall Torgny","unstructured":"Torgny Lindvall. 2002. Lectures on the coupling method .Courier Corporation."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3-030--25543--5_12"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3-030--26951--7_12"},{"key":"e_1_3_2_1_37_1","unstructured":"Robert Rand. 2019. Verification Logics for Quantum Programs. (2019). arxiv: cs.LO\/1904.04304"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1060590.1060603"},{"key":"e_1_3_2_1_39_1","volume-title":"QWIRE Practice: Formal Verification of Quantum Circuits in Coq. In 14th International Conference on Quantum Physics and Logic 2017 (QPL '17)","author":"Robert Rand Steve Zdancewic","year":"2017","unstructured":"Steve Zdancewic Robert Rand, Jennifer Paykin. 2017. QWIRE Practice: Formal Verification of Quantum Circuits in Coq. In 14th International Conference on Quantum Physics and Logic 2017 (QPL '17). https:\/\/qpl.science.ru.nl\/papers\/QPL_2017_paper_45.pdf"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"e_1_3_2_1_41_1","volume-title":"Workshop on the theory and application of cryptographic techniques. Springer, 47--53","author":"Shamir Adi","year":"1984","unstructured":"Adi Shamir. 1984. Identity-based cryptosystems and signature schemes. In Workshop on the theory and application of cryptographic techniques. Springer, 47--53."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3--319--11659--4_15"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"crossref","unstructured":"Hermann Thorisson. 2000. Coupling Stationarity and Regeneration .springer.","DOI":"10.1007\/978-1-4612-1236-2"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2817206"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785779"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290346"},{"key":"e_1_3_2_1_47_1","unstructured":"Dominique Unruh. 2020. Local Variables and Quantum Relational Hoare Logic. (2020). arxiv: cs.LO\/2007.14155"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"crossref","unstructured":"C\u00e9dric Villani. 2008. Optimal transport: Old and new .springer.","DOI":"10.1007\/978-3-540-71050-9"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00220-016-2609-8"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_3_2_1_51_1","unstructured":"Mingsheng Ying Li Zhou and Yangjia Li. 2018. Reasoning about Parallel Quantum Programs. (2018). arxiv: cs.LO\/1810.11334"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2012.37"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3--642--32009--5_44"},{"key":"e_1_3_2_1_54_1","unstructured":"Mark Zhandry. 2015. Cryptography in the Age of Quantum Computers. Ph.D. Dissertation. Stanford University. https:\/\/www.cs.princeton.edu\/ mzhandry"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-26951-7_9"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"crossref","unstructured":"Li Zhou Gilles Barthe Justin Hsu Mingsheng Ying and Nengkun Yu. 2021. A Quantum Interpretation of Bunched Logic for Quantum Separation Logic. (2021). arxiv: cs.LO\/2102.00329","DOI":"10.1109\/LICS52264.2021.9470673"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.08.026"}],"event":{"name":"CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications Security","location":"Virtual Event Republic of Korea","acronym":"CCS '21","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3460120.3484567","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3460120.3484567","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3460120.3484567","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T20:44:23Z","timestamp":1763498663000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3460120.3484567"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11,12]]},"references-count":57,"alternative-id":["10.1145\/3460120.3484567","10.1145\/3460120"],"URL":"https:\/\/doi.org\/10.1145\/3460120.3484567","relation":{},"subject":[],"published":{"date-parts":[[2021,11,12]]},"assertion":[{"value":"2021-11-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}