YAPA: 一种计算攻击者知识的通用工具
计算机科学中的逻辑
2010-05-06 v1 密码学与安全
摘要
在许多安全协议的形式化分析中，推理攻击者的知识是必要的一步。在应用π演算的框架中，如同在基于等式逻辑的类似语言中一样，知识通常通过两种关系来表达：可推导性和静态等价性。针对各种等式理论，已经提出了若干种针对这些关系的决策过程。然而，每种理论都有其特定的算法，并且迄今为止尚未有实现。我们提供了一种通用的可推导性和静态等价性过程，该过程以任何收敛重写系统作为输入。我们表明，我们的算法涵盖了大多数现有的针对收敛理论的决策过程。我们还提供了一种高效的实现，并将其与ProVerif和KiSs工具进行了简要比较。
引用
@article{arxiv.1005.0737,
title = {YAPA: A generic tool for computing intruder knowledge},
author = {Mathieu Baudet and Véronique Cortier and Stéphanie Delaune},
journal= {arXiv preprint arXiv:1005.0737},
year = {2010}
}