{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,14]],"date-time":"2026-07-14T20:09:35Z","timestamp":1784059775232,"version":"3.55.0"},"reference-count":58,"publisher":"IEEE","license":[{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026,5,18]]},"DOI":"10.1109\/sp63933.2026.00026","type":"proceedings-article","created":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T19:34:20Z","timestamp":1782934460000},"page":"1822-1841","source":"Crossref","is-referenced-by-count":0,"title":["The Secrets Must Not Flow: Scaling Security Verification to Large Codebases"],"prefix":"10.1109","author":[{"given":"Linard","family":"Arquint","sequence":"first","affiliation":[{"name":"ETH Zurich,Department of Computer Science,Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Samarth","family":"Kishor","sequence":"additional","affiliation":[{"name":"Amazon Web Services,USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jason R.","family":"Koenig","sequence":"additional","affiliation":[{"name":"Amazon Web Services,USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joey","family":"Dodds","sequence":"additional","affiliation":[{"name":"Amazon Web Services,USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[{"name":"Amazon Web Services,USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[{"name":"ETH Zurich,Department of Computer Science,Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref1","article-title":"The secrets must not flow: Scaling security verification to large codebases (extended version)","volume":"abs\/2507.00595","author":"Arquint","year":"2025","journal-title":"CoRR"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2012.25"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2001.930138"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.26"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00037"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2017.38"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243846"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2019.23394"},{"key":"ref10","year":"2021","journal-title":"CVE-2021\u201340823"},{"key":"ref11","year":"2022","journal-title":"CVE-2022-22805"},{"key":"ref12","year":"2022","journal-title":"CVE-2022-22806"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2011.8"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/SP46215.2023.10179325"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3623105"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"ref17","year":"2024","journal-title":"CVE-2024-47083"},{"key":"ref18","year":"2023","journal-title":"CVE-2023-6746"},{"key":"ref19","article-title":"Usable auto-active verification","volume-title":"Usable Verification Workshop","author":"Leino"},{"key":"ref20","volume-title":"Working with SSM Agent","year":"2023"},{"key":"ref21","volume-title":"The secrets must not flow: Scaling security verification to large codebases (artifact)","author":"Arquint","year":"2025"},{"key":"ref22","volume-title":"The secrets must not flow: Scaling security verification to large codebases. Artifact repository containing the protocol models, the forked SSM Agent\u2019s codebase, a DH implementation codebase, and the static analysis tools","author":"Arquint"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_17"},{"key":"ref24","volume-title":"Argot","author":"Labs","year":"2024"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-71162-6_2"},{"key":"ref27","first-page":"1857","article-title":"A spectral analysis of Noise: A comprehensive, automated, formal analysis of Diffie-Hellman protocols","volume-title":"USENIX Security Symposium","author":"Girol"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_4"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040326"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9457-5"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_33"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_7"},{"key":"ref35","volume-title":"Capslock","year":"2024"},{"key":"ref36","volume-title":"Astr\u00e9e static analyzer for C and C++","year":"2025"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00114"},{"key":"ref38","volume-title":"The Go memory model","year":"2022"},{"key":"ref39","article-title":"Sound verification of security protocols: From design to interoperable implementations (extended version)","volume":"abs\/2212.04171","author":"Arquint","year":"2022","journal-title":"CoRR"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.09.029"},{"key":"ref41","volume-title":"AWS Key Management Service","year":"2024"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00008"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0269-9"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28641-4_2"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1109\/AINA.2004.1283943"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1109\/ARES.2012.63"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP51992.2021.00042"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1109\/SP46215.2023.10179477"},{"key":"ref49","first-page":"5071","article-title":"OwlC: Compiling security protocols to verified, secure, high-performance libraries","volume-title":"USENIX Security Symposium","author":"Singh"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1145\/1452044.1452049"},{"key":"ref51","article-title":"Using Elyjah to analyse Java implementations of cryptographic protocols","author":"O\u2019Shea","year":"2008","journal-title":"FCS-ARSPA-WITS-2008"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1145\/2382196.2382271"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676972"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833621"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-73721-8_2"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1145\/3428296"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1145\/3632916"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1145\/3747522"}],"event":{"name":"2026 IEEE Symposium on Security and Privacy (SP)","location":"San Francisco, CA, USA","start":{"date-parts":[[2026,5,18]]},"end":{"date-parts":[[2026,5,21]]}},"container-title":["2026 IEEE Symposium on Security and Privacy (SP)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/11573355\/11573356\/11573428.pdf?arnumber=11573428","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,14]],"date-time":"2026-07-14T19:38:03Z","timestamp":1784057883000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11573428\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,5,18]]},"references-count":58,"URL":"https:\/\/doi.org\/10.1109\/sp63933.2026.00026","relation":{},"subject":[],"published":{"date-parts":[[2026,5,18]]}}}