SVP PEPR Cybersécurité

PEPR Cybersecurity Security Verification Protocol

Proving Unlinkability using ProVerif through Desynchronized Bi-Processes

David Baelde, Alexandre Debant, and Stéphanie Delaune
Unlinkability is a privacy property of crucial im- portance 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. 

Paper to be published at the CSF 2023.

Laisser un commentaire

Votre adresse e-mail ne sera pas publiée. Les champs obligatoires sont indiqués avec *