TY - JOUR
T1 - Bisimulations Respecting Duration and Causality for the Non-interleaving Applied ≠-Calculus
AU - Aubert, Clément
AU - Horne, Ross
AU - Johansen, Christian
N1 - Funding Information:
The definitions in this paper are introduced to support an invited talk by the second author at EXPRESS/SOS on proving privacy properties using bisimilarity. We thank the organisers Valentina Castiglioni and Claudio Antares Mezzina for this invitation.
Publisher Copyright:
© C. Aubert, R. Horne and C. Johansen.
PY - 2022/9/6
Y1 - 2022/9/6
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85138686900&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85138686900&partnerID=8YFLogxK
U2 - 10.4204/EPTCS.368.1
DO - 10.4204/EPTCS.368.1
M3 - Conference article
AN - SCOPUS:85138686900
SN - 2075-2180
VL - 368
SP - 3
EP - 22
JO - Electronic Proceedings in Theoretical Computer Science, EPTCS
JF - Electronic Proceedings in Theoretical Computer Science, EPTCS
T2 - Combined 29th International Workshop on Expressiveness in Concurrency and 19th Workshop on Structural Operational Semantics, EXPRESS/SOS 2022
Y2 - 12 September 2022
ER -