论文标题
尊重非交流的持续时间和因果关系的$π$ -calculus
Bisimulations Respecting Duration and Causality for the Non-interleaving Applied $π$-Calculus
论文作者
论文摘要
本文展示了我们如何利用异步过渡系统，其过渡标记为事件并配备了事件的独立性，以定义用于应用的$π$ -Calculus的非交流语义。我们定义的最重要的概念是：起始终止或st-bisibrility，保留事件的持续时间；以及保存历史或双性恋，保留因果关系。我们指出的是，相应的相似性预订在这些语义之间明确区分。我们特别注意HP失败相似性的区别能力，并讨论它如何影响我们验证安全性和隐私属性的攻击者威胁模型。我们还将现有的二合一性概念与我们介绍的定义进行了比较。
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.
