A Formal Analysis Model for Tracking Attacks on RFID Security Protocols
Yuanyuan Yang, You Yu, Xiaoxiao Zhang · 2024
In order to solve the problem of malicious tracking attacks that may exist in RFID security protocols, a formal analysis model named TAMET was proposed. In this model, two important concepts were firstly defined, i.e. the initial messages set of attacker and the operation behaviors set of attacker, which were used to formally regulate the attacker's ability. Then, the key indicators for tracking attack in TAMET model, i.e. tag eigenvalue, was introduced, and the relationship between tracking attacks and tag eigenvalue was proved. Finally, using the TAMET model, the tag eigenvalue of CP-LRDP was found and a tracking attack on the protocol was illustrated, which explicitly proved the effectiveness of the TAMET model.