Article Preview
TopIntroduction
Security protocols are short concurrent communication programs designed to secure exchanges over a network, using encryption primitives. They are intended to achieve various goals depending on the target application, e.g. confidentiality, authenticity, and integrity. Their verification has shown its interest for detecting and preventing different types of attacks, e.g., eavesdropping, replay attack, password guessing attack, man-in-the-middle attack and quantum computer attack (Paul, Kumar, & Suman, 2019). Cryptographic protocols are ubiquitous and widely used in applications that require secure electronic transactions, such as banking, e-voting, e-commerce, e-mail exchange, and so on. They are also increasingly designed and used to secure new emerging technologies like the Internet of Things (IoT) (Kaur, Verma, Jain, & Kesswani, 2019), RFID tags, mobile phones, wireless sensors and Wi-Fi networks (Rath & Pattanayak, 2019). Cryptography appears here as an essential tool to ensure security properties, in particular by encryption algorithms and hash functions. Although security protocols are typically small, analysis by hand is an extremely challenging, error prone and time-consuming problem, since a protocol should work even when many runs are interleaved and in the presence of a malicious adversary. Failures in such protocols may lead to financial loss, violations of personal privacy, and real threats to the economy (Ben, 2011).
Recent model checking and automated verification approaches have made it possible to find and build attacks over protocols, which had apparently been undiscovered for many years. A famous example is the Needham-Schroeder protocol (Needham & Schroeder, 1978) on which Lowe (1995) has discovered a flaw 17 years after its publication. Hence, verification approaches are proposed to help protocol designers in writing, adjusting and strengthening the security protocol specification (Cramer, Damgard, & Nielsen, 2015; Schoenmakers, 2019). This article advances verification techniques for cryptographic protocols using formal methods with an emphasis on expressiveness, compactness and automation.
Let us briefly review some existing approaches used to analyze security protocols. Methods based on induction and theorem proving have been developed in the literature (Cortier, Kremer, & Warinschi, 2011; Paulson, 1997). Those methods ensure correctness proofs and they can handle protocols by considering several unbounded dimensions (unbounded number of parallel and sequential runs, unbounded number of principals, nonces, and encryption keys). However, unlike model checking, they are difficult to implement and not fully automated (require user interaction). Moreover, when the security verifier fails, it is difficult to build counter-examples violating some security properties. Other methods such as first-order resolution address the verification problem by attempting to prove correctness on unbounded protocols by means of the Horn logic formal language, which includes an inference procedure as well as suitable proof strategies. Those methods are automatic and successfully implemented using Prolog programs (Blanchet, 2001). However, the termination of their analysis is not guaranteed in general. In addition, protocol abstraction may lead to false positive results (false attacks).