{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,25]],"date-time":"2026-02-25T12:26:21Z","timestamp":1772022381200,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":31,"publisher":"ACM","license":[{"start":{"date-parts":[[2008,10,27]],"date-time":"2008-10-27T00:00:00Z","timestamp":1225065600000},"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":[[2008,10,27]]},"DOI":"10.1145\/1455770.1455787","type":"proceedings-article","created":{"date-parts":[[2008,11,6]],"date-time":"2008-11-06T13:49:50Z","timestamp":1225979390000},"page":"119-128","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":36,"title":["Unbounded verification, falsification, and characterization of security protocols by pattern refinement"],"prefix":"10.1145","author":[{"given":"Cas J.F.","family":"Cremers","sequence":"first","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2008,10,27]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-007-0041-y"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_39"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2007.11"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-004-0055-7"},{"key":"e_1_3_2_1_5_1","unstructured":"S. Berezin. Extensions to Athena: Constraint satisfiability problem and new pruning theorems based on type system extensions for messages. http:\/\/www.sergeyberezin.com\/papers\/athena--extensions.ps (unpublished manuscript) 2001.  S. Berezin. Extensions to Athena: Constraint satisfiability problem and new pruning theorems based on type system extensions for messages. http:\/\/www.sergeyberezin.com\/papers\/athena--extensions.ps (unpublished manuscript) 2001."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/872752.873511"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/1145948.1145950"},{"key":"e_1_3_2_1_8_1","volume-title":"Proc. International Workshop on Automated Verification of Infinite-State Systems (AVIS'2004)","author":"Boichut Y.","unstructured":"Y. Boichut , P.-C. Heam , O. Kouchnarenko , and F. Oehl . Improvements on the Genet and Klay technique to automatically verify security protocols . In Proc. International Workshop on Automated Verification of Infinite-State Systems (AVIS'2004) . Y. Boichut, P.-C. Heam, O. Kouchnarenko, and F. Oehl. Improvements on the Genet and Klay technique to automatically verify security protocols. In Proc. International Workshop on Automated Verification of Infinite-State Systems (AVIS'2004)."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1029133.1029135"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/77648.77649"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/647171.718316"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/ARES.2006.63"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_38"},{"key":"e_1_3_2_1_14_1","volume-title":"Proc. of the 7th Int. Workshop on Automated Verification of Critical Systems (AVoCS'07)","author":"Cremers C.","year":"2007","unstructured":"C. Cremers and P. Lafourcade . Comparing state spaces in automatic protocol verification . In Proc. of the 7th Int. Workshop on Automated Verification of Critical Systems (AVoCS'07) , Electronic Notes in Theoretical Computer Science. Elsevier Science Direct , September 2007 . C. Cremers and P. Lafourcade. Comparing state spaces in automatic protocol verification. In Proc. of the 7th Int. Workshop on Automated Verification of Critical Systems (AVoCS'07), Electronic Notes in Theoretical Computer Science. Elsevier Science Direct, September 2007."},{"key":"e_1_3_2_1_15_1","volume-title":"Transformations and Tools, International Workshop","volume":"3466","author":"Cremers C.","year":"2003","unstructured":"C. Cremers and S. Mauw . Operational semantics of security protocols. In Scenarios: Models , Transformations and Tools, International Workshop , 2003 , Revised Selected Papers , volume 3466 of Lecture Notes in Computer Science. Springer, 2005. C. Cremers and S. Mauw. Operational semantics of security protocols. In Scenarios: Models, Transformations and Tools, International Workshop, 2003, Revised Selected Papers, volume 3466 of Lecture Notes in Computer Science. Springer, 2005."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.029"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_3_2_1_18_1","volume-title":"Proc. of the FLOC'99 Workshop on Formal Methods and Security Protocols (FMSP'99)","author":"Durgin N.","year":"1999","unstructured":"N. Durgin , P. Lincoln , J. Mitchell , and A. Scedrov . Undecidability of bounded security protocols . In Proc. of the FLOC'99 Workshop on Formal Methods and Security Protocols (FMSP'99) , 1999 . N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov. Undecidability of bounded security protocols. In Proc. of the FLOC'99 Workshop on Formal Methods and Security Protocols (FMSP'99), 1999."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.04.004"},{"key":"e_1_3_2_1_20_1","volume-title":"IST-2001-39252. AVISPA: Automated validation of internet security protocols and applications","author":"F. O.","year":"2003","unstructured":"F. O. P. IST-2001-39252. AVISPA: Automated validation of internet security protocols and applications , 2003 . F. O. P. IST-2001-39252. AVISPA: Automated validation of internet security protocols and applications, 2003."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/646480.693776"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/794197.795076"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(95)00095-X"},{"key":"e_1_3_2_1_24_1","volume-title":"ETH Zurich","author":"Meier S.","year":"2007","unstructured":"S. Meier . A formalization of an operational semantics of security protocols. Diploma thesis , ETH Zurich , August 2007 . http:\/\/people.inf.ethz.ch\/meiersi\/fossp\/index.html. S. Meier. A formalization of an operational semantics of security protocols. Diploma thesis, ETH Zurich, August 2007. http:\/\/people.inf.ethz.ch\/meiersi\/fossp\/index.html."},{"key":"e_1_3_2_1_25_1","volume-title":"Workshop on Formal Methods and Security Protocols","author":"Millen J.","year":"1999","unstructured":"J. Millen . A necessarily parallel attack . In Workshop on Formal Methods and Security Protocols , Trento, Italy , 1999 . J. Millen. A necessarily parallel attack. In Workshop on Formal Methods and Security Protocols, Trento, Italy, 1999."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/353677.353681"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/322510.322530"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/374742.374749"},{"key":"e_1_3_2_1_29_1","unstructured":"Security protocols open repository (SPORE). http:\/\/www.lsv.ens-cachan.fr\/spore.  Security protocols open repository (SPORE). http:\/\/www.lsv.ens-cachan.fr\/spore."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/353594.353603"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/11805618_21"}],"event":{"name":"CCS08: 15th ACM Conference on Computer and Communications Security 2008","location":"Alexandria Virginia USA","acronym":"CCS08","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the 15th ACM conference on Computer and communications security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1455770.1455787","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1455770.1455787","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:14Z","timestamp":1750287254000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1455770.1455787"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,10,27]]},"references-count":31,"alternative-id":["10.1145\/1455770.1455787","10.1145\/1455770"],"URL":"https:\/\/doi.org\/10.1145\/1455770.1455787","relation":{},"subject":[],"published":{"date-parts":[[2008,10,27]]},"assertion":[{"value":"2008-10-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}