Publication detail

Modeling of Contactless Smart Card Protocols and Automated Vulnerability Finding

HENZL, M. HANÁČEK, P.

Original Title

Modeling of Contactless Smart Card Protocols and Automated Vulnerability Finding

English Title

Modeling of Contactless Smart Card Protocols and Automated Vulnerability Finding

Type

conference paper

Language

en

Original Abstract

We present a method of automated vulnerability finding in protocols that use contactless smart cards. We focus on smart cards with contactless interface because they are simpler than their counterparts with contact interface and provide less functionality, which can be modeled more easily. Our method uses model checking to find possible attacks in a model of the protocol implementation on particular smart card. There is a possibility to model arbitrary smart card, we demonstrate this method on one of the currently most widespread contactless smart cards - the Mifare DESFire. Using our method we were able to locate a couple of weaknesses of this smart card which may cause vulnerability if the protocol is not implemented properly. This method can be used by developers to evaluate security of their protocol implementation on particular smart card.

English abstract

We present a method of automated vulnerability finding in protocols that use contactless smart cards. We focus on smart cards with contactless interface because they are simpler than their counterparts with contact interface and provide less functionality, which can be modeled more easily. Our method uses model checking to find possible attacks in a model of the protocol implementation on particular smart card. There is a possibility to model arbitrary smart card, we demonstrate this method on one of the currently most widespread contactless smart cards - the Mifare DESFire. Using our method we were able to locate a couple of weaknesses of this smart card which may cause vulnerability if the protocol is not implemented properly. This method can be used by developers to evaluate security of their protocol implementation on particular smart card.

Keywords

contactless smart card, security, vulnerability, model, Mifare DESFire

RIV year

2013

Released

05.07.2013

Publisher

IEEE Computer Society

Location

Chengdu

ISBN

978-0-7695-5010-7

Book

2013 International Symposium on Biometrics and Security Technologies (ISBAST)

Edition

NEUVEDEN

Edition number

NEUVEDEN

Pages from

141

Pages to

148

Pages count

8

Documents

BibTex


@inproceedings{BUT104512,
  author="Martin {Henzl} and Petr {Hanáček}",
  title="Modeling of Contactless Smart Card Protocols and Automated Vulnerability Finding",
  annote="We present a method of automated vulnerability finding in protocols that use
contactless smart cards. We focus on smart cards with contactless interface
because they are simpler than their counterparts with contact interface and
provide less functionality, which can be modeled more easily. Our method uses
model checking to find possible attacks in a model of the protocol implementation
on particular smart card. There is a possibility to model arbitrary smart card,
we demonstrate this method on one of the currently most widespread contactless
smart cards - the Mifare DESFire. Using our method we were able to locate
a couple of weaknesses of this smart card which may cause vulnerability if the
protocol is not implemented properly. This method can be used by developers to
evaluate security of their protocol implementation on particular smart card.",
  address="IEEE Computer Society",
  booktitle="2013 International Symposium on Biometrics and Security Technologies (ISBAST)",
  chapter="104512",
  edition="NEUVEDEN",
  howpublished="print",
  institution="IEEE Computer Society",
  year="2013",
  month="july",
  pages="141--148",
  publisher="IEEE Computer Society",
  type="conference paper"
}