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.