{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:18:29Z","timestamp":1750306709425,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":26,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,7,21]],"date-time":"2014-07-21T00:00:00Z","timestamp":1405900800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2014,7,21]]},"DOI":"10.1145\/2632362.2632378","type":"proceedings-article","created":{"date-parts":[[2014,7,11]],"date-time":"2014-07-11T12:10:42Z","timestamp":1405080642000},"page":"77-86","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Generic and efficient attacker models in SPIN"],"prefix":"10.1145","author":[{"given":"Noomene","family":"Ben Henda","sequence":"first","affiliation":[{"name":"Ericsson Research, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,7,21]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"3GPP The Mobile Broadband Standard. http:\/\/www.3gpp.org\/specifications\/. 3GPP The Mobile Broadband Standard. http:\/\/www.3gpp.org\/specifications\/."},{"volume-title":"Computer Security Foundations Workshop (CSFW \u201997)","year":"1997","key":"e_1_3_2_1_2_1"},{"volume-title":"IEEE Computer Security Foundations Workshop (CSFW-14 2001)","year":"2001","key":"e_1_3_2_1_3_1"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"M. Abadi B. Blanchet and C. Fournet . Just fast keying in the pi calculus. In D. A. Schmidt editor ESOP volume 2986 of Lecture Notes in Computer Science pages 340\u2013 354 . Springer 2004. M. Abadi B. Blanchet and C. Fournet. Just fast keying in the pi calculus. In D. A. Schmidt editor ESOP volume 2986 of Lecture Notes in Computer Science pages 340\u2013354. Springer 2004.","DOI":"10.1007\/978-3-540-24725-8_24"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360213"},{"first-page":"96","volume-title":"CSFW {3}","author":"Blanchet B.","key":"e_1_3_2_1_6_1"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/1576303.1576304"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/2412048"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_38"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-01957-9_2"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"crossref","unstructured":"C. J. F. Cremers . Key exchange in ipsec revisited: Formal analysis of ikev1 and ikev2. In V. Atluri and C. D\u00b4\u0131az editors ESORICS volume 6879 of Lecture Notes in Computer Science pages 315\u2013 334 . Springer 2011. C. J. F. Cremers. Key exchange in ipsec revisited: Formal analysis of ikev1 and ikev2. In V. Atluri and C. D\u00b4\u0131az editors ESORICS volume 6879 of Lecture Notes in Computer Science pages 315\u2013334. Springer 2011.","DOI":"10.1007\/978-3-642-23822-2_18"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/358722.358740"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/1017273.1017276"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/646139.680779"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11537328_18"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","unstructured":"G. Lowe . Breaking and fixing the needham-schroeder public-key protocol using fdr. In T. Margaria and B. Steffen editors TACAS volume 1055 of Lecture Notes in Computer Science pages 147\u2013 166 . Springer 1996. G. Lowe. Breaking and fixing the needham-schroeder public-key protocol using fdr. In T. Margaria and B. Steffen editors TACAS volume 1055 of Lecture Notes in Computer Science pages 147\u2013166. Springer 1996.","DOI":"10.1007\/3-540-61042-1_43"},{"first-page":"30","volume-title":"CSFW {2}","author":"Lowe G.","key":"e_1_3_2_1_19_1"},{"first-page":"44","volume-title":"CSFW {2}","author":"Lowe G.","key":"e_1_3_2_1_20_1"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"crossref","unstructured":"P. Maggi and R. Sisto . Using spin to verify security properties of cryptographic protocols. In D. Bosnacki and S. Leue editors SPIN volume 2318 of Lecture Notes in Computer Science pages 187\u2013 204 . Springer 2002. P. Maggi and R. Sisto. Using spin to verify security properties of cryptographic protocols. In D. Bosnacki and S. Leue editors SPIN volume 2318 of Lecture Notes in Computer Science pages 187\u2013204. Springer 2002.","DOI":"10.1007\/3-540-46017-9_14"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958047"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/359657.359659"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"crossref","unstructured":"M. Rusinowitch and M. Turuani. Protocol insecurity with finite number of sessions is np-complete. In CSFW {3} pages 174\u2013. M. Rusinowitch and M. Turuani. Protocol insecurity with finite number of sessions is np-complete. In CSFW {3} pages 174\u2013.","DOI":"10.1109\/CSFW.2001.930145"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"crossref","unstructured":"C. Tang D. A. Naumann and S. Wetzel . Symbolic analysis for security of roaming protocols in mobile networks - {extended abstract}. In M. Rajarajan F. Piper H. Wang and G. Kesidis editors SecureComm volume 96 of Lecture Notes of the Institute for Computer Sciences Social Informatics and Telecommunications Engineering pages 480\u2013 490 . Springer 2011. C. Tang D. A. Naumann and S. Wetzel. Symbolic analysis for security of roaming protocols in mobile networks - {extended abstract}. In M. Rajarajan F. Piper H. Wang and G. Kesidis editors SecureComm volume 96 of Lecture Notes of the Institute for Computer Sciences Social Informatics and Telecommunications Engineering pages 480\u2013490. Springer 2011.","DOI":"10.1007\/978-3-642-31909-9_29"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"crossref","unstructured":"M. Tatebayashi N. Matsuzaki and D. B. N. Jr . Key distribution protocol for digital mobile communication systems. In G. Brassard editor CRYPTO volume 435 of Lecture Notes in Computer Science pages 324\u2013 334 . Springer 1989. M. Tatebayashi N. Matsuzaki and D. B. N. Jr. Key distribution protocol for digital mobile communication systems. In G. Brassard editor CRYPTO volume 435 of Lecture Notes in Computer Science pages 324\u2013334. Springer 1989.","DOI":"10.1007\/0-387-34805-0_30"}],"event":{"name":"ISSTA '14: International Symposium on Software Testing and Analysis","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"San Jose CA USA","acronym":"ISSTA '14"},"container-title":["Proceedings of the 2014 International SPIN Symposium on Model Checking of Software"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2632362.2632378","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2632362.2632378","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:19:14Z","timestamp":1750231154000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2632362.2632378"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,7,21]]},"references-count":26,"alternative-id":["10.1145\/2632362.2632378","10.1145\/2632362"],"URL":"https:\/\/doi.org\/10.1145\/2632362.2632378","relation":{},"subject":[],"published":{"date-parts":[[2014,7,21]]},"assertion":[{"value":"2014-07-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}