子句

安全协议验证者proverif及其喇叭子句分辨率算法

安全协议的验证是自1990年代以来非常活跃的研究领域。安全协议无处不在：Internet（特别是用于https：// connections使用的TLS协议），WiFi，移动电话，信用卡，。。。。众所周知，他们的设计容易出错，并且未通过测试检测到错误：仅当对手试图攻击协议时，它们才会出现。因此，正式验证它们很重要。为了使安全协议形式化，需要为其数学模型。通常会考虑一个活跃的对手，可以收听网络上发送的消息，计算自己的媒介，然后将它们发送到网络上，就好像它们来自诚实的参与者一样。为了促进协议的自动验证，大多数协议验证者都考虑了加密的符号模型，也称为“ dolev-yao模型” [18，15]。在此模型中，加密原语（例如加密）被视为理想的黑盒，以功能符号为代表。消息是通过这些原始词的术语建模的；并且对手仅限于应用定义的原语。这也称为完美的加密假设：对手解密消息的唯一途径是将解密函数与正确的密钥一起使用。在这样的模型中，协议验证的主要任务之一是计算对手的知识，即对对手可以获得的一组术语。这仍然是并非繁琐的，因为该集合通常是无限的，但是它比有关斑点和概率的推理要简单得多。两个最广泛使用的符号协议验证者可能是proverif [11]和tamarin [17]。有关协议验证领域的更多详细信息，我们将读者转移到调查[10，6]。在本文中，我们专注于协议验证者proverif，可以从https://proverif.inria.fr下载。我们在下一节中介绍了王朝的概述，并关注其喇叭条款分辨率算法。