Stéphanie Delaune: Proving Unlinkability using Proverif through Desynchronised Bi-Processes

Proving Unlinkability using Proverif through Desynchronised Bi-Processes

David Baelde, Alexandre Debant, and Stéphanie Delaune. Proving Unlinkability using Proverif through Desynchronised Bi-Processes. In Proceedings of the 36th IEEE Computer Security Foundations Symposium (CSF'23), IEEE Computer Society Press, Dubrovnik, Croatia, July 2023.

Download

[PDF]

Abstract

Unlinkability is a privacy property of crucial importance for severalsystems such as mobile phones or RFID chips. Analysing this securityproperty is very complex, and highly error-prone. Therefore, formalverification with machine support is desirable.Unfortunately, existing techniques are not sufficient to directlyapply verification tools to automatically prove unlinkability.In this paper, we overcome this limitation by defining a simpletransformation that will exploit some specific features of Proverif. This transformation, together with some genericaxioms, allows the tool to successfullyconclude on several case studies. We have implemented our approach,effectively obtaining direct proofs of unlinkability on several protocols that were, until now,out of reach of automatic verification tools.

BibTeX

@inproceedings{BDD-csf23,
  abstract =      {Unlinkability is a privacy property of crucial importance for several
systems such as mobile phones or RFID chips. Analysing this security
property is very complex, and highly error-prone. Therefore, formal
verification with machine support is desirable.
Unfortunately, existing techniques are not sufficient to directly
apply verification tools to automatically prove unlinkability.
In this paper, we overcome this limitation by defining a simple
transformation that will exploit some specific features of Proverif. 
This transformation, together with some generic
axioms, allows the tool to successfully
conclude on several case studies. We have implemented our approach,
effectively obtaining direct proofs of unlinkability on several 
protocols that were, until now,
out of reach of automatic verification tools.
},
  address =       {Dubrovnik, Croatia},
  author =        {Baelde, David and Debant, Alexandre and Delaune, St{\'e}phanie},
  booktitle =     {{P}roceedings of the 36th {IEEE} {C}omputer
                   {S}ecurity {F}oundations {S}ymposium ({CSF}'23)},
  month =         jul,
  OPTpages =         {169--183},
  publisher =     {{IEEE} Computer Society Press},
  title =         {Proving Unlinkability using {P}roverif through Desynchronised Bi-Processes},
  year =          {2023},
  acronym =       {{CSF}'23},
  nmonth =        {7},
  lsv-category =  {intc},
  wwwpublic =     {public and ccsb},
}