Unlinkability and History Preserving Bisimilarity

Computer Science > Cryptography and Security [Submitted on 14 Mar 2026] Unlinkability and History Preserving Bisimilarity Clément Aubert, Ross Horne, Christian Johansen, Sjouke Mauw 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 this http URL 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. Subjects: Cryptography and Security (cs.CR) Cite as: arXiv:2603.13735 [cs.CR]   (or arXiv:2603.13735v1 [cs.CR] for this version)   https://doi.org/10.48550/arXiv.2603.13735 Focus to learn more Journal reference: Computers & Security, Volume 165, 2026, 104819, ISSN 0167-4048 Related DOI: https://doi.org/10.1016/j.cose.2025.104819 Focus to learn more Submission history From: Clément Aubert [view email] [v1] Sat, 14 Mar 2026 03:41:38 UTC (766 KB) Access Paper: view license Current browse context: cs.CR < prev   |   next > new | recent | 2026-03 Change to browse by: cs References & Citations NASA ADS Google Scholar Semantic Scholar Export BibTeX Citation Bookmark Bibliographic Tools Bibliographic and Citation Tools Bibliographic Explorer Toggle Bibliographic Explorer (What is the Explorer?) Connected Papers Toggle Connected Papers (What is Connected Papers?) Litmaps Toggle Litmaps (What is Litmaps?) scite.ai Toggle scite Smart Citations (What are Smart Citations?) Code, Data, Media Demos Related Papers About arXivLabs Which authors of this paper are endorsers? | Disable MathJax (What is MathJax?)