Quantitative Analysis for Authentication of Low-cost RFID Tags

Formal analysis techniques are widely used today in order to verify and analyze communication protocols. In this work, we launch a quantitative analysis for the low-cost Radio Frequency Identification (RFID) protocol proposed by Song and Mitchell. The analysis exploits a Discrete-Time Markov Chain (DTMC) using the well-known PRISM model checker. We have managed to represent up to 100 RFID tags communicating with a reader and quantify each RFID session according to the protocol's computation and transmission cost requirements. As a consequence, not only does the proposed analysis provide quantitative verification results, but also it constitutes a methodology for RFID designers who want to validate their products under specific cost requirements.


Published in:
2011 Ieee 36Th Conference On Local Computer Networks (Lcn), 295-298
Presented at:
36th Annual IEEE Conference on Local Computer Networks (LCN), Bonn, GERMANY, Oct 04-07, 2011
Year:
2011
Publisher:
Ieee Computer Soc Press, Customer Service Center, Po Box 3014, 10662 Los Vaqueros Circle, Los Alamitos, Ca 90720-1264 Usa
ISBN:
978-1-61284-928-7
Keywords:
Laboratories:




 Record created 2012-06-25, last modified 2018-09-13


Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)