{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,3]],"date-time":"2026-05-03T11:00:29Z","timestamp":1777806029963,"version":"3.51.4"},"reference-count":36,"publisher":"SAGE Publications","issue":"6","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["JCS"],"published-print":{"date-parts":[[2017,8,24]]},"DOI":"10.3233\/jcs-16832","type":"journal-article","created":{"date-parts":[[2017,8,11]],"date-time":"2017-08-11T11:31:20Z","timestamp":1502451080000},"page":"463-510","source":"Crossref","is-referenced-by-count":2,"title":["An interpolation-based method for the verification of security protocols"],"prefix":"10.1177","volume":"25","author":[{"given":"Marco","family":"Rocchetto","sequence":"first","affiliation":[{"name":"ALES, United Technologies Research Center, Italy. E-mail:\u00a0marco.rocchetto@utrc.utc.com"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"Vigan\u00f2","sequence":"additional","affiliation":[{"name":"Department of Informatics, King\u2019s College London, UK. E-mail:\u00a0luca.vigano@kcl.ac.uk"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Volpe","sequence":"additional","affiliation":[{"name":"INRIA and LIX, \u00c9cole Polytechnique, France. E-mail:\u00a0marco.volpe@inria.fr"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","reference":[{"key":"10.3233\/JCS-16832_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_19"},{"key":"10.3233\/JCS-16832_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_27"},{"key":"10.3233\/JCS-16832_ref3","doi-asserted-by":"crossref","unstructured":"A. Armando, R. Carbone, L. Compagna, J. Cu\u00e9llar and L. Tobarra, Formal analysis of SAML 2.0 Web browser single sign-on: Breaking the SAML-based single sign-on for Google apps, in: FMSE, ACM Press, 2008.","DOI":"10.1145\/1456396.1456397"},{"key":"10.3233\/JCS-16832_ref4","doi-asserted-by":"crossref","unstructured":"A. Armando and L. Compagna, SATMC: A SAT-based model checker for security protocols, in: JELIA, LNAI 3229, Springer, 2004, pp.\u00a0730\u2013733.","DOI":"10.1007\/978-3-540-30227-8_68"},{"key":"10.3233\/JCS-16832_ref5","doi-asserted-by":"crossref","unstructured":"A. Armando, G. Pellegrino, R. Carbone, A. Merlo and D. Balzarotti, From model-checking to automated testing of security protocols: Bridging the Gap, in: TAP, LNCS 7305, Springer, 2012, pp.\u00a03\u201318.","DOI":"10.1007\/978-3-642-30473-6_3"},{"issue":"3","key":"10.3233\/JCS-16832_ref7","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/s10207-004-0055-7","article-title":"OFMC: A symbolic model checker for security protocols","volume":"4","author":"Basin","year":"2005","journal-title":"International Journal of Information Security"},{"key":"10.3233\/JCS-16832_ref8","doi-asserted-by":"crossref","unstructured":"B. Blanchet, An efficient cryptographic protocol verifier based on prolog rules, in: CSFW, IEEE CS, 2001, pp.\u00a082\u201396.","DOI":"10.1109\/CSFW.2001.930138"},{"key":"10.3233\/JCS-16832_ref9","unstructured":"C. Boyd and A. Mathuria, Protocols for Authentication and Key Establishment, Springer, 2010."},{"key":"10.3233\/JCS-16832_ref10","doi-asserted-by":"crossref","unstructured":"M. B\u00fcchler, J. Oudinet and A. Pretschner, Security mutants for property-based testing, in: TAP, LNCS 6706, Springer, 2011, pp.\u00a069\u201377.","DOI":"10.1007\/978-3-642-21768-5_6"},{"key":"10.3233\/JCS-16832_ref11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.3233\/JCS-2006-14101","article-title":"A survey of algebraic properties used in cryptographic protocols","volume":"1","author":"Cortier","year":"2006","journal-title":"Journal of Computer Security"},{"issue":"3","key":"10.3233\/JCS-16832_ref12","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","article-title":"Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory","volume":"22","author":"Craig","year":"1957","journal-title":"The Journal of Symbolic Logic"},{"key":"10.3233\/JCS-16832_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78636-8"},{"key":"10.3233\/JCS-16832_ref14","doi-asserted-by":"crossref","unstructured":"C.J.F. Cremers, The Scyther Tool: Verification, falsification, and analysis of security protocols, in: Proceedings of CAV 2008, LNCS 5123, Springer, 2008, pp.\u00a0414\u2013418.","DOI":"10.1007\/978-3-540-70545-1_38"},{"key":"10.3233\/JCS-16832_ref15","doi-asserted-by":"crossref","unstructured":"L. de Moura and N. Bjorner, Z3: An efficient SMT solver, in: TACAS, LNCS 4963, Springer, 2008, pp.\u00a0337\u2013340. ISBN 978-3-540-78799-0.","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"2","key":"10.3233\/JCS-16832_ref16","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","article-title":"On the security of public-key protocols","volume":"29","author":"Dolev","year":"1983","journal-title":"IEEE Transactions on Information Theory"},{"key":"10.3233\/JCS-16832_ref17","doi-asserted-by":"crossref","unstructured":"S. Escobar, C. Meadows and J. Meseguer, Maude-NPA: Cryptographic protocol analysis modulo equational properties, in: FOSAD, Springer, 2007, pp.\u00a01\u201350.","DOI":"10.1007\/978-3-642-03829-7_1"},{"key":"10.3233\/JCS-16832_ref18","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/j.ic.2014.07.007","article-title":"State space reduction in the Maude-NRL protocol analyzer","volume":"238","author":"Escobar","year":"2014","journal-title":"Information and Computation"},{"key":"10.3233\/JCS-16832_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0039592"},{"issue":"7","key":"10.3233\/JCS-16832_ref20","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","article-title":"Symbolic execution and program testing","volume":"19","author":"King","year":"1976","journal-title":"CACM"},{"key":"10.3233\/JCS-16832_ref21","doi-asserted-by":"crossref","unstructured":"G. Lowe, Breaking and fixing the Needham\u2013Shroeder public-key protocol using FDR, in: TACAS, LNCS 1055, Springer, 1996, pp.\u00a0147\u2013166.","DOI":"10.1007\/3-540-61042-1_43"},{"key":"10.3233\/JCS-16832_ref22","doi-asserted-by":"crossref","unstructured":"K.L. McMillan, An interpolating theorem prover, in: Tools and Algorithms for the Construction and Analysis of Systems, Springer, 2004, pp.\u00a016\u201330.","DOI":"10.1007\/978-3-540-24730-2_2"},{"key":"10.3233\/JCS-16832_ref23","doi-asserted-by":"crossref","unstructured":"K.L. McMillan, Applications of Craig interpolants in model checking, in: TACAS, LNCS 3440, Springer, 2005, pp.\u00a01\u201312. ISBN 978-3-540-25333-4.","DOI":"10.1007\/978-3-540-31980-1_1"},{"issue":"1","key":"10.3233\/JCS-16832_ref24","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/j.tcs.2005.07.003","article-title":"An interpolating theorem prover","volume":"345","author":"McMillan","year":"2005","journal-title":"Theoretical Computer Science"},{"key":"10.3233\/JCS-16832_ref25","doi-asserted-by":"crossref","unstructured":"K.L. McMillan, Lazy abstraction with interpolants, in: CAV, 18th International Conference, Springer, 2006, pp.\u00a0123\u2013136.","DOI":"10.1007\/11817963_14"},{"key":"10.3233\/JCS-16832_ref26","doi-asserted-by":"crossref","unstructured":"K.L. McMillan, Lazy annotation for program testing and verification, in: CAV, LNCS 6174, Springer, 2010, pp.\u00a0104\u2013118. ISBN 978-3-642-14294-9.","DOI":"10.1007\/978-3-642-14295-6_10"},{"key":"10.3233\/JCS-16832_ref27","unstructured":"K.L. McMillan, Interpolants from Z3 proofs, in: FMCAD, 2011, pp.\u00a019\u201327. ISBN 978-0-9835678-1-3."},{"key":"10.3233\/JCS-16832_ref28","doi-asserted-by":"crossref","unstructured":"K.L. McMillan, Lazy annotation revisited, in: Computer Aided Verification \u2013 26th International Conference, 2014, pp.\u00a0243\u2013259.","DOI":"10.1007\/978-3-319-08867-9_16"},{"key":"10.3233\/JCS-16832_ref29","doi-asserted-by":"crossref","unstructured":"S. M\u00f6dersheim, Algebraic properties in Alice and Bob notation, in: Ares, IEEE CS, 2009, pp.\u00a0433\u2013440.","DOI":"10.1109\/ARES.2009.95"},{"key":"10.3233\/JCS-16832_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03829-7_6"},{"key":"10.3233\/JCS-16832_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04444-1_21"},{"key":"10.3233\/JCS-16832_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-41098-7_7"},{"issue":"1\u20133","key":"10.3233\/JCS-16832_ref33","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1016\/S0304-3975(02)00490-5","article-title":"Protocol insecurity with a finite number of sessions and composed keys is NP-complete","volume":"299","author":"Rusinowitch","year":"2003","journal-title":"Theor. Comput. Sci."},{"key":"10.3233\/JCS-16832_ref34","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2014.19"},{"key":"10.3233\/JCS-16832_ref35","doi-asserted-by":"crossref","unstructured":"M. Turuani, The CL-atse protocol analyser, in: Term Rewriting and Applications, LNCS 4098, Springer, 2006, pp.\u00a0277\u2013286. ISBN 978-3-540-36834-2.","DOI":"10.1007\/11805618_21"},{"key":"10.3233\/JCS-16832_ref36","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2013.75"},{"key":"10.3233\/JCS-16832_ref37","doi-asserted-by":"crossref","unstructured":"D. von Oheimb and S. M\u00f6dersheim, ASLan++ \u2013 a formal security specification language for distributed systems, in: FMCO, LNCS 6957, Springer, 2010, pp.\u00a01\u201322.","DOI":"10.1007\/978-3-642-25271-6_1"}],"container-title":["Journal of Computer Security"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/JCS-16832","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T20:45:05Z","timestamp":1777495505000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.medra.org\/servlet\/aliasResolver?alias=iospress&doi=10.3233\/JCS-16832"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,24]]},"references-count":36,"journal-issue":{"issue":"6"},"URL":"https:\/\/doi.org\/10.3233\/jcs-16832","relation":{},"ISSN":["1875-8924","0926-227X"],"issn-type":[{"value":"1875-8924","type":"electronic"},{"value":"0926-227X","type":"print"}],"subject":[],"published":{"date-parts":[[2017,8,24]]}}}