{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,7]],"date-time":"2026-07-07T02:54:07Z","timestamp":1783392847866,"version":"3.54.6"},"reference-count":29,"publisher":"IEEE","license":[{"start":{"date-parts":[[2026,3,17]],"date-time":"2026-03-17T00:00:00Z","timestamp":1773705600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2026,3,17]],"date-time":"2026-03-17T00:00:00Z","timestamp":1773705600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62402371,62192734,62302375,62402372,62193273024"],"award-info":[{"award-number":["62402371,62192734,62302375,62402372,62193273024"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026,3,17]]},"DOI":"10.1109\/saner67736.2026.00103","type":"proceedings-article","created":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T19:41:17Z","timestamp":1783021277000},"page":"1-6","source":"Crossref","is-referenced-by-count":1,"title":["How Well Does Knowledge Injection Enhance LLM-Aided Formal Protocol Modeling?"],"prefix":"10.1109","author":[{"given":"Yajia","family":"Lin","sequence":"first","affiliation":[{"name":"Xidian University,China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jie","family":"Su","sequence":"additional","affiliation":[{"name":"Xidian University,China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cheng","family":"Wen","sequence":"additional","affiliation":[{"name":"Xidian University,China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rong","family":"Wang","sequence":"additional","affiliation":[{"name":"Guangdong Polytechnic Normal University,China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cong","family":"Tian","sequence":"additional","affiliation":[{"name":"Xidian University,China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhenhua","family":"Dun","sequence":"additional","affiliation":[{"name":"Xidian University,China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shengchao","family":"Qin","sequence":"additional","affiliation":[{"name":"Xidian University,China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref1","article-title":"Survey on secure communication protocols for the internet of things","author":"Nguyen","journal-title":"Ad Hoc Networks, vol. 32, pp. 17\u201331, 2015, internet of Things security and privacy: design methods and optimization."},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1561\/3300000004"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.3233\/jcs-2004-12203"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134063"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243846"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.3233\/jcs-160556"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/3744746"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/icse55347.2025.00197"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/3626111.3628205"},{"key":"ref11","volume-title":"Cryptoformaleval: Integrating 11 ms and formal verification for automated cryptographic protocol vulnerability detection","author":"Curaba","year":"2024"},{"key":"ref12","volume-title":"Retrieval-augmented generation for large language models: A survey","author":"Gao","year":"2024"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-020-09360-1"},{"key":"ref14","volume-title":"Tamgram: A frontend for large-scale protocol modeling in tamarin","author":"Li","year":"2024"},{"key":"ref15","volume-title":"Model-driven engineering for formal verification and security testing of authentication protocols","author":"Raimondo","year":"2022"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1038\/s41598-025-93373-y"},{"key":"ref17","article-title":"Ephemeral DiffieHellman Over COSE (EDHOC)","volume-title":"RFC 9528","author":"Selander","year":"2024"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17143-7_4"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/11745853_25"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24852-1_16"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22497-3_23"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-75670-5_1"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/csfw.1996.503701"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/bf00196790"},{"key":"ref25","first-page":"67","article-title":"Secure Mobile RFID system against privacy and security problems","volume-title":"Security, Privacy and Trust in Pervasive and Ubiquitous Computing, International Workshop on","author":"Lee","year":"2007"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1109\/csf.2011.12"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1023\/a:1010056221226"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00028"},{"key":"ref29","volume-title":"Advancing the formal foundations for voting protocols","author":"Schmid","year":"2020"}],"event":{"name":"2026 IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER)","location":"Limassol, Cyprus","start":{"date-parts":[[2026,3,17]]},"end":{"date-parts":[[2026,3,20]]}},"container-title":["2026 IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/11576582\/11576527\/11576645.pdf?arnumber=11576645","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,3]],"date-time":"2026-07-03T05:40:25Z","timestamp":1783057225000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11576645\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,3,17]]},"references-count":29,"URL":"https:\/\/doi.org\/10.1109\/saner67736.2026.00103","relation":{},"subject":[],"published":{"date-parts":[[2026,3,17]]}}}