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

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F16%3APU121602" target="_blank" >RIV/00216305:26230/16:PU121602 - isvavai.cz</a>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

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

Original language description

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.

Czech name

—

Czech description

—

Type

J_imp - Article in a specialist periodical, which is included in the Web of Science database

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

<a href="/en/project/ED1.1.00%2F02.0070" target="_blank" >ED1.1.00/02.0070: IT4Innovations Centre of Excellence</a><br>

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

Publication year

2016

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Name of the periodical

Radioengineering

ISSN

1210-2512

e-ISSN

—

Volume of the periodical

2016

Issue of the periodical within the volume

1

Country of publishing house

CZ - CZECH REPUBLIC

Number of pages

8

Pages from-to

132-139

UT code for WoS article

000373749300018

EID of the result in the Scopus database

2-s2.0-84964577779