Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Proving Unlinkability using ProVerif through Desynchronized Bi-Processes

David Baelde 1 Alexandre Debant 2 Stéphanie Delaune 1 
1 SPICY - Security & PrIvaCY
IRISA-D1 - SYSTÈMES LARGE ÉCHELLE
2 PESTO - Proof techniques for security protocols
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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 several features recently introduced in the tool ProVerif. This transformation, together with some generic axioms, allow 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. Moreover, our approach is not specific to unlinkability and could, in principle, be useful in other contexts.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

https://hal.inria.fr/hal-03674979
Contributor : Alexandre Debant Connect in order to contact the contributor
Submitted on : Wednesday, May 25, 2022 - 11:43:37 AM
Last modification on : Wednesday, May 25, 2022 - 3:29:40 PM

Identifiers

  • HAL Id : hal-03674979, version 1

Citation

David Baelde, Alexandre Debant, Stéphanie Delaune. Proving Unlinkability using ProVerif through Desynchronized Bi-Processes. 2022. ⟨hal-03674979⟩

Share

Metrics

Record views

0

Files downloads

0