基于迹的Spi演算互模拟
A Trace Based Bisimulation for the Spi Calculus
摘要：
一个开放互模拟的概念制定的spi演算，一个扩展的pi演算与密码原语。在这个公式中，开放互模拟是由成对的符号迹索引的，符号迹表示环境与被检查的过程对之间的相互作用的历史。符号迹的使用允许在互模拟检查中对约束输入进行符号处理，这避免了对输入值的量化。证明了开放双相似性在等价性检验方面是合理的，并进一步证明了开放双相似性是过程上的等价关系和有限过程上的同余关系。据我们所知，这是第一个制定的开放互模拟的spi演算的全等结果得到证明。
英文摘要：
A notion of open bisimulation is formulated for the spi calculus, an extension of the pi-calculus with cryptographic primitives. In this formulation, open bisimulation is indexed by pairs of symbolic traces, which represent the history of interactions between the environment with the pairs of processes being checked for bisimilarity. The use of symbolic traces allows for a symbolic treatment of bound input in bisimulation checking which avoids quantification over input values. Open bisimilarity is shown to be sound with respect to testing equivalence, and futher, it is shown to be an equivalence relation on processes and a congruence relation on finite processes. As far as we know, this is the first formulation of open bisimulation for the spi calculus for which the congruence result is proved.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
