有状态应用π演算的计算可靠性结果

近年来，许多研究致力于建立有状态协议的符号模型。其中，SAPIC工具和StatVerif工具提供了高级规范语言和自动化分析。它们的语言，即有状态应用\pi-演算，通过定义显式状态构造从应用\pi-演算扩展而来。其中使用的密码学符号抽象使得分析易于自动化。然而，这可能忽略基于密码算法代数性质的攻击。在本文中，我们建立了SAPIC工具和StatVerif工具中所用有状态应用\pi-演算的计算可靠性结果。在我们的方法中，我们基于CoSP框架构建结果。对于SAPIC，我们将非单调协议状态嵌入到CoSP协议中，并证明所得CoSP协议是高效的。通过该嵌入，我们提供了SAPIC的计算可靠性结果（由定理1）。对于StatVerif，我们将StatVerif进程编码为SAPIC进程的一个子集，并获得了StatVerif的计算可靠性结果（由定理2）。我们的编码显示了两种语言语义之间的差异。我们的工作继承了CoSP的模块化，允许轻松扩展证明到特定密码学原语。因此我们为使用公钥加密和签名的SAPIC和StatVerif输入语言建立了计算可靠自动化验证结果（由定理3）。