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.
In this paper, we describe an attack against one of the
Oblivious-Transfer-based blind signatures scheme, proposed in [1]. An attacker
with a primitive capability of producing specific-range random numbers, while
exhibiting a partial MITM behavior, is able to corrupt the communication
between the protocol participants. The attack is quite efficient as it leads to
a protocol communication corruption and has a sound-minimal computational cost.
We propose a solution to fix the security flaw.
Model checking is a widespread automatic formal analysis that has been
successful in discovering flaws in security protocols. However existing
possibilities for state space explosion still hinder analyses of complex
protocols and protocol configurations. Message Inspection, is a technique that
delimits the branching of the state space due to the intruder model without
excluding possible attacks. In a preliminary simulation, the intruder model
tags the eavesdropped messages with specific metadata that enable validation of
feasibility of possible attack actions.