{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T21:30:19Z","timestamp":1773264619720,"version":"3.50.1"},"reference-count":37,"publisher":"IEEE","license":[{"start":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T00:00:00Z","timestamp":1762905600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T00:00:00Z","timestamp":1762905600000},"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":[[2025,11,12]]},"DOI":"10.1109\/icdmw69685.2025.00143","type":"proceedings-article","created":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T19:50:39Z","timestamp":1773172239000},"page":"1210-1216","source":"Crossref","is-referenced-by-count":0,"title":["Autoformalization of Cryptographic Protocols"],"prefix":"10.1109","author":[{"given":"Lauren","family":"Brandt","sequence":"first","affiliation":[{"name":"The MITRE Corporation,Virginia,USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joshua","family":"Guttman","sequence":"additional","affiliation":[{"name":"The MITRE Corporation,Virginia,USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andres","family":"Molina-Markham","sequence":"additional","affiliation":[{"name":"The MITRE Corporation,Virginia,USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref1","year":"2024","journal-title":"The transport layer security (TLS) protocol version 1.3"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-016-0319-z"},{"key":"ref3","volume-title":"Tamarin-Prover Manual: Security Protocol Analysis in the Symbolic Model","year":"2024"},{"key":"ref4","author":"Blanchet","year":"2023","journal-title":"ProVerif 2.05: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial"},{"key":"ref5","author":"Liskov","year":"2023","journal-title":"The Cryptographic Protocol Shapes Analyzer: A Manual for CPSA 4"},{"key":"ref6","author":"Song","year":"2025","journal-title":"Lean copilot: Large language models as copilots for theorem proving in Lean"},{"key":"ref7","doi-asserted-by":"crossref","DOI":"10.1109\/ICSE55347.2025.00022","article-title":"Rustassistant: Using LLMs to fix compilation errors in Rust code","volume-title":"47th International Conference on Software Engineering (ICSE)","author":"Deligiannis"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-91631-2_20"},{"key":"ref9","article-title":"Molly: A verified compiler for cryptoprotocol roles","volume-title":"CoRR","volume":"abs\/2311.13692","author":"Dougherty","year":"2023"},{"key":"ref10","journal-title":"Usable formal methods research group UFMRG"},{"key":"ref11","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-3-030-58298-2_1","article-title":"The2020 expert survey on formal methods","volume-title":"Formal Methods for Industrial Critical Systems","author":"Garavel","year":"2020"},{"key":"ref12","volume-title":"Discussion on formal methods usability","author":"Sardar","year":"2024"},{"key":"ref13","volume-title":"Discussion on formal methods usability","author":"Hoyland","year":"2024"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06410-9_2"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53518-6_1"},{"key":"ref16","author":"Wu","year":"2022","journal-title":"Autoformalization with large language models"},{"key":"ref17","author":"Nipkow","year":"2025","journal-title":"A Proof Assistant for Higher-Order Logic"},{"key":"ref18","author":"Azerbayev","year":"2023","journal-title":"ProofNet: Autoformalizing and formally proving undergraduate-level mathematics"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"ref21","author":"Curaba","year":"2024","journal-title":"CryptoFormalEval: Integrating LLMs and formal verification for automated cryptographic protocol vulnerability detection"},{"key":"ref22","doi-asserted-by":"crossref","first-page":"11866","DOI":"10.1038\/s41598-025-93373-y","article-title":"Constructing formal models of cryptographic protocols from Alice&Bob style specifications via 11 m","author":"Li","year":"2025","journal-title":"Scientific Reports"},{"key":"ref23","author":"Liu","year":"2023","journal-title":"Fimo: A challenge formal dataset for automated theorem proving"},{"key":"ref24","author":"Lu","year":"2025","journal-title":"Process-driven autoformalization in lean 4"},{"key":"ref25","author":"Pathak","year":"2024","journal-title":"Gflean: An autoformalisation framework for lean via gf"},{"key":"ref26","author":"First","year":"2023","journal-title":"Baldur: Whole-proof generation and repair with large language models"},{"key":"ref27","article-title":"Formalizing soundness proofs of SNARKs","author":"Bailey","year":"2023","journal-title":"Cryptology ePrint Archive"},{"key":"ref28","author":"Liu","year":"2023","journal-title":"Llm+p: Empowering large language models with optimal planning proficiency"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28641-4_2"},{"key":"ref30","article-title":"X. 509 Recommendation - The Directory: Authentication Framework (Part 3)","year":"1987","journal-title":"SPore project, ENS Paris-Saclay"},{"key":"ref31","article-title":"Fluffy: Simplified Key Exchange for Constrained Environments","author":"Hardjono","year":"2016","journal-title":"Internet-Draft draft-hardjono-ace-fluffy03, IETF"},{"key":"ref32","volume-title":"Information technology - Security techniques - Entity authentication - Part 2: Mechanisms using symmetric encipherment algorithms","year":"2008"},{"key":"ref33","volume-title":"Information technology - Security techniques - Entity authentication - Part 3: Mechanisms using digital signature techniques - Amendment 1","year":"2010"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1137\/0218082"},{"key":"ref35","author":"Brown","year":"2020","journal-title":"Language models are few-shot learners"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.1998.683159"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1145\/359657.359659"}],"event":{"name":"2025 IEEE International Conference on Data Mining Workshops (ICDMW)","location":"Washington, DC, USA","start":{"date-parts":[[2025,11,12]]},"end":{"date-parts":[[2025,11,15]]}},"container-title":["2025 IEEE International Conference on Data Mining Workshops (ICDMW)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/11415623\/11415713\/11416409.pdf?arnumber=11416409","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T05:29:05Z","timestamp":1773206945000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11416409\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,12]]},"references-count":37,"URL":"https:\/\/doi.org\/10.1109\/icdmw69685.2025.00143","relation":{},"subject":[],"published":{"date-parts":[[2025,11,12]]}}}