入侵者理论的证明论分析

我们考虑安全协议分析中的入侵者推导问题：即在盲签名理论以及某些二元算子满足结合律与交换律 (AC) 的任意收敛等式理论下，判定给定消息 $M$ 是否可从消息集 $\Gamma$ 中推导出来。入侵者推导的传统表述通常采用类似自然演绎的系统，而证明其可判定性需要大量工作以表明规则在某种意义上是“局部”的。通过利用自然演绎与相继式演算之间众所周知的转换，我们将入侵者推导问题重述为相继式演算中的证明搜索，其中局部性是显而易见的。利用规则的置换性和切消等标准证明论方法，我们表明入侵者推导问题可在多项式时间内归约为基本推导问题，这等价于求解底层单个等式理论中的某些方程。我们进一步表明，该结果可推广至不相交 AC-收敛理论的组合，即在组合理论下的入侵者推导的可判定性可归约为各组成理论中基本推导的可判定性。尽管各种研究人员已针对个别情况报告了类似结果，但我们的工作表明，这些结果可以通过基于相继式演算的系统化统一方法论获得。