{"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":1750309522651,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":19,"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":"FCT - Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia","award":["LA\\\/P\\\/0063\\\/2020"],"award-info":[{"award-number":["LA\\\/P\\\/0063\\\/2020"]}]},{"name":"Estonian Research Council","award":["PSG749"],"award-info":[{"award-number":["PSG749"]}]},{"name":"Estonian Research Council","award":["819317"],"award-info":[{"award-number":["819317"]}]},{"name":"Estonian Centre of Excellence in IT","award":["TK148"],"award-info":[{"award-number":["TK148"]}]},{"name":"Estonian Centre of Excellence","award":["TK202"],"award-info":[{"award-number":["TK202"]}]},{"name":"Estonian Research Council","award":["PRG946"],"award-info":[{"award-number":["PRG946"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,1,10]]},"DOI":"10.1145\/3703595.3705871","type":"proceedings-article","created":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T21:23:16Z","timestamp":1736544196000},"page":"3-16","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Leakage-Free Probabilistic Jasmin Programs"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0011-7455","authenticated-orcid":false,"given":"Jos\u00e9","family":"Bacelar Almeida","sequence":"first","affiliation":[{"name":"HASLAB\/INESCTEC, Braga, Portugal"},{"name":"University of Minho, Braga, Portugal"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1267-7898","authenticated-orcid":false,"given":"Denis","family":"Firsov","sequence":"additional","affiliation":[{"name":"Tallinn University of Technology, Tallinn, Estonia"},{"name":"Input Output, Tallinn, Estonia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7395-3070","authenticated-orcid":false,"given":"Tiago","family":"Oliveira","sequence":"additional","affiliation":[{"name":"SandboxAQ, Palo Alto, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8965-1931","authenticated-orcid":false,"given":"Dominique","family":"Unruh","sequence":"additional","affiliation":[{"name":"University of Tartu, Tartu, Estonia"},{"name":"RWTH Aachen, Aachen, Germany"}]}],"member":"320","published-online":{"date-parts":[[2025,1,10]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134078"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00028"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.46586\/TCHES.V2023.I3.164-193"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484771"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3363211"},{"key":"e_1_3_2_2_6_1","unstructured":"Jos\u00e9 Bacelar Almeida Denis Firsov Tiago Oliveira and Dominique Unruh. 2024. Accompanying EasyCrypt Development. https:\/\/github.com\/dfirsov\/jasmin-leakage-freeness Accessed: 2025-12-03"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","unstructured":"Jos\u00e9 Bacelar Almeida Denis Firsov Tiago Oliveira and Dominique Unruh. 2024. Archived Accompanying EasyCrypt Development. https:\/\/doi.org\/10.5281\/zenodo.14281008 Accessed: 2025-12-05 10.5281\/zenodo.14281008","DOI":"10.5281\/zenodo.14281008"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","unstructured":"Jos\u00e9 Bacelar Almeida Santiago Arranz Olmos Manuel Barbosa Gilles Barthe Fran\u00e7ois Dupressoir Benjamin Gr\u00e9goire Vincent Laporte Jean-Christophe L\u00e9chenet Cameron Low Tiago Oliveira Hugo Pacheco Miguel Quaresma Peter Schwabe and Pierre-Yves Strub. 2024. Formally Verifying Kyber - Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt. In Advances in Cryptology - CRYPTO 2024 - 44th Annual International Cryptology Conference Santa Barbara CA USA August 18-22 2024 Proceedings Part II Leonid Reyzin and Douglas Stebila (Eds.) (Lecture Notes in Computer Science Vol. 14921). Springer 384\u2013421. https:\/\/doi.org\/10.1007\/978-3-031-68379-4_12 10.1007\/978-3-031-68379-4_12","DOI":"10.1007\/978-3-031-68379-4_12"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88313-5_22"},{"volume-title":"EasyCrypt: A Tutorial","author":"Barthe Gilles","key":"e_1_3_2_2_10_1","unstructured":"Gilles Barthe, Fran\u00e7ois Dupressoir, Benjamin Gr\u00e9goire, C\u00e9sar Kunz, Benedikt Schmidt, and Pierre-Yves Strub. 2013. EasyCrypt: A Tutorial. In Foundations of Security Analysis and Design VII. Springer, 146\u2013166."},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.29007\/VZ48"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22792-9_5"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484761"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2013.20"},{"volume-title":"ML-DSA: Module-Lattice-Based Digital Signature Standard","author":"NIST Computer Security Division","key":"e_1_3_2_2_15_1","unstructured":"NIST Computer Security Division. 2024. ML-DSA: Module-Lattice-Based Digital Signature Standard. National Institute of Standards and Technology, U.S. Department of Commerce. https:\/\/csrc.nist.gov\/pubs\/fips\/204\/final"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3497775.3503693"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46215.2023.10179418"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3548606.3560689"}],"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.3705871","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3703595.3705871","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.3705871"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,10]]},"references-count":19,"alternative-id":["10.1145\/3703595.3705871","10.1145\/3703595"],"URL":"https:\/\/doi.org\/10.1145\/3703595.3705871","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"}}]}}