Sciweavers

SAFECOMP
2007
Springer

Intrusion Attack Tactics for the Model Checking of e-Commerce Security Guarantees

13 years 9 months ago
Intrusion Attack Tactics for the Model Checking of e-Commerce Security Guarantees
In existing security model-checkers the intruder’s behavior is defined as a message deducibility rule base governing use of eavesdropped information, with the aim to find out a message that is meant to be secret or to generate messages that impersonate some protocol participant(s). The advent of complex protocols like those used in e-commerce brings to the foreground intrusion attacks that are not always attributed to failures of secrecy or authentication. We introduce an intruder model that provides an open-ended base for the integration of multiple attack tactics. In our model checking approach, protocol correctness is checked by appropriate user-supplied assertions or reachability of invalid end states. Thus, the analyst can express e-commerce security guarantees that are not restricted to the absence of secrecy and the absence of authentication failures. The described intruder was implemented within the SPIN model-checker and revealed an integrity violation attack on the PayWord ...
Stylianos Basagiannis, Panagiotis Katsaros, Andrew
Added 09 Jun 2010
Updated 09 Jun 2010
Type Conference
Year 2007
Where SAFECOMP
Authors Stylianos Basagiannis, Panagiotis Katsaros, Andrew Pombortsis
Comments (0)