{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T15:23:33Z","timestamp":1781105013201,"version":"3.54.1"},"reference-count":27,"publisher":"IGI Global Scientific Publishing","issue":"4","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020,10,1]]},"abstract":"<p>Cryptographic protocols form the backbone of digital society. They are concurrent multiparty communication protocols that use cryptography to achieve security goals such as confidentiality, authenticity, integrity, etc., in the presence of adversaries. Unfortunately, protocol verification still represents a critical task and a major cost to engineer attack-free security protocols. Model checking and SAT-based techniques proved quite effective in this context. This article proposes an efficient automatic model checking approach that exemplifies a security property violation. In this approach, a protocol verification is abstracted as a compact planning problem, which is efficiently solved by a state-of-the-art SAT solver. The experiments performed on some real-world cryptographic protocols succeeded in detecting new logical attacks, violating some security properties. Those attacks encompass both \u201ctype flaw\u201d and \u201creplay\u201d attacks, which are difficult to tackle with the existing planning-based approaches.<\/p>","DOI":"10.4018\/ijisp.2020100101","type":"journal-article","created":{"date-parts":[[2020,9,8]],"date-time":"2020-09-08T07:14:17Z","timestamp":1599549257000},"page":"1-21","source":"Crossref","is-referenced-by-count":0,"title":["A SAT-Based Planning Approach for Finding Logical Attacks on Cryptographic Protocols"],"prefix":"10.4018","volume":"14","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3204-6065","authenticated-orcid":true,"given":"Noureddine","family":"Aribi","sequence":"first","affiliation":[{"name":"LITIO Lab., Universit\u00e9 Oran1, Oran, Algeria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yahia","family":"Lebbah","sequence":"additional","affiliation":[{"name":"LITIO Lab., Universit\u00e9 Oran1, Oran, Algeria"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"2432","reference":[{"key":"IJISP.2020100101-0","first-page":"21","article-title":"V\u00e9rification des protocoles cryptographiques avec le langage PDDL et les solveurs SAT","author":"N.Aribi","year":"2008","journal-title":"JFPC 2008 \u2013 Quatri\u00e8mes Journ\u00e9es Francophones de Programmation par Contraintes"},{"key":"IJISP.2020100101-1","doi-asserted-by":"crossref","unstructured":"Armando, A., Carbone, R., & Compagna, L. (2014). SATMC: A SAT-Based Model Checker for Security-Critical Systems. In Tacas. Academic Press.","DOI":"10.1007\/978-3-642-54862-8_3"},{"key":"IJISP.2020100101-2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_22"},{"key":"IJISP.2020100101-3","unstructured":"Ben, S. (2011). Formal verification of cryptographic protocols with automated reasoning. Unpublished doctoral dissertation, University of Birmingham."},{"key":"IJISP.2020100101-4","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2001.930138"},{"key":"IJISP.2020100101-5","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45789-5_25"},{"key":"IJISP.2020100101-6","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(96)00047-1"},{"key":"IJISP.2020100101-7","doi-asserted-by":"publisher","DOI":"10.1145\/363516.363528"},{"key":"IJISP.2020100101-8","unstructured":"Compagna, L. (2005). SAT-based Model-Checking of Security Protocols. Unpublished doctoral dissertation, Universit\u00e0 degli Studi di Genova and the University of Edinburgh."},{"key":"IJISP.2020100101-9","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9187-9"},{"key":"IJISP.2020100101-10","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107337756"},{"key":"IJISP.2020100101-11","unstructured":"Delaune, S., & Klay, F. (2004, November). V\u00e9rification automatique appliqu\u00e9e \u00e0 un protocole de commerce \u00e9lectronique. In Actes des 6\u00e8mes Journ\u00e9es Doctorales Informatique et R\u00e9seau (JDIR\u201904) (p. 260-269). Lannion, France."},{"issue":"2","key":"IJISP.2020100101-12","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":"D.Dolev","year":"1983","journal-title":"IEEE Transactions on Information Theory"},{"key":"IJISP.2020100101-13","first-page":"36","article-title":"Analyzing a library of security protocols using Casper and FDR.","author":"B.Donovan","year":"1999","journal-title":"Proceedings of the Workshop on Formal Methods and Security Protocols"},{"key":"IJISP.2020100101-14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70936-7_10"},{"key":"IJISP.2020100101-15","doi-asserted-by":"publisher","DOI":"10.1613\/jair.855"},{"key":"IJISP.2020100101-16","doi-asserted-by":"publisher","DOI":"10.1613\/jair.655"},{"key":"IJISP.2020100101-17","doi-asserted-by":"publisher","DOI":"10.4018\/IJISP.2019010106"},{"key":"IJISP.2020100101-18","unstructured":"Kautz, H. A., McAllester, D., & Selman, B. (1996). Encoding plans in propositional logic. In Proceedings of the fifth international conference on the principle of knowledge representation and reasoning (KR\u201996) (pp. 374\u2013384). Academic Press."},{"key":"IJISP.2020100101-19","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(95)00144-2"},{"key":"IJISP.2020100101-20","first-page":"141","article-title":"Automated Analysis of Crypto-graphic Protocols Using Mur \u03c6","author":"J. C.Mitchell","year":"1997","journal-title":"Proceedings of the 1997 conference on security and privacy"},{"key":"IJISP.2020100101-21","doi-asserted-by":"publisher","DOI":"10.1145\/359657.359659"},{"key":"IJISP.2020100101-22","doi-asserted-by":"publisher","DOI":"10.1145\/24592.24594"},{"key":"IJISP.2020100101-23","doi-asserted-by":"publisher","DOI":"10.4018\/IJISP.2019100101"},{"key":"IJISP.2020100101-24","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.1997.596788"},{"key":"IJISP.2020100101-25","doi-asserted-by":"publisher","DOI":"10.4018\/IJISP.2019010104"},{"key":"IJISP.2020100101-26","unstructured":"Schoenmakers, B. (2019, February). Lecture notes in cryptographic protocols. Technical University of Eindhoven, Department of Mathematics and Computer Science."}],"container-title":["International Journal of Information Security and Privacy"],"original-title":[],"language":"ng","link":[{"URL":"https:\/\/www.igi-global.com\/viewtitle.aspx?TitleId=262083","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,6]],"date-time":"2022-05-06T11:57:55Z","timestamp":1651838275000},"score":1,"resource":{"primary":{"URL":"https:\/\/services.igi-global.com\/resolvedoi\/resolve.aspx?doi=10.4018\/IJISP.2020100101"}},"subtitle":[""],"short-title":[],"issued":{"date-parts":[[2020,10,1]]},"references-count":27,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2020,10]]}},"URL":"https:\/\/doi.org\/10.4018\/ijisp.2020100101","relation":{},"ISSN":["1930-1650","1930-1669"],"issn-type":[{"value":"1930-1650","type":"print"},{"value":"1930-1669","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,10,1]]}}}