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 ...

• Type: Conference
• Year: 2007
• Where: SAFECOMP
• Authors: Stylianos Basagiannis, Panagiotis Katsaros, Andrew Pombortsis
• Keywords: Appropriate User-supplied Assertions, Deducibility Rule Base, Intruder’s Behavior, SAFECOMP 2007