# Formal Computational Unlinkability Proofs of RFID Protocols

## TL;DR

This paper develops a formal framework for proving RFID protocols are computationally unlinkable, introducing axioms for hash functions and demonstrating the first formal unlinkability proofs in the computational model.

## Contribution

It introduces a sound axiomatic framework for formal proofs of RFID protocol unlinkability in the computational model, filling a gap in formal security analysis.

## Key findings

- First formal proofs of RFID unlinkability in the computational model
- Development of axioms for hash function properties
- Formalization of computational 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: 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.