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.

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

Quantitative Analysis for Authentication of Low-cost RFID Tags

Graph Chatbot

Chat with Graph Search

RE:SLAB — a load bearing system for open-ended component reuse in building structures

Lessons Learned from Data-Driven Building Control Experiments: Contrasting Gaussian Process-based MPC, Bilevel DeePC, and Deep Reinforcement Learning

Lessons Learned from Data-Driven Building Control Experiments: Contrasting Gaussian Process-based MPC, Bilevel DeePC, and Deep Reinforcement Learning

RE:SLAB — a load bearing system for open-ended component reuse in building structures