Synthesis of attack actions using model checking for the verification of security protocols

Model checking cryptographic protocols have evolved to a valuable method for discovering counterintuitive security flaws, which make possible for a hostile agent to subvert the goals of the protocol. Published works and existing security analysis tools are usually based on general intruder models that embody at least some aspects of the seminal work of DolevYao, in an attempt to detect failures of secrecy. In this work, we propose an alternative intruder model, which is based on a thorough analysis of how potential attacks might proceed. We introduce an intruder model that provides an open-ended base for the integration of multiple basic attack tactics. Those attack tactics have the possibility to be combined, in a way to compose complex attack actions that require a number of procedural steps from the intruder’s side, such as a Denial of Service attack. In our model checking approach, protocol correctness is checked by appropriate user-supplied assertions or reachability of invalid...

• Type: Journal
• Year: 2011
• Where: SCN
• Authors: Stylianos Basagiannis, Panagiotis Katsaros, Andrew Pombortsis
• Keywords: Attack Tactics, Communications, Intruder Model, Model, SCN 2011