Sciweavers

Share
SCN
2011
Springer

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

9 years 6 months ago
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...
Stylianos Basagiannis, Panagiotis Katsaros, Andrew
Added 15 May 2011
Updated 15 May 2011
Type Journal
Year 2011
Where SCN
Authors Stylianos Basagiannis, Panagiotis Katsaros, Andrew Pombortsis
Comments (0)
books