Formal verification of cryptographic protocol for secure RFID system

Hyun Seok Kim, Jung Hyun Oh, Ju Bae Kim, Yeon Oh Jeong, Jin Young Choi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)

Abstract

RFID technology has become one of the most hotly debated ubiquitous computing technologies, and public fears of its alleged capability for comprehensive surveillance have prompted a flurry of research trying to alleviate such concerns. Security mechanisms for RFID systems are therefore of utmost important. In this paper, we describe problems of previous work on RFlD security protocols and specify several known attacks with Casper (A Compiler of Security Protocol Analyzer), then verify their security properties such as secrecy and authentication using the FDR (Failure Divergence Refinement) model checking tool. Finally, we discuss practical issue of the hash authentication RFID security protocol, which guarantee data privacy and authentication between a tag and a reader using Casper and FDR.

Original languageEnglish
Title of host publicationProceedings - 4th International Conference on Networked Computing and Advanced Information Management, NCM 2008
Pages470-477
Number of pages8
Volume2
DOIs
Publication statusPublished - 2008 Dec 29
Event4th International Conference on Networked Computing and Advanced Information Management, NCM 2008 - Gyeongju, Korea, Republic of
Duration: 2008 Sep 22008 Sep 4

Other

Other4th International Conference on Networked Computing and Advanced Information Management, NCM 2008
CountryKorea, Republic of
CityGyeongju
Period08/9/208/9/4

Fingerprint

Radio frequency identification (RFID)
Authentication
Network protocols
Data privacy
Ubiquitous computing
Model checking
Formal verification

Keywords

  • Authentication
  • Model checking
  • Privacy
  • RFID

ASJC Scopus subject areas

  • Computer Networks and Communications
  • Information Systems

Cite this

Kim, H. S., Oh, J. H., Kim, J. B., Jeong, Y. O., & Choi, J. Y. (2008). Formal verification of cryptographic protocol for secure RFID system. In Proceedings - 4th International Conference on Networked Computing and Advanced Information Management, NCM 2008 (Vol. 2, pp. 470-477). [4624188] https://doi.org/10.1109/NCM.2008.21

Formal verification of cryptographic protocol for secure RFID system. / Kim, Hyun Seok; Oh, Jung Hyun; Kim, Ju Bae; Jeong, Yeon Oh; Choi, Jin Young.

Proceedings - 4th International Conference on Networked Computing and Advanced Information Management, NCM 2008. Vol. 2 2008. p. 470-477 4624188.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Kim, HS, Oh, JH, Kim, JB, Jeong, YO & Choi, JY 2008, Formal verification of cryptographic protocol for secure RFID system. in Proceedings - 4th International Conference on Networked Computing and Advanced Information Management, NCM 2008. vol. 2, 4624188, pp. 470-477, 4th International Conference on Networked Computing and Advanced Information Management, NCM 2008, Gyeongju, Korea, Republic of, 08/9/2. https://doi.org/10.1109/NCM.2008.21
Kim HS, Oh JH, Kim JB, Jeong YO, Choi JY. Formal verification of cryptographic protocol for secure RFID system. In Proceedings - 4th International Conference on Networked Computing and Advanced Information Management, NCM 2008. Vol. 2. 2008. p. 470-477. 4624188 https://doi.org/10.1109/NCM.2008.21
Kim, Hyun Seok ; Oh, Jung Hyun ; Kim, Ju Bae ; Jeong, Yeon Oh ; Choi, Jin Young. / Formal verification of cryptographic protocol for secure RFID system. Proceedings - 4th International Conference on Networked Computing and Advanced Information Management, NCM 2008. Vol. 2 2008. pp. 470-477
@inproceedings{6e281fc8491049cfbecbebf69e7dfc74,
title = "Formal verification of cryptographic protocol for secure RFID system",
abstract = "RFID technology has become one of the most hotly debated ubiquitous computing technologies, and public fears of its alleged capability for comprehensive surveillance have prompted a flurry of research trying to alleviate such concerns. Security mechanisms for RFID systems are therefore of utmost important. In this paper, we describe problems of previous work on RFlD security protocols and specify several known attacks with Casper (A Compiler of Security Protocol Analyzer), then verify their security properties such as secrecy and authentication using the FDR (Failure Divergence Refinement) model checking tool. Finally, we discuss practical issue of the hash authentication RFID security protocol, which guarantee data privacy and authentication between a tag and a reader using Casper and FDR.",
keywords = "Authentication, Model checking, Privacy, RFID",
author = "Kim, {Hyun Seok} and Oh, {Jung Hyun} and Kim, {Ju Bae} and Jeong, {Yeon Oh} and Choi, {Jin Young}",
year = "2008",
month = "12",
day = "29",
doi = "10.1109/NCM.2008.21",
language = "English",
isbn = "9780769533223",
volume = "2",
pages = "470--477",
booktitle = "Proceedings - 4th International Conference on Networked Computing and Advanced Information Management, NCM 2008",

}

TY - GEN

T1 - Formal verification of cryptographic protocol for secure RFID system

AU - Kim, Hyun Seok

AU - Oh, Jung Hyun

AU - Kim, Ju Bae

AU - Jeong, Yeon Oh

AU - Choi, Jin Young

PY - 2008/12/29

Y1 - 2008/12/29

N2 - RFID technology has become one of the most hotly debated ubiquitous computing technologies, and public fears of its alleged capability for comprehensive surveillance have prompted a flurry of research trying to alleviate such concerns. Security mechanisms for RFID systems are therefore of utmost important. In this paper, we describe problems of previous work on RFlD security protocols and specify several known attacks with Casper (A Compiler of Security Protocol Analyzer), then verify their security properties such as secrecy and authentication using the FDR (Failure Divergence Refinement) model checking tool. Finally, we discuss practical issue of the hash authentication RFID security protocol, which guarantee data privacy and authentication between a tag and a reader using Casper and FDR.

AB - RFID technology has become one of the most hotly debated ubiquitous computing technologies, and public fears of its alleged capability for comprehensive surveillance have prompted a flurry of research trying to alleviate such concerns. Security mechanisms for RFID systems are therefore of utmost important. In this paper, we describe problems of previous work on RFlD security protocols and specify several known attacks with Casper (A Compiler of Security Protocol Analyzer), then verify their security properties such as secrecy and authentication using the FDR (Failure Divergence Refinement) model checking tool. Finally, we discuss practical issue of the hash authentication RFID security protocol, which guarantee data privacy and authentication between a tag and a reader using Casper and FDR.

KW - Authentication

KW - Model checking

KW - Privacy

KW - RFID

UR - http://www.scopus.com/inward/record.url?scp=57849127238&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=57849127238&partnerID=8YFLogxK

U2 - 10.1109/NCM.2008.21

DO - 10.1109/NCM.2008.21

M3 - Conference contribution

AN - SCOPUS:57849127238

SN - 9780769533223

VL - 2

SP - 470

EP - 477

BT - Proceedings - 4th International Conference on Networked Computing and Advanced Information Management, NCM 2008

ER -