{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,4]],"date-time":"2026-03-04T17:23:53Z","timestamp":1772645033456,"version":"3.50.1"},"reference-count":64,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2007,9,21]],"date-time":"2007-09-21T00:00:00Z","timestamp":1190332800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Inf. Secur."],"published-print":{"date-parts":[[2008,1]]},"DOI":"10.1007\/s10207-007-0041-y","type":"journal-article","created":{"date-parts":[[2007,9,20]],"date-time":"2007-09-20T07:04:03Z","timestamp":1190271843000},"page":"3-32","source":"Crossref","is-referenced-by-count":68,"title":["SAT-based model-checking for security protocols analysis"],"prefix":"10.1007","volume":"7","author":[{"given":"Alessandro","family":"Armando","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"Compagna","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,9,21]]},"reference":[{"issue":"5","key":"41_CR1","doi-asserted-by":"crossref","first-page":"749","DOI":"10.1145\/324133.324266","volume":"46","author":"M. Abadi","year":"1999","unstructured":"Abadi M. (1999). Secrecy by typing in security protocols. J. ACM 46(5): 749\u2013786","journal-title":"J. ACM"},{"key":"41_CR2","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1080\/00150517.1973.12430815","volume":"11","author":"A.V. Aho","year":"1973","unstructured":"Aho A.V. and Sloane N.J.A. (1973). Some doubly exponential sequences. Fibonacci Q. 11: 429\u2013437","journal-title":"Fibonacci Q."},{"issue":"4","key":"41_CR3","doi-asserted-by":"crossref","first-page":"542","DOI":"10.1145\/383779.383785","volume":"2","author":"L.C. Aiello","year":"2001","unstructured":"Aiello L.C. and Massacci F. (2001). Verifying security protocols as planning in logic programming. ACM Trans. Comput. Logic 2(4): 542\u2013580","journal-title":"ACM Trans. Comput. Logic"},{"key":"41_CR4","doi-asserted-by":"crossref","unstructured":"Allamigeon, X., Blanchet, B.: Reconstruction of attacks against cryptographic protocols. In: 18th IEEE Computer Security Foundations Workshop (CSFW-18 2005), 20\u201322 June 2005, Aix- en-Provence, France, pp. 140\u2013154 (2005)","DOI":"10.1109\/CSFW.2005.25"},{"key":"41_CR5","doi-asserted-by":"crossref","unstructured":"Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Drielsma, P.H., Heam, P., Kouchnarenko, O., Mantovani, J., Moedersheim, 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: Proceedings of the 17th International Conference on Computer-Aided Verification (CAV\u201905) (2005)","DOI":"10.1007\/11513988_27"},{"key":"41_CR6","unstructured":"Armando, A., Basin, D., Bouallagui, M., Chevalier, Y., Compagna, L., M\u00f6dersheim, S., Rusinowitch, M., Turuani, M., Vigan\u00f2, L., Vigneron, L.: The AVISS security protocol analysis tool. In: Proceedings of CAV\u201902, LNCS, vol. 2404, pp. 349\u2013354. Springer (2002). URL of the AVISS and AVISPA projects: http:\/\/www.avispa-project.org"},{"key":"41_CR7","doi-asserted-by":"crossref","unstructured":"Armando, A., Compagna, L.: Automatic SAT-compilation of protocol insecurity problems via reduction to planning. In: Proceedings of FORTE 2002, LNCS, vol. 2529, pp. 210\u2013225. Springer (2002)","DOI":"10.1007\/3-540-36135-9_14"},{"key":"41_CR8","unstructured":"Armando, A., Compagna, L.: Abstraction-driven SAT-based analysis of security protocols. In: Giunchiglia, E., Tacchella, A. (eds.) Theory and Applications of Satisfiability Testing, LNCS, vol. 2919, pp. 257\u2013271. Springer (2004). Selected Revised Papers. Presented to SAT 2003, S. Margherita Ligure, Italy. Available at http:\/\/www.avispa-project.org"},{"key":"41_CR9","doi-asserted-by":"crossref","unstructured":"Armando, A., Compagna, L.: SATMC: a SAT-based model checker for security protocols. In: Proceedings of the 9th European Conference on Logics in Artificial Intelligence (JELIA 2004), LNAI, vol. 3229. Springer, Lisbon (2004)","DOI":"10.1007\/978-3-540-30227-8_68"},{"key":"41_CR10","doi-asserted-by":"crossref","unstructured":"Armando, A., Compagna, L., Ganty, P.: SAT-based model- checking of security protocols using planning graph analysis. In: Proceedings of FME\u20192003, LNCS, vol. 2805. Springer (2003)","DOI":"10.1007\/978-3-540-45236-2_47"},{"key":"41_CR11","doi-asserted-by":"crossref","unstructured":"Armando, A., Compagna, L., Lierler, Y.: Automatic compilation of protocol insecurity problems into logic programming. In: Proceedings of the 9th European Conference on Logics in Artificial Intelligence (JELIA 2004), LNAI, vol. 3229. Springer, Lisbon (2004)","DOI":"10.1007\/978-3-540-30227-8_51"},{"key":"41_CR12","doi-asserted-by":"crossref","unstructured":"Basin, D., M\u00f6dersheim, S., Vigan\u00f2, L.: An on-the-fly model-checker for security protocol analysis. In: Snekkenes, E., Gollmann, D. (eds.) Proceedings of ESORICS\u201903, LNCS, vol. 2808, pp. 253\u2013270. Springer (2003). Available at http:\/\/www.avispa-project.org","DOI":"10.1007\/978-3-540-39650-5_15"},{"key":"41_CR13","unstructured":"Basin, D., M\u00f6dersheim, S., Vigan\u00f2, L.: Constraint differentiation: a new reduction technique for constraint-based analysis of security protocols. In: Atluri, V., Liu, P. (eds.) Proceedings of CCS\u201903, pp. 335\u2013344. ACM Press (2003). Available at http:\/\/www.avispa-project.org"},{"key":"41_CR14","doi-asserted-by":"crossref","unstructured":"Basin, D., M\u00f6dersheim, S., Vigan\u00f2, L.: OFMC: a symbolic model-checker for security protocols. Int. J. Information Security (2004) (in press)","DOI":"10.1007\/s10207-004-0055-7"},{"key":"41_CR15","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) Proceedings of TACAS\u201999, LNCS, vol. 1579, pp. 193\u2013207. Springer (1999)","DOI":"10.21236\/ADA360973"},{"key":"41_CR16","doi-asserted-by":"crossref","unstructured":"Blanchet, P.: Verification of cryptographic protocols: Tagging enforces termination. Theor. Comput. Sci. 333 (2005) (in press)","DOI":"10.1016\/j.tcs.2004.10.018"},{"key":"41_CR17","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Proceedings of CSFW\u201901, pp. 82\u201396. IEEE Computer Society Press (2001)","DOI":"10.1109\/CSFW.2001.930138"},{"key":"41_CR18","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: Automatic verification of cryptographic protocols: a logic programming approach (invited talk). In: Proceedings of PPDP\u201903, pp. 1\u20133. ACM Press (2003)","DOI":"10.1145\/888251.888252"},{"key":"41_CR19","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: Automatic proof of strong secrecy for security protocols. In: Proceedings of IEEE Symposium on Security and Privacy, pp. 86\u2013100. IEEE Computer Society Press (2004)","DOI":"10.1109\/SECPRI.2004.1301317"},{"key":"41_CR20","unstructured":"Blum, A., Furst, M.: Fast planning through planning graph analysis. In: Proceedings of the 14th International Joint Conference on Artificial Intelligence (IJCAI 95), pp. 1636\u20131642 (1995). URL http:\/\/citeseer.nj.nec.com\/blum95fast.html"},{"key":"41_CR21","unstructured":"Bodei, C., Buchholtz, M., Degano, P., Nielson, F., Nielson, H.R.: Control flow analysis can find new flaws too. In: Proceedings of Workshop on Issues in the Theory of Security (WITS 04) (2004). URL http:\/\/www2.imm.dtu.dk\/pubdb\/p.php?3058"},{"key":"41_CR22","doi-asserted-by":"crossref","unstructured":"Bodei, C., Buchholtz, M., Degano, P., Nielson, F., Riis~Nielson, H.: Automatic validation of protocol narration. In: Proceedings of CSFW\u201903, pp. 126\u2013140. IEEE Computer Society Press (2003)","DOI":"10.1109\/CSFW.2003.1212709"},{"key":"41_CR23","doi-asserted-by":"crossref","unstructured":"Bugliesi, M., Focardi, R., Maffei, M.: Compositional analysis of authentication protocols. In: Schmidt, D.A. (ed.) ESOP, Lecture Notes in Computer Science, vol. 2986, pp. 140\u2013154. Springer (2004). URL http:\/\/springerlink.metapress.com\/openurl.asp?genre=article&issn=0302-9743&volume=2986&spage=140","DOI":"10.1007\/978-3-540-24725-8_11"},{"key":"41_CR24","doi-asserted-by":"crossref","unstructured":"Cervesato, I., Durgin, N.A., Lincoln, P., Mitchell, J.C., Scedrov, A.: A meta-notation for protocol analysis. In: CSFW, pp. 55\u201369 (1999). URL http:\/\/citeseer.nj.nec.com\/cervesato99metanotation.html","DOI":"10.1109\/CSFW.1999.779762"},{"key":"41_CR25","unstructured":"Chevalier, Y., Compagna, L., Cuellar, J., Hankes~Drieslma, P., Mantovani, J., M\u00f6dersheim, S., Vigneron, L.: A high level protocol specification language for industrial security-sensitive protocols. In: Proceedings of SAPS\u20192004 (2004)"},{"key":"41_CR26","doi-asserted-by":"crossref","unstructured":"Chevalier, Y., Vigneron, L.: Automated unbounded verification of security protocols. In: Brinksma, E., Larsen, K.G. (eds.) Proceedings of CAV\u201902, LNCS, vol. 2404, pp. 324\u2013337. Springer (2002)","DOI":"10.1007\/3-540-45657-0_24"},{"key":"41_CR27","unstructured":"Clark, J., Jacob, J.: A survey of authentication protocol literature: Version 1.0, 17. Nov. 1997 (1997). URL: http:\/\/www.cs.york.ac.uk\/~jac\/papers\/drareview.ps.gz"},{"key":"41_CR28","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Jha, S., Marrero, W.R.: Partial order reductions for security protocol verification. In: TACAS, pp. 503\u2013518 (2000)","DOI":"10.1007\/3-540-46419-0_34"},{"key":"41_CR29","unstructured":"Compagna, L.: SAT-based model-checking of security protocols. Ph.D. thesis, Universit\u00e0 degli Studi di Genova and the University of Edinburgh (joint programme) (2005)"},{"key":"41_CR30","doi-asserted-by":"crossref","unstructured":"Corin, R., Etalle, S.: An improved constraint-based system for the verification of security protocols. In: Proceedings of SAS 2002, LNCS, vol. 2477, pp. 326\u2013341. Springer (2002)","DOI":"10.1007\/3-540-45789-5_24"},{"key":"41_CR31","doi-asserted-by":"crossref","unstructured":"Dolev, D., Yao, A.: On the security of public-key protocols. IEEE Trans. Inf. Theory 2(29) (1983) (in press)","DOI":"10.1109\/TIT.1983.1056650"},{"key":"41_CR32","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":"41_CR33","doi-asserted-by":"crossref","unstructured":"Durante, F., Gorrieri: CVS at work: a report on new failures upon some cryptographic protocols. In: MMMACNS: International Workshop on Methods, Models and Architectures for Network Security, LNCS (2001)","DOI":"10.1007\/3-540-45116-1_28"},{"key":"41_CR34","unstructured":"Durgin, N., Lincoln, P., Mitchell, J., Scedrov, A.: Multiset rewriting and the complexity of bounded security protocols (2002)"},{"key":"41_CR35","unstructured":"Ernst, M.D., Millstein, T.D., Weld, D.S.: Automatic SAT- compilation of planning problems. In: Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI-97), pp. 1169\u20131177. Morgan Kaufmann (1997)"},{"key":"41_CR36","doi-asserted-by":"crossref","unstructured":"Even, S., Goldreich, O.: On the security of multi-party ping pong protocols. In: Proceedings of 24th IEEE Symposium on Foundations of Computer Science. IEEE Computer Society (1983)","DOI":"10.1109\/SFCS.1983.42"},{"key":"41_CR37","doi-asserted-by":"crossref","unstructured":"F\u00e1brega, F.J.T., Herzog, J.C., Guttman, J.D.: Strand spaces: why a security protocol is correct? In: Proceedings of the 1998 IEEE Symposium on Security and Privacy, pp. 160\u2013171. IEEE Computer Society Press, New York (1998)","DOI":"10.21236\/ADA459060"},{"key":"41_CR38","unstructured":"Focardi, R., Gorrieri, R., Martinelli, F.: Secrecy in security protocols as non interference. Electr. Notes Theor. Comput. Sci 32 (2000). URL http:\/\/www.elsevier.com\/gej-ng\/31\/29\/23\/57\/23\/show\/Products\/notes\/index.htt#007"},{"key":"41_CR39","unstructured":"Ghallab, M., Howe, A., Knoblock, C., McDermott, D., Ram, A., Veloso, M., Weld, D., Wilkins, D.: The PDDL planning domain definition language (1998). The AIPS-98 Planning Competition Commitee"},{"key":"41_CR40","doi-asserted-by":"crossref","unstructured":"Gordon, J.: Typing correspondence assertions for communication protocols. Theor. Comput. Sci. 300 (2003) (in press)","DOI":"10.1016\/S0304-3975(02)00333-X"},{"issue":"4","key":"41_CR41","doi-asserted-by":"crossref","first-page":"451","DOI":"10.3233\/JCS-2003-11402","volume":"11","author":"A.D. Gordon","year":"2003","unstructured":"Gordon A.D. and Jeffrey A. (2003). Authenticity by typing for security protocols. J. Comput. Security 11(4): 451\u2013520","journal-title":"J. Comput. Security"},{"key":"41_CR42","unstructured":"Hansen, S.M., Skriver, J., Nielson, H.R.: Using static analysis to validate the SAML single sign-on protocol. In: WITS (2005). URL http:\/\/www2.imm.dtu.dk\/pubdb\/p.php?3657"},{"key":"41_CR43","doi-asserted-by":"crossref","unstructured":"Heather, J., Lowe, G., Schneider, S.: How to prevent type flaw attacks on security protocols. In: Proceedings of the 13th computer Security Foundations Workshop (CSFW\u201900). IEEE Computer Society Press (2000)","DOI":"10.1109\/CSFW.2000.856942"},{"key":"41_CR44","unstructured":"ISO\/IEC: ISO\/IEC 9798-3: Information technology\u2014Security techniques\u2014Entity authentication\u2014Part 3: Mechanisms using digital signature techniques (1997)"},{"key":"41_CR45","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 (1996)"},{"key":"41_CR46","unstructured":"Kautz, H.A., Selman, B.: Planning as satisfiability. In: ECAI, pp. 359\u2013363 (1992)"},{"key":"41_CR47","doi-asserted-by":"crossref","unstructured":"Lifschitz, V.: Answer set programming and plan generation. Artif. Intell. 138(1\u20132), 39\u201354 (2002). doi: http:\/\/dx.doi.org\/10.1016\/S0004-3702(02)00186-8","DOI":"10.1016\/S0004-3702(02)00186-8"},{"issue":"1\u20132","key":"41_CR48","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/j.artint.2004.04.004","volume":"157","author":"F. Lin","year":"2004","unstructured":"Lin F. and Zhao Y. (2004). ASSAT: computing answer sets of a logic program by SAT solvers. Artif. Intell. 157(1\u20132): 115\u2013137","journal-title":"Artif. Intell."},{"key":"41_CR49","doi-asserted-by":"crossref","unstructured":"Lowe, G.: Breaking and fixing the Needham\u2013Shroeder Public-Key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) Proceedings of TACAS\u201996, LNCS, vol. 1055, pp. 147\u2013166. Springer (1996)","DOI":"10.1007\/3-540-61042-1_43"},{"key":"41_CR50","doi-asserted-by":"crossref","unstructured":"Lowe, G.: A hierarchy of authentication specifications. In: Proceedings of the 10th IEEE Computer Security Foundations Workshop (CSFW\u201997), pp. 31\u201343. IEEE Computer Society Press (1997)","DOI":"10.1109\/CSFW.1997.596782"},{"key":"41_CR51","unstructured":"Lowe, G.: Towards a completeness result for model checking of security protocols. In: Proceedings of CSFW\u201998. IEEE Computer Society Press (1998). URL http:\/\/citeseer.nj.nec.com\/article\/lowe98towards.html"},{"key":"41_CR52","doi-asserted-by":"crossref","unstructured":"Marrero, W.R., Clarke, E.M., Jha, S.: Model checking for security protocols. In: DIMACS Workshop on Design and Formal Verication of Security Protocols (1997)","DOI":"10.21236\/ADA327281"},{"issue":"1","key":"41_CR53","doi-asserted-by":"crossref","first-page":"1057","DOI":"10.1016\/S0304-3975(02)00596-0","volume":"290","author":"F. Martinelli","year":"2003","unstructured":"Martinelli F. (2003). Analysis of security protocols as open systems. Theor. Comput Sci. 290(1): 1057\u20131106","journal-title":"Theor. Comput Sci."},{"key":"41_CR54","doi-asserted-by":"crossref","unstructured":"Millen, J.K., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: Proceedings of the ACM Conference on Computer and Communications Security CCS\u201901, pp. 166\u2013175 (2001)","DOI":"10.1145\/501983.502007"},{"key":"41_CR55","unstructured":"Mitchell, J.C., Mitchell, M., Stern, U.: Automated analysis of cryptographic protocols using murphi. In: Proceedings of IEEE Symposium on Security and Privacy, pp. 141\u2013153 (1997)"},{"key":"41_CR56","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference (DAC\u201901) (2001). URL http:\/\/www.ee.princeton.edu\/~chaff\/DAC2001v56.pdf"},{"key":"41_CR57","unstructured":"Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Tech. Rep. CSL-78-4, Xerox Palo Alto Research Center, Palo Alto (1978). Reprinted June 1982"},{"issue":"3\u20134","key":"41_CR58","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1023\/A:1018930122475","volume":"25","author":"I. Niemel\u00e4","year":"1999","unstructured":"Niemel\u00e4 I. (1999). Logic programs with stable model semantics as a constraint programming paradigm. Ann. Math. Artif. Intell. 25(3\u20134): 241\u2013273","journal-title":"Ann. Math. Artif. Intell."},{"issue":"1","key":"41_CR59","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L.C. Paulson","year":"1998","unstructured":"Paulson L.C. (1998). The inductive approach to verifying cryptographic protocols. J. Comput. Security 6(1): 85\u2013128","journal-title":"J. Comput. Security"},{"key":"41_CR60","unstructured":"Rintanen, J., Heljanko, K., Niemel\u00e4, I.: Planning as satisfiability: parallel plans and algorithms for plan search (2005). Submitted for journal publication. Eearlier version: Technical report 216, Albert-Ludwigs-Universit\u00e4t Freiburg, Institut fnr Informatik, 2005. Available at URL http:\/\/www.informatik.uni-freiburg.de\/~rintanen"},{"key":"41_CR61","unstructured":"Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions is NP-complete. In: Proceedings of the 14th IEEE Computer Security Foundations Workshop. IEEE Computer Society Press (2001)"},{"key":"41_CR62","doi-asserted-by":"crossref","first-page":"47","DOI":"10.3233\/JCS-2001-91-203","volume":"9","author":"D. Song","year":"2001","unstructured":"Song D., Berezin S. and Perrig A. (2001). Athena: a novel approach to efficient automatic security protocol analysis. J. Comput. Security 9: 47\u201374","journal-title":"J. Comput. Security"},{"key":"41_CR63","volume-title":"Logic: A Foundation for Computer Science","author":"V. Sperschneider","year":"1991","unstructured":"Sperschneider V. and Antoniou G. (1991). Logic: A Foundation for Computer Science. Addison-Wesley, Reading"},{"key":"41_CR64","unstructured":"Turuani, M.: S\u00e9curit\u00e9 des Protocoles Cryptographiques: D\u00e9cidabilit\u00e9 et Complexit\u00e9. Ph.D. thesis, Universit\u00e9 Henri Poincar\u00e9, Nancy (2003)"}],"container-title":["International Journal of Information Security"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10207-007-0041-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10207-007-0041-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10207-007-0041-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T03:35:59Z","timestamp":1737430559000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10207-007-0041-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,9,21]]},"references-count":64,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2008,1]]}},"alternative-id":["41"],"URL":"https:\/\/doi.org\/10.1007\/s10207-007-0041-y","relation":{},"ISSN":["1615-5262","1615-5270"],"issn-type":[{"value":"1615-5262","type":"print"},{"value":"1615-5270","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,9,21]]}}}