{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T22:15:15Z","timestamp":1725747315647},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642410970"},{"type":"electronic","value":"9783642410987"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-41098-7_7","type":"book-chapter","created":{"date-parts":[[2013,9,4]],"date-time":"2013-09-04T09:16:01Z","timestamp":1378286161000},"page":"99-114","source":"Crossref","is-referenced-by-count":2,"title":["Using Interpolation for the Verification of Security Protocols"],"prefix":"10.1007","author":[{"given":"Marco","family":"Rocchetto","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"Vigan\u00f2","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Volpe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giacomo Dalle","family":"Vedove","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-642-28756-5_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Armando","year":"2012","unstructured":"Armando, A., et al.: The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 267\u2013282. Springer, Heidelberg (2012)"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11513988_27","volume-title":"Computer Aided Verification","author":"A. Armando","year":"2005","unstructured":"Armando, A., et al.: The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 281\u2013285. Springer, Heidelberg (2005)"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Armando, A., Carbone, R., Compagna, L., Cu\u00e9llar, J., Tobarra Abad, L.: Formal Analysis of SAML 2.0 Web Browser Single Sign-On: Breaking the SAML-based Single Sign-On for Google Apps. In: FMSE. ACM (2008)","DOI":"10.1145\/1456396.1456397"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-642-30473-6_3","volume-title":"Tests and Proofs","author":"A. Armando","year":"2012","unstructured":"Armando, A., Pellegrino, G., Carbone, R., Merlo, A., Balzarotti, D.: From Model-Checking to Automated Testing of Security Protocols: Bridging the Gap. In: Brucker, A.D., Julliand, J. (eds.) TAP 2012. LNCS, vol.\u00a07305, pp. 3\u201318. Springer, Heidelberg (2012)"},{"issue":"3","key":"7_CR5","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/s10207-004-0055-7","volume":"4","author":"D. Basin","year":"2005","unstructured":"Basin, D., M\u00f6dersheim, S., Vigan\u00f2, L.: OFMC: A symbolic model checker for security protocols. Int. Journal of Information Security\u00a04(3), 181\u2013208 (2005)","journal-title":"Int. Journal of Information Security"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-642-21768-5_6","volume-title":"Tests and Proofs","author":"M. B\u00fcchler","year":"2011","unstructured":"B\u00fcchler, M., Oudinet, J., Pretschner, A.: Security mutants for property-based testing. In: Gogolla, M., Wolff, B. (eds.) TAP 2011. LNCS, vol.\u00a06706, pp. 69\u201377. Springer, Heidelberg (2011)"},{"issue":"3","key":"7_CR7","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W. Craig","year":"1957","unstructured":"Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. The Journal of Symbolic Logic\u00a022(3), 269\u2013285 (1957)","journal-title":"The Journal of Symbolic Logic"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Dolev, D., Yao, A.: On the Security of Public-Key Protocols. IEEE Transactions on Information Theory\u00a02(29) (1983)","DOI":"10.1109\/TIT.1983.1056650"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL, pp. 232\u2013244. ACM (2004)","DOI":"10.1145\/982962.964021"},{"issue":"7","key":"7_CR10","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"J.C. King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. CACM\u00a019(7), 385\u2013394 (1976)","journal-title":"CACM"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-61042-1_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Lowe","year":"1996","unstructured":"Lowe, G.: Breaking and Fixing the Needham-Shroeder Public-Key Protocol Using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol.\u00a01055, pp. 147\u2013166. Springer, Heidelberg (1996)"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-31980-1_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.L. McMillan","year":"2005","unstructured":"McMillan, K.L.: Applications of Craig Interpolants in Model Checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 1\u201312. Springer, Heidelberg (2005)"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-642-14295-6_10","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2010","unstructured":"McMillan, K.L.: Lazy annotation for program testing and verification. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 104\u2013118. Springer, Heidelberg (2010)"},{"key":"7_CR14","unstructured":"McMillan, K.L.: Interpolants from Z3 proofs. In: FMCAD, pp. 19\u201327 (2011)"},{"key":"7_CR15","unstructured":"Mitchell, J.C., Mitchell, M., Stern, U.: Automated analysis of cryptographic protocols using Murphi. In: Security and Privacy, pp. 141\u2013151. IEEE CS (1997)"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"7_CR17","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1016\/S0304-3975(02)00490-5","volume":"299","author":"M. Rusinowitch","year":"2003","unstructured":"Rusinowitch, M., Turuani, M.: Protocol insecurity with a finite number of sessions and composed keys is NP-complete. TCS\u00a0299, 451\u2013475 (2003)","journal-title":"TCS"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-25271-6_1","volume-title":"Formal Methods for Components and Objects","author":"D. Oheimb von","year":"2011","unstructured":"von Oheimb, D., M\u00f6dersheim, S.: ASLan++ \u2014 A formal security specification language for distributed systems. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol.\u00a06957, pp. 1\u201322. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","Security and Trust Management"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-41098-7_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T21:34:57Z","timestamp":1558042497000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-41098-7_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642410970","9783642410987"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-41098-7_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}