Formal Computational Unlinkability Proofs of RFID Protocols

摘要

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: 1) To design (and prove sound) axioms reflecting the properties of hash functions (Collision-Resistance, PRF). 2) To formalize computational unlinkability in the model. 3) To illustrate the method, providing the first formal proofs of unlinkability of RFID protocols, in the computational model.