Unlinkability and History Preserving Bisimilarity

TL;DR

This paper investigates the unlinkability privacy property in security protocols, demonstrating that history-preserving bisimilarity semantics can detect attacks missed by traditional methods, and introduces a modal logic for attack certification.

Contribution

It introduces the use of history-preserving bisimilarity in the applied alculus to detect privacy attacks and develops a modal logic for formal attack certification.

Findings

History-preserving bisimilarity detects attacks missed by trace equivalence.

Concurrency-aware semantics reveal vulnerabilities in protocols.

A novel modal logic enables formal certification of privacy attacks.

Abstract

An ever-increasing number of critical infrastructures rely heavily on the assumption that security protocols satisfy a wealth of requirements. Hence, the importance of certifying e.g., privacy properties using methods that are better at detecting attacks can hardly be overstated. This paper scrutinises the "unlinkability" privacy property using relations equating behaviours that cannot be distinguished by attackers. Starting from the observation that some reasonable design choice can lead to formalisms missing attacks, we draw attention to a classical concurrent semantics accounting for relationship between past events, and show that there are concurrency-aware semantics that can discover attacks on all protocols we consider.More precisely, we focus on protocols where trace equivalence is known to miss attacks that are observable using branching-time equivalences. We consider the impact of three dimensions: design decisions made by the programmer specifying an unlinkability problem (style), semantics respecting choices during execution (branching-time), and semantics sensitive to concurrency (non-interleaving), and discover that reasonable styles miss attacks unless we give attackers enough power to observe choices and concurrency. Our main contribution is to draw attention to how a popular concurrent semantics -- history-preserving bisimilarity -- when defined for the non-interleaving applied \(\pi\)-calculus, can discover attacks on all protocols we consider, regardless of the choice of style. Furthermore, we can describe all such attacks using a novel modal logic that is hence suitable to formally certify attacks on privacy properties.