Formal Computational Unlinkability Proofs of RFID Protocols
Cryptography and Security
2017-05-08 v1
Abstract
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.
Keywords
Cite
@article{arxiv.1705.02296,
title = {Formal Computational Unlinkability Proofs of RFID Protocols},
author = {Hubert Comon and Adrien Koutsos},
journal= {arXiv preprint arXiv:1705.02296},
year = {2017}
}