YAPA: A Generic Tool for Computing Intruder Knowledge
YAPA: A Generic Tool for Computing Intruder Knowledge
复制标题
YAPA：计算入侵者知识的通用工具
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
S. Delaune
中科院分区：
文献类型：
--
作者：
M. Baudet;V. Cortier;S. Delaune
在许多安全协议的形式化分析中，对攻击者的知识进行推理是一个必要的步骤。在应用π演算的框架中，就像在基于方程逻辑的类似语言中一样，知识通常由两种关系表示：演绎和静态等价。已经提出了几个决策程序，这些关系下的各种方程理论。然而，每种理论都有其特定的算法，迄今为止还没有一种被实现。
我们提供了一个通用的演绎和静态等价的输入任何收敛重写系统的过程。我们表明，我们的算法涵盖了大多数现有的决策程序的收敛理论。我们还提供了一个有效的实现，并简要地比较它与工具ProVerif和KiSs。
Reasoning about the knowledge of an attacker is a necessary step in many formal analyses of security protocols. In the framework of the applied pi-calculus, as in similar languages based on equational logics, knowledge is typically expressed by two relations: deducibility and static equivalence. Several decision procedures have been proposed for these relations under a variety of equational theories. However, each theory has its particular algorithm, and none has been implemented so far.
We provide a generic procedure for deducibility and static equivalence that takes as input any convergent rewrite system. We show that our algorithm covers most of the existing decision procedures for convergent theories. We also provide an efficient implementation and compare it briefly with the tools ProVerif and KiSs.