{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T14:04:49Z","timestamp":1773324289901,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642304729","type":"print"},{"value":"9783642304736","type":"electronic"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-30473-6_3","type":"book-chapter","created":{"date-parts":[[2012,5,25]],"date-time":"2012-05-25T15:29:12Z","timestamp":1337959752000},"page":"3-18","source":"Crossref","is-referenced-by-count":18,"title":["From Model-Checking to Automated Testing of Security Protocols: Bridging the Gap"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Armando","sequence":"first","affiliation":[]},{"given":"Giancarlo","family":"Pellegrino","sequence":"additional","affiliation":[]},{"given":"Roberto","family":"Carbone","sequence":"additional","affiliation":[]},{"given":"Alessio","family":"Merlo","sequence":"additional","affiliation":[]},{"given":"Davide","family":"Balzarotti","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","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., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Drielsma, P.H., He\u00e1m, P.C., Kouchnarenko, O., Mantovani, J., M\u00f6dersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Vigan\u00f2, L., Vigneron, L.: 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":"3_CR2","doi-asserted-by":"crossref","unstructured":"Armando, A., Carbone, R., Compagna, L.: LTL Model Checking for Security Protocols. Journal of Applied Non-Classical Logics (2009)","DOI":"10.3166\/jancl.19.403-429"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Armando, A., Carbone, R., Compagna, L., Cuellar, J., Abad, L.T.: Formal Analysis of SAML 2.0 Web Browser Single Sign-On: Breaking the SAML-based Single Sign-On for Google Apps. In: Proc. of ACM FMSE 2008 (2008)","DOI":"10.1145\/1456396.1456397"},{"key":"3_CR4","series-title":"IFIP AICT","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-642-21424-0_6","volume-title":"Future Challenges in Security and Privacy for Academia and Industry","author":"A. Armando","year":"2011","unstructured":"Armando, A., Carbone, R., Compagna, L., Cuellar, J., Pellegrino, G., Sorniotti, A.: From Multiple Credentials to Browser-Based Single Sign-On: Are We More Secure? In: Camenisch, J., Fischer-H\u00fcbner, S., Murayama, Y., Portmann, A., Rieder, C. (eds.) SEC 2011. IFIP AICT, vol.\u00a0354, pp. 68\u201379. Springer, Heidelberg (2011)"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Armando, A., Carbone, R., Compagna, L., Li, K., Pellegrino, G.: Model-checking driven security testing of web-based applications. In: Proc. of ICSTW 2010 (2010)","DOI":"10.1109\/ICSTW.2010.54"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/3-540-36135-9_14","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2002","author":"A. Armando","year":"2002","unstructured":"Armando, A., Compagna, L.: Automatic SAT-Compilation of Protocol Insecurity Problems via Reduction to Planning. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol.\u00a02529, pp. 210\u2013225. Springer, Heidelberg (2002)"},{"key":"3_CR7","unstructured":"AVANTSSAR. Deliverable 2.1: Requirements for modelling and ASLan v.1 (2008), http:\/\/www.avantssar.eu"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/11690634_29","volume-title":"Foundations of Software Science and Computation Structures","author":"M. Backes","year":"2006","unstructured":"Backes, M., M\u00f6dersheim, S., Pfitzmann, B., Vigan\u00f2, L.: Symbolic and Cryptographic Analysis of the Secure WS-ReliableMessaging Scenario. In: Aceto, L., Ing\u00f3lfsd\u00f3ttir, A. (eds.) FOSSACS 2006. LNCS, vol.\u00a03921, pp. 428\u2013445. Springer, Heidelberg (2006)"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Bau, J., Bursztein, E., Gupta, D., Mitchell, J.: State of the art: Automated black-box web application vulnerability testing. In: 2010 IEEE Symposium on Security and Privacy, SP (2010)","DOI":"10.1109\/SP.2010.27"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: Automatic verification of cryptographic protocols: A logic programming approach. In: Proc. of PPDP 2003 (2003) (invited talk)","DOI":"10.1145\/888251.888252"},{"key":"3_CR11","unstructured":"Bortolozzo, M., Centenaro, M., Focardi, R., Steel, G.: Attacking and fixing PKCS#11 security tokens. In: ACM Conf. on CSS"},{"key":"3_CR12","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)"},{"key":"3_CR13","unstructured":"Clark, J., Jacob, J.: A Survey of Authentication Protocol Literature: Version 1.0 (November 17, 1997), www.cs.york.ac.uk\/~jac\/papers\/drareview.ps.gz"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Dadeau, F., H\u00e9andam, P.-C., Kheddam, R.: Mutation-based test generation from security protocols in HLPSL. In: ICST 2011 (2011)","DOI":"10.1109\/ICST.2011.42"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-642-14215-4_7","volume-title":"Detection of Intrusions and Malware, and Vulnerability Assessment","author":"A. Doup\u00e9","year":"2010","unstructured":"Doup\u00e9, A., Cova, M., Vigna, G.: Why Johnny Can\u2019t Pentest: An Analysis of Black-Box Web Vulnerability Scanners. In: Kreibich, C., Jahnke, M. (eds.) DIMVA 2010. LNCS, vol.\u00a06201, pp. 111\u2013131. Springer, Heidelberg (2010)"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Fraser, G., Wotawa, F., Ammann, P.: Testing with model checkers: a survey. Softw. Test., Verif. Reliab.\u00a019 (2009)","DOI":"10.1002\/stvr.402"},{"issue":"2","key":"3_CR17","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1147\/sj.412.0228","volume":"41","author":"M. Hondo","year":"2002","unstructured":"Hondo, M., Nagaratnam, N., Nadalin, A.: Securing web services. IBM Systems Journal\u00a041(2), 228\u2013241 (2002)","journal-title":"IBM Systems Journal"},{"key":"3_CR18","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/3-540-44404-1_10","volume-title":"Logic for Programming and Automated Reasoning","author":"F. Jacquemard","year":"2000","unstructured":"Jacquemard, F., Rusinowitch, M., Vigneron, L.: Compiling and Verifying Security Protocols. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol.\u00a01955, pp. 131\u2013160. Springer, Heidelberg (2000)"},{"key":"3_CR19","unstructured":"Lowe, G.: A hierarchy of authentication specifications. In: Proc. of the 10th IEEE CSFW 1997 (1997)"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","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-Schroeder Public-Key Protocol Using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol.\u00a01055, pp. 167\u2013181. Springer, Heidelberg (1996)"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Marrero, W., Clarke, E.M., Jha, S.: Model checking for security protocols. tech. report cmu-scs-97-139. Technical report, CMU (May 1997)","DOI":"10.21236\/ADA327281"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Millen, J.K., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: Proc. of ACM CCS 2001 (2001)","DOI":"10.1145\/501983.502007"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"OASIS. SAML V2.0 (2005), http:\/\/docs.oasis-open.org\/security\/saml\/v2.0\/","DOI":"10.1049\/ic:20050239"},{"key":"3_CR24","unstructured":"Ryan, P., Schneider, S., Goldsmith, M., Lowe, G., Roscoe, B.: Modelling and Analysis of Security Protocols. Addison Wesley (2000)"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Salas, P.A.P., Krishnan, P., Ross, K.J.: Model-based security vulnerability testing. In: Australian Software Engineering Conf., pp. 284\u2013296 (2007)","DOI":"10.1109\/ASWEC.2007.31"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Salas, P.A.P., Krishnan, P.: Testing privacy policies using models. In: Proc. of SEFM 2008 (2008)","DOI":"10.1109\/SEFM.2008.7"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"Sala\u00fcn, G., Bordeaux, L., Schaerf, M.: Describing and reasoning on web services using process algebra. In: Proc. of ICWS 2004 (2004)","DOI":"10.1109\/ICWS.2004.1314722"},{"issue":"2","key":"3_CR28","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1016\/S0304-3975(01)00141-4","volume":"283","author":"V. Shmatikov","year":"2002","unstructured":"Shmatikov, V., Mitchell, J.C.: Finite-state analysis of two contract signing protocols. Theoretical Computer Science\u00a0283(2), 419\u2013450 (2002)","journal-title":"Theoretical Computer Science"},{"key":"3_CR29","unstructured":"Tretmans, G.J., Brinksma, H.: Torx: Automated model-based testing. In: First European Conf. on Model-Driven Software Engineering"},{"key":"3_CR30","unstructured":"Utting, M., Pretschner, A., Legeard, B.: A taxonomy of model-based testing. Technical report, University of Waikato, New Zealand"}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-30473-6_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T21:24:36Z","timestamp":1743197076000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-30473-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642304729","9783642304736"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-30473-6_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}