Detail publikace

A Security Formal Verification Method for Protocols Using Cryptographic Contactless Smart Cards

Originální název

A Security Formal Verification Method for Protocols Using Cryptographic Contactless Smart Cards

Anglický název

A Security Formal Verification Method for Protocols Using Cryptographic Contactless Smart Cards

Jazyk

en

Originální abstrakt

We present a method of contactless smart card protocol modeling suitable for finding vulnerabilities using model checking. Smart cards are used in applications that require high level of security, such as payment applications, therefore it should be ensured that the implementation does not contain any vulnerabilities. High level application specifications may lead to different implementations. Protocol that is proved to be secure on high level and that uses secure smart card can be implemented in more than one way; some of these implementations are secure, some of them introduce vulnerabilities to the application. The goal of this paper is to provide a method that can be used to create a model of arbitrary smart card, with focus on contactless smart cards, to create a model of the protocol, and to use model checking to find attacks in this model. AVANTSSAR Platform was used for the formal verification, the models are written in the ASLan++ language. Examples demonstrate the usability of the proposed method.

Anglický abstrakt

We present a method of contactless smart card protocol modeling suitable for finding vulnerabilities using model checking. Smart cards are used in applications that require high level of security, such as payment applications, therefore it should be ensured that the implementation does not contain any vulnerabilities. High level application specifications may lead to different implementations. Protocol that is proved to be secure on high level and that uses secure smart card can be implemented in more than one way; some of these implementations are secure, some of them introduce vulnerabilities to the application. The goal of this paper is to provide a method that can be used to create a model of arbitrary smart card, with focus on contactless smart cards, to create a model of the protocol, and to use model checking to find attacks in this model. AVANTSSAR Platform was used for the formal verification, the models are written in the ASLan++ language. Examples demonstrate the usability of the proposed method.

BibTex


@article{BUT130946,
  author="Martin {Henzl} and Petr {Hanáček}",
  title="A Security Formal Verification Method for Protocols Using Cryptographic Contactless Smart Cards",
  annote="
We present a method of contactless smart card protocol modeling suitable for
finding vulnerabilities using model checking. Smart cards are used in
applications that require high level of security, such as payment applications,
therefore it should be ensured that the implementation does not contain any
vulnerabilities. High level application specifications may lead to different
implementations. Protocol that is proved to be secure on high level and that uses
secure smart card can be implemented in more than one way; some of these
implementations are secure, some of them introduce vulnerabilities to the
application. The goal of this paper is to provide a method that can be used to
create a model of arbitrary smart card, with focus on contactless smart cards, to
create a model of the protocol, and to use model checking to find attacks in this
model. AVANTSSAR Platform was used for the formal verification, the models are
written in the ASLan++ language. Examples demonstrate the usability of the
proposed method.",
  address="NEUVEDEN",
  booktitle="Radioengineering",
  chapter="130946",
  edition="NEUVEDEN",
  howpublished="print",
  institution="NEUVEDEN",
  number="1",
  volume="2016",
  year="2016",
  month="april",
  pages="132--139",
  publisher="NEUVEDEN",
  type="journal article in Web of Science"
}