David Baelde, Stéphanie Delaune, and Solène Moreau. A Method for Proving Unlinkability of Stateful Protocols. In Proceedings of the 33rd IEEE Computer Security Foundations Symposium (CSF'20), pp. 169–183, IEEE Computer Society Press, Virtual conference, June 2020.
The rise of contactless and wireless devices such as mobile phones and RFID chips justifies significant concerns over privacy, and calls for communication protocols that ensure some form of unlinkability. Formally specifying this property is difficult and context-dependent, and analysing it is very complex; as is common with security protocols, several incorrect unlinkability claims can be found in the literature. Formal verification is therefore desirable, but current techniques are not sufficient to directly analyse unlinkability. In a recent work by Hirshi et al. (published at JCS in 2019), two conditions have been identified that imply unlinkability and can be automatically verified. That work, however, only considers a restricted class of protocols. We adapt their formal definition as well as their proof method to the common setting of RFID authentication protocols, where readers access a central database of authorised users. Moreover, we also consider protocols where readers may update their database, and tags may also carry a mutable state. We propose sufficient conditions to ensure unlinkability, find new attacks, and obtain new proofs of unlinkability using Tamarin to establish our sufficient conditions.
@inproceedings{BDM-csf20,
abstract = {The rise of contactless and wireless devices such as mobile phones
and RFID chips justifies significant concerns over privacy,
and calls for communication protocols that ensure some form of
unlinkability. Formally specifying this property is difficult
and context-dependent, and analysing it is very complex;
as is common with security protocols, several incorrect unlinkability
claims can be found in the literature.
Formal verification is therefore desirable, but current techniques
are not sufficient to directly analyse unlinkability.
In a recent work by Hirshi et al. (published at JCS in 2019), two conditions have been
identified that imply unlinkability and can be automatically verified.
That work, however, only considers a restricted class of protocols.
We adapt their formal definition as well as their proof method
to the common setting of RFID authentication protocols, where
readers access a central database of authorised users. Moreover, we
also consider protocols where readers may update their database, and
tags may also carry a mutable state.
We propose sufficient conditions to ensure unlinkability,
find new attacks, and obtain new proofs of unlinkability using
Tamarin to establish our sufficient conditions.
},
address = {Virtual conference},
author = {Baelde, David and Delaune, St{\'e}phanie and Moreau, Sol{\`e}ne},
booktitle = {{P}roceedings of the 33rd {IEEE} {C}omputer
{S}ecurity {F}oundations {S}ymposium ({CSF}'20)},
month = jun,
pages = {169--183},
publisher = {{IEEE} Computer Society Press},
title = {A Method for Proving Unlinkability of Stateful~Protocols},
year = {2020},
acronym = {{CSF}'20},
nmonth = {6},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}