Detecting Attacks on Security Protocols Using Model Checking

The increased use of computer networks, distributed systems and wireless mobile systems requires the use of effective security protocols to ensure properties such as authentication, data integrity or non-repudiation. However, the design of these security protocols is highly complex and error-prone task. Thus, formal verification of these protocols is an imperative step in their development. There are several ways in which a security protocol can be verified, including theorem proving, deductive methods, programming logic, modal logic and model checking.This paper concerns the detection of attacks on security protocols using model checking. After introducing a categorisation of attacks, the general approach of setting up a model checker to detect these attacks is discussed. As a case study, the AVISPA tool is applied to detect a parallel session attack on a key distribution and authentication protocol.