Conference paper

HENZL Martin, HANÁČEK Petr, JURNEČKA Peter and KAČIC Matej. A Concept of Automated Vulnerability Search in Contactless Communication Applications. In: Proceedings 46th Annual IEEE International Carnahan Conference on Security Technology. Boston: Institute of Electrical and Electronics Engineers, 2012, pp. 180-186. ISBN 978-1-4673-4807-2.
Publication language:english
Original title:A Concept of Automated Vulnerability Search in Contactless Communication Applications
Title (cs):Koncept automatického hledání zranitelností v aplikacích využívajících bezkontaktní komunikaci
Proceedings:Proceedings 46th Annual IEEE International Carnahan Conference on Security Technology
Place:Boston, US
Publisher:Institute of Electrical and Electronics Engineers
security, vulnerability, contactless, proximity, smart card, Mifare DESFire, near field communication, NFC
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.
   author = {Martin Henzl and Petr Han{\'{a}}{\v{c}}ek and Peter
	Jurne{\v{c}}ka and Matej Ka{\v{c}}ic},
   title = {A Concept of Automated Vulnerability Search in Contactless
	Communication Applications},
   pages = {180--186},
   booktitle = {Proceedings 46th Annual IEEE International Carnahan
	Conference on Security Technology},
   year = {2012},
   location = {Boston, US},
   publisher = {Institute of Electrical and Electronics Engineers},
   ISBN = {978-1-4673-4807-2},
   language = {english},
   url = {}

Your IPv4 address:
Switch to IPv6 connection

DNSSEC [dnssec]