{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,25]],"date-time":"2025-10-25T14:15:49Z","timestamp":1761401749109},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2015,6,3]],"date-time":"2015-06-03T00:00:00Z","timestamp":1433289600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2016,4]]},"DOI":"10.1007\/s10009-015-0385-y","type":"journal-article","created":{"date-parts":[[2015,6,3]],"date-time":"2015-06-03T00:13:49Z","timestamp":1433290429000},"page":"187-204","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["SATMC: a SAT-based model checker for security protocols, business processes, and security APIs"],"prefix":"10.1007","volume":"18","author":[{"given":"Alessandro","family":"Armando","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Carbone","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"Compagna","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,6,3]]},"reference":[{"key":"385_CR1","first-page":"374","volume-title":"KR\u201996: Principles of Knowledge Representation and Reasoning","author":"H Kautz","year":"1996","unstructured":"Kautz, H., McAllester, H., Selman, B.: Encoding plans in propositional logic. In: Aiello, L.C., Doyle, J., Shapiro, S. (eds.) KR\u201996: Principles of Knowledge Representation and Reasoning, pp. 374\u2013384. Morgan Kaufmann, San Francisco (1996)"},{"key":"385_CR2","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Proceedings of TACAS\u201999. LNCS, vol. 1579. Springer (1999)","DOI":"10.1007\/3-540-49059-0_14"},{"key":"385_CR3","doi-asserted-by":"crossref","unstructured":"Armando, A., Compagna, L.: SATMC: a SAT-based model checker for security protocols. In: Proceedings European Conference on Logics in Artificial Intelligence. LNAI, vol. 3229. pp. 730\u2013733, Lisbon, Portugal, Springer (2004)","DOI":"10.1007\/978-3-540-30227-8_68"},{"key":"385_CR4","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"Gerard Holzmann","year":"2003","unstructured":"Holzmann, Gerard: The Spin Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley Professional, Boston (2003)","edition":"1"},{"key":"385_CR5","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV Version 2: An opensource tool for symbolic model checking. In: Proceedings International Conference on Computer-Aided Verification (CAV 2002). LNCS, vol. 2404. Springer, Copenhagen, (2002)"},{"key":"385_CR6","doi-asserted-by":"crossref","unstructured":"Turuani, M.: The CL-Atse protocol analyser. In: Pfenning, F. (ed.), Term rewriting and applications. LNCS, vol. 4098. pp. 277\u2013286. Springer (2006)","DOI":"10.1007\/11805618_21"},{"issue":"30","key":"385_CR7","first-page":"181","volume":"4","author":"D Basin","year":"2004","unstructured":"Basin, D., M\u00f6dersheim, S., Vigan\u00f2, L.: OFMC: A symbolic model-checker for security protocols. Int. J. Inf. Secur. 4(30), 181\u2013208 (2004)","journal-title":"Int. J. Inf. Secur."},{"key":"385_CR8","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: Computer Security Foundations Workshop (CSFW). pp. 82\u201396 (2001)","DOI":"10.1109\/CSFW.2001.930138"},{"key":"385_CR9","doi-asserted-by":"crossref","unstructured":"Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Hankes Drielsma, P., 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: CAV\u201905. Springer (2005)","DOI":"10.1007\/11513988_27"},{"key":"385_CR10","doi-asserted-by":"crossref","unstructured":"Bortolozzo, M., Centenaro, M., Focardi, R., Steel, G.: Attacking and fixing PKCS#11 security tokens. In: Proceedings ACM Conference on Computer and Communications Security (CCS\u201910). pp. 260\u2013269, ACM Press, Chicago (2010)","DOI":"10.1145\/1866307.1866337"},{"key":"385_CR11","doi-asserted-by":"crossref","unstructured":"Armando, A., Arsac, W., Avanesov, T., Barletta, M., Calvi, A., Cappai, A., Carbone, R., Chevalier, Y., Compagna, L., Cu\u00e9llar, J., Erzse, G., Frau, S., Minea, M., M\u00f6dersheim, S., Oheimb, D., Pellegrino, G., Ponta, S.E., Rocchetto, M., Rusinowitch, M., Torabi Dashti, M., Turuani, M., Vigan\u00f2, L.: The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures. In: TACAS\u201912. LNCS, vol. 7214, pp. 267\u2013282. Springer, New York (2012)","DOI":"10.1007\/978-3-642-28756-5_19"},{"key":"385_CR12","doi-asserted-by":"crossref","unstructured":"Vigan\u00f2, L.: The SPaCIoS project: secure provision and consumption in the internet of services. In: ICST\u201913. pp. 497\u2013498 (2013)","DOI":"10.1109\/ICST.2013.75"},{"key":"385_CR13","doi-asserted-by":"crossref","unstructured":"Armando, A., Carbone, R., Compagna, L.: LTL model checking for security protocols. In: 20th IEEE Computer Security Foundations Symposium (CSF). pp. 385\u2013396. IEEE Computer Society (2007)","DOI":"10.1109\/CSF.2007.24"},{"key":"385_CR14","doi-asserted-by":"crossref","unstructured":"Armando, A., Carbone, R., Compagna, L., Cu\u00e9llar, J., Tobarra, L.: Formal analysis of SAML 2.0 Web browser single sign-on: breaking the SAML-based single sign-on for google apps. In: Shmatikov, V. (eds.), Proceedings ACM Workshop on Formal Methods in Security Engineering. pp. 1\u201310. ACM Press (2008)","DOI":"10.1145\/1456396.1456397"},{"key":"385_CR15","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1016\/j.cose.2012.08.007","volume":"33","author":"A Armando","year":"2013","unstructured":"Armando, A., Carbone, R., Compagna, L., Cu\u00e9llar, J., Pellegrino, G., Sorniotti, A.: An authentication flaw in browser-based single sign-on protocols: impact and remediations. Comput. Secur. 33, 41\u201358 (2013)","journal-title":"Comput. Secur."},{"key":"385_CR16","doi-asserted-by":"crossref","unstructured":"Armando, A., Carbone, R., Zanetti, L.: Formal modeling and automatic security analysis of two-factor and two-channel authentication protocols. In: Network and System Security (NSS). LNCS, vol. 7873. pp. 728\u2013734. Springer (2013)","DOI":"10.1007\/978-3-642-38631-2_63"},{"key":"385_CR17","unstructured":"AVANTSSAR. Deliverable 2.1: Requirements for modelling and ASLan v. 1. http:\/\/www.avantssar.eu (2008)"},{"key":"385_CR18","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N: An extensible sat-solver. In: Giunchiglia, E., Tacchella, A. (eds.), SAT. LNCS, vol. 2919. pp. 502\u2013518. Springer (2003)","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"385_CR19","unstructured":"Armando, A., Carbone, R., Compagna, L.: SATMC: A SAT-based model checker for security-critical systems. In: \u00c1brah\u00e1m, E., Havelund, K, (ed.) Tools and Algorithms for the Construction and Analysis of Systems\u201420th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5\u201313, 2014. Proceedings, volume 8413 of Lecture Notes in Computer Science. pp. 31\u201345. Springer (2014)"},{"key":"385_CR20","unstructured":"OASIS Consortium. SAML V2.0 Technical Overview. http:\/\/wiki.oasis-open.org\/security\/Saml2TechOverview (2008)"},{"key":"385_CR21","unstructured":"Armando, A., Ponta, S.E.: Model checking of security-sensitive business processes. In: Degano, P., Guttman, J.D. (ed.), Formal Aspects in Security and Trust. LNCS, 5983. pp. 66\u201380. Springer (2009)"},{"key":"385_CR22","doi-asserted-by":"crossref","unstructured":"Arsac, W., Compagna, L., Pellegrino, G., Ponta, S.E.: Security validation of business processes via model-checking. In: International Symposium on Engineering Secure Software and Systems (ESSoS 2011). LNCS, Springer (2011)","DOI":"10.1007\/978-3-642-19125-1_3"},{"key":"385_CR23","doi-asserted-by":"crossref","unstructured":"Compagna, L., Guilleminot, P., Brucker, A.D.: Business process compliance via security validation as a service. In: ICST\u201913. pp. 455\u2013462 (2013)","DOI":"10.1109\/ICST.2013.63"},{"key":"385_CR24","unstructured":"RSA Sec. Inc. PKCS#11: Cryptographic Token Interface Standard v2.20, (2004)"},{"key":"385_CR25","doi-asserted-by":"crossref","unstructured":"Focardi, R., Luccio, F.L., Steel, G.: An introduction to security API analysis. In: Foundations of Security Analysis and Design\u2014FOSAD Tutorial Lectures (FOSAD\u2019VI). LNCS, vol. 6858. pp. 35\u201365 (2011)","DOI":"10.1007\/978-3-642-23082-0_2"},{"issue":"2","key":"385_CR26","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.: On the security of public-key protocols. IEEE Trans. Inf. Theory 29(2), 198\u2013208 (1983)","journal-title":"IEEE Trans. Inf. Theory"},{"issue":"4","key":"385_CR27","doi-asserted-by":"crossref","first-page":"403","DOI":"10.3166\/jancl.19.403-429","volume":"19","author":"A Armando","year":"2009","unstructured":"Armando, A., Carbone, R., Compagna, L.: LTL model checking for security protocols. J. Appl. Non Class. Logics 19(4), 403\u2013429 (2009)","journal-title":"J. Appl. Non Class. Logics"},{"key":"385_CR28","doi-asserted-by":"crossref","unstructured":"Blum, A., Furst, M.: Fast planning through planning graph analysis. In: Proceedings International Joint Conference on Artificial Intelligence (IJCAI 95) (1995)","DOI":"10.21236\/ADA303260"},{"key":"385_CR29","series-title":"Frontiers in artificial intelligence and applications","first-page":"457","volume-title":"Handbook of Satisfiability","author":"A Biere","year":"2009","unstructured":"Biere, A.: Bounded model checking. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in artificial intelligence and applications, pp. 457\u2013481. IOS Press, Amsterdam (2009)"},{"issue":"1","key":"385_CR30","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10207-007-0041-y","volume":"7","author":"A Armando","year":"2008","unstructured":"Armando, A., Compagna, L.: SAT-based model-checking for security protocols analysis. Int. J. Inf. Secur. 7(1), 3\u201332 (2008)","journal-title":"Int. J. Inf. Secur."},{"key":"385_CR31","doi-asserted-by":"crossref","unstructured":"Cremers, C.J.F., Lafourcade, P., Nadeau, P.: Comparing state spaces in automatic security protocol analysis. In: Formal to practical security. pp. 70\u201394. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-02002-5_5"},{"issue":"10","key":"385_CR32","first-page":"779","volume":"3","author":"N Dalal","year":"2010","unstructured":"Dalal, N., Shah, J., Hisaria, K., Jinwala, D., et al.: A comparative analysis of tools for verification of security protocols. Int. J. Commun. Netw. Syst. Sci. 3(10), 779 (2010)","journal-title":"Int. J. Commun. Netw. Syst. Sci."},{"issue":"1","key":"385_CR33","first-page":"89","volume":"12","author":"JCL Pimentel","year":"2008","unstructured":"Pimentel, J.C.L., Monroy, R.: Formal support to security protocol development: a survey. Comput. Sist. 12(1), 89\u2013108 (2008)","journal-title":"Comput. Sist."},{"key":"385_CR34","doi-asserted-by":"crossref","unstructured":"Cortier, V., Kremer, S.: Formal models and techniques for analyzing security protocols-a tutorial (2014)","DOI":"10.1561\/2500000001"},{"key":"385_CR35","doi-asserted-by":"crossref","unstructured":"Lowe, G.: Casper: a compiler for the analysis of security protocols. J. Comput. Secur. 6(1), 53\u201384 (1998). See http:\/\/web.comlab.ox.ac.uk\/oucl\/work\/gavin.lowe\/Security\/Casper\/","DOI":"10.3233\/JCS-1998-61-204"},{"key":"385_CR36","unstructured":"Donovan, B., Norris, P., Lowe, G.: Analyzing a library of security protocols using casper and FDR. In: Proceedings of the Workshop on Formal Methods and Security Protocols (1999)"},{"key":"385_CR37","unstructured":"CSP\u2013Communicating Sequential Processes. http:\/\/www.formal.demon.co.uk\/CSP.html"},{"key":"385_CR38","unstructured":"FDR2 System\u2014Failures-Divergence Refinement. http:\/\/www.formal.demon.co.uk\/CSP.html"},{"key":"385_CR39","unstructured":"Cremers, C.J.F.: Scyther documentation. http:\/\/www.win.tue.nl\/~ccremers\/scyther"},{"key":"385_CR40","unstructured":"Boichut, Y., H\u00e9am, P.-C., Kouchnarenko, O., Oehl, F.: Improvements on the genet and klay technique to automatically verify security protocols. In: Proceedings of Automated Verification of Infinite States Systems (AVIS\u201904), ENTCS (2004)"},{"key":"385_CR41","unstructured":"Dilloway, C., Lowe, G.: On the specification of secure channels. In: Proceedings of the Workshop on Issues in the Theory of Security (WITS \u201907) (2007)"},{"key":"385_CR42","doi-asserted-by":"crossref","unstructured":"Bansal, C., Bhargavan, K., Maffeis, S.: Discovering concrete attacks on website authorization by formal analysis. In: Proceedings of the 2012 IEEE 25th Computer Security Foundations Symposium, CSF \u201912. pp. 247\u2013262. IEEE Computer Society, Washington (2012)","DOI":"10.1109\/CSF.2012.27"},{"key":"385_CR43","doi-asserted-by":"crossref","unstructured":"M\u00f6dersheim, S., Vigan\u00f2, L.: Secure pseudonymous channels. In: Backes, M., Ning, P. (eds.) Computer Security ESORICS 2009. Lecture Notes in Computer Science, vol. 5789, pp. 337\u2013354. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-04444-1_21"},{"issue":"2","key":"385_CR44","doi-asserted-by":"crossref","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. Theor. Comput. Sci. 283(2), 419\u2013450 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"385_CR45","doi-asserted-by":"crossref","unstructured":"Steel, G.: Formal analysis of security APIs (2011)","DOI":"10.1007\/978-1-4419-5906-5_873"},{"issue":"1","key":"385_CR46","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/JCS-2006-14101","volume":"14","author":"V Cortier","year":"2006","unstructured":"Cortier, V., Delaune, S., Lafourcade, P.: A survey of algebraic properties used in cryptographic protocols. J. Comput. Secur. 14(1), 1\u201343 (2006)","journal-title":"J. Comput. Secur."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0385-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-015-0385-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0385-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,2]],"date-time":"2020-09-02T23:49:50Z","timestamp":1599090590000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-015-0385-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,6,3]]},"references-count":46,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,4]]}},"alternative-id":["385"],"URL":"https:\/\/doi.org\/10.1007\/s10009-015-0385-y","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,6,3]]}}}