入侵者理论的证明论分析

我们考虑安全协议分析中的入侵者推导问题：即在盲签名理论以及某些二元算子的结合性和交换性 (AC) 下的任意收敛等式理论中，判定给定消息 M 是否能从一组消息 Gamma 中推导出来。入侵者推导的传统表述通常给出在类似自然演绎的系统中，证明可判定性需要花费大量精力来表明规则在某种意义上是“局部的”。通过利用自然演绎与相继式演算之间众所周知的转换，我们将入侵者推导问题重新表述为相继式演算中的证明搜索，其中局部性是直接的。使用标准的证明论方法（如规则的可置换性和切消去），我们证明了入侵者推导问题可以在多项式时间内归约为基本推导问题，后者相当于在底层各个等式理论中求解特定方程。我们证明了该结果可扩展到不相交 AC 收敛理论的组合，从而在组合理论下的入侵者推导可判定性归约为每个组成理论中基本推导的可判定性。为了进一步证明基于相继式方法的实用性，我们表明，对于 Dolev-Yao 入侵者，我们的基于相继式的技术可用于解决更困难的可推导性约束求解问题，其中要推导的相继式可能包含代表入侵者可能产生的可能消息的间隙（或变量）。