Visible to the public Formal Computational Unlinkability Proofs of RFID Protocols

TitleFormal Computational Unlinkability Proofs of RFID Protocols
Publication TypeConference Paper
Year of Publication2017
AuthorsComon, H., Koutsos, A.
Conference Name2017 IEEE 30th Computer Security Foundations Symposium (CSF)
Date PublishedAug. 2017
PublisherIEEE
ISBN Number978-1-5386-3217-8
Keywordscommunication complexity, computational complete symbolic attacker, computational model, Computational modeling, cryptographic protocols, cryptography, formal computational unlinkability proofs, Hash functions, Human Behavior, human factors, Protocols, pubcrawl, radiofrequency identification, Resiliency, RFID, RFID protocols, RFIDs, security of data, security protocols, theorem proving, Tools, Turing machines, unlinkability
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: 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 omputational model.

URLhttps://ieeexplore.ieee.org/document/8049714/
DOI10.1109/CSF.2017.9
Citation Keycomon_formal_2017