A Security Formal Verification Method for Protocols Using Cryptographic Contactless Smart Cards
| العنوان: | A Security Formal Verification Method for Protocols Using Cryptographic Contactless Smart Cards |
|---|---|
| المؤلفون: | Martin Henzl, Petr Hanacek |
| المصدر: | Radioengineering, Vol 25, Iss 1, Pp 132-139 (2016) Radioengineering. 2016 vol. 25, č. 1, s. 132-139. ISSN 1210-2512 |
| بيانات النشر: | Spolecnost pro radioelektronicke inzenyrstvi, 2016. |
| سنة النشر: | 2016 |
| مصطلحات موضوعية: | Computer science, 02 engineering and technology, Smart Card, Model Checking, MULTOS, 0502 economics and business, 0202 electrical engineering, electronic engineering, information engineering, Protocol, Electrical and Electronic Engineering, Formal verification, Contactless smart card, OpenPGP card, business.industry, 05 social sciences, 020206 networking & telecommunications, BasicCard, Smart card application protocol data unit, Formal Verification, Embedded system, Security, ASLan++, Open Smart Card Development Platform, Smart card, lcsh:Electrical engineering. Electronics. Nuclear engineering, business, lcsh:TK1-9971, 050203 business & management |
| الوصف: | 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 spec- ifications may lead to dierent 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 check- ing 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. |
| وصف الملف: | text; application/pdf |
| اللغة: | English |
| تدمد: | 1210-2512 |
| URL الوصول: | https://explore.openaire.eu/search/publication?articleId=doi_dedup___::946521aa94690ee873eaa5dc75d0909b http://www.radioeng.cz/fulltexts/2016/16_01_0132_0139.pdf |
| Rights: | OPEN |
| رقم الانضمام: | edsair.doi.dedup.....946521aa94690ee873eaa5dc75d0909b |
| قاعدة البيانات: | OpenAIRE |
| تدمد: | 12102512 |
|---|