Bisimulations respecting duration and causality for the non-interleaving applied pi-calculus

Aubert, Clément and Horne, Ross and Johansen, Christian; Castiglioni, Valentina and Mezzina, Claudio A., eds. (2022) Bisimulations respecting duration and causality for the non-interleaving applied pi-calculus. In: Proceedings Combined 29th International Workshop on Expressiveness in Concurrency and 19th Workshop on Structural Operational Semantics. Electronic Proceedings in Theoretical Computer Science . Open Publishing Association, POL, pp. 3-22. (https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?EXPSO...)

[thumbnail of Aubert-etal-EPTCS-2022-Bisimulations-respecting-duration-and-causality-for-the-non-interleaving-applied-pi-calculus]
Preview
 Text. Filename: Aubert-etal-EPTCS-2022-Bisimulations-respecting-duration-and-causality-for-the-non-interleaving-applied-pi-calculus.pdf
Final Published Version
License: Creative Commons Attribution 4.0 logo
Download (262kB)| Preview

Abstract

This paper shows how we can make use of an asynchronous transition system, whose transitions are labelled with events and which is equipped with a notion of independence of events, to define non-interleaving semantics for the applied π-calculus. The most important notions we define are: Start-Termination or ST-bisimilarity, preserving duration of events; and History-Preserving or HP- bisimilarity, preserving causality. We point out that corresponding similarity preorders expose clearly distinctions between these semantics. We draw particular attention to the distinguishing power of HP failure similarity, and discuss how it affects the attacker threat model against which we verify security and privacy properties. We also compare existing notions of located bisimilarity to the definitions we introduce.

CORE (COnnecting REpositories)