A SAT-Based Planning Approach for Finding Logical Attacks on Cryptographic Protocols

Noureddine Aribi and Yahia Lebbah
Additional contact information
Noureddine Aribi: LITIO Lab., Université Oran1, Oran, Algeria
Yahia Lebbah: LITIO Lab., Université Oran1, Oran, Algeria

International Journal of Information Security and Privacy (IJISP), 2020, vol. 14, issue 4, 1-21

Abstract: 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 “type flaw” and “replay” attacks, which are difficult to tackle with the existing planning-based approaches.

Date: 2020
References: Add references at CitEc
Citations:

Downloads: (external link)
http://services.igi-global.com/resolvedoi/resolve. ... 018/IJISP.2020100101 (application/pdf)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:igg:jisp00:v:14:y:2020:i:4:p:1-21

Access Statistics for this article

International Journal of Information Security and Privacy (IJISP) is currently edited by Yassine Maleh

More articles in International Journal of Information Security and Privacy (IJISP) from IGI Global
Bibliographic data for series maintained by Journal Editor ().