A concept of automated vulnerability search in contactless communication applications

Designing and implementing secure applications which use contactless communication link is difficult even when secure hardware is used. Many current proximity devices, such as contactless smart cards or near field communication devices, are verified to be highly secure; however, inappropriate protocol implementation may result in the leak of sensitive information, even if the protocol is also secure by itself. In this paper we show a concept of automated vulnerability search in protocol implementation by using verification methods, which should help developers to verify their applications. We also show simple example of possible attack on seemingly secure payment protocol implemented using seemingly secure smart card to show the way the adversary can abuse improper implementation. The vulnerability the attacker exploits can be in one command or in a combination of commands, which are not vulnerable individually. It is not easy to find such combinations manually, this is where the automated verification methods are put to use. A model checker, provided with an appropriate model, can automatically find vulnerabilities which are not likely to be found manually. The model can be created by the actual communication analysis. We wanted to show that the adversary does not have to have the access to the source code of the application to perform a successful attack, so a platform for the application analysis from the actual contactless communication was developed. The platform provides eavesdropping, altering data for man-in-the-middle attack, and emulating of both communication parties. The source code can help the analysis, but would not be sufficient by itself, so creating model from source code was left for future research. When the model checker finds vulnerability, an attack can be executed. The attack can be either successful, revealing real vulnerability which must be fixed, or unsuccessful, which would result in the model refinement and another model checker run.