Quantitative Analysis for Authentication of Low-cost RFID Tags

TL;DR

This paper presents a quantitative verification method for low-cost RFID protocols using Markov chains, enabling analysis of communication costs for up to 100 tags and aiding designers in protocol validation.

Contribution

It introduces a novel quantitative analysis approach for RFID protocols using DTMCs and the PRISM model checker, specifically tailored for low-cost RFID systems.

Findings

Quantified communication costs for RFID sessions.

Validated protocol performance with up to 100 tags.

Provided a methodology for cost-based RFID design validation.

Abstract

Formal analysis techniques are widely used today in order to verify and analyze communication protocols. In this work, we launch a quantitative verification 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.