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 \(π\)-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.

翻译：随着关键基础设施日益依赖于安全协议满足多种需求的假设，采用更优攻击检测方法验证隐私属性（如不可链接性）的重要性不言而喻。本文通过等价于攻击者无法区分行为的关系，深入审视"不可链接性"这一隐私属性。基于某些合理设计选择可能导致形式化方法遗漏攻击的观察，我们关注一种能够解释历史事件间关联的经典并发语义，并证明存在能够发现我们所考虑全部协议攻击的并发感知语义。具体而言，我们聚焦于迹等价已知会遗漏分支时间等价可观测攻击的协议。通过考察三个维度的影响：程序员定义不可链接性问题时的设计决策（风格）、遵循执行过程中选择行为的语义（分支时间）、以及对并发敏感的语义（非交错），我们发现除非赋予攻击者足够能力以观测选择与并发行为，否则合理的设计风格仍会遗漏攻击。我们的核心贡献在于阐明：当为应用非交错π演算定义时，一种流行的并发语义——历史保持双模拟——能够发现所考虑全部协议的攻击，且不受风格选择影响。此外，我们可通过一种新颖的模态逻辑描述所有此类攻击，该逻辑因此适用于对隐私属性攻击进行形式化验证。