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 $\pi$-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.
翻译:本文展示了我们怎样才能利用一个非同步过渡系统,其过渡标志是事件,并配有事件独立性的概念,来界定应用的$\pion$-calcululus的非交叉语义。我们定义的最重要的概念是:启动-终止或ST-相似性,保持事件持续时间;历史-保存或HP-两样性,保持因果关系。我们指出,相应的相似性前令暴露出这些语义之间的明显区别。我们特别提请注意HP失败相似性的区别力量,并讨论它如何影响我们用来核查安全和隐私特性的攻击性威胁模式。我们还比较了现有的位于不同位置的概念与我们引入的定义。