Formal Computational Unlinkability Proofs of RFID Protocols
This work addresses security verification for RFID systems, though it is incremental as it extends existing formal methods to a specific domain.
The authors tackled the problem of formally proving RFID protocol security by developing a computational framework based on the computationally complete symbolic attacker model, resulting in the first formal proofs of unlinkability for RFID protocols in this model.
We set up a framework for the formal proofs of RFID protocols in the computational model. We rely on the so-called computationally complete symbolic attacker model. Our contributions are: i) To design (and prove sound) axioms reflecting the properties of hash functions (Collision-Resistance, PRF); ii) To formalize computational unlinkability in the model; iii) To illustrate the method, providing the first formal proofs of unlinkability of RFID protocols, in the computational model.