Publication detail

A Concept of Automated Vulnerability Search in Contactless Communication Applications

HENZL, M. HANÁČEK, P. JURNEČKA, P. KAČIC, M.

Original Title

A Concept of Automated Vulnerability Search in Contactless Communication Applications

Type

article in a collection out of WoS and Scopus

Language

English

Original Abstract

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.

Keywords

security, vulnerability, contactless, proximity, smart card, Mifare DESFire, near field communication, NFC

Authors

HENZL, M.; HANÁČEK, P.; JURNEČKA, P.; KAČIC, M.

RIV year

2012

Released

18. 10. 2012

Publisher

Institute of Electrical and Electronics Engineers

Location

Boston

ISBN

978-1-4673-4807-2

Book

Proceedings 46th Annual IEEE International Carnahan Conference on Security Technology

Pages from

180

Pages to

186

Pages count

6

BibTex

@inproceedings{BUT96971,
  author="Martin {Henzl} and Petr {Hanáček} and Peter {Jurnečka} and Matej {Kačic}",
  title="A Concept of Automated Vulnerability Search in Contactless Communication Applications",
  booktitle="Proceedings 46th Annual IEEE International Carnahan Conference on Security Technology",
  year="2012",
  pages="180--186",
  publisher="Institute of Electrical and Electronics Engineers",
  address="Boston",
  isbn="978-1-4673-4807-2"
}