A Framework for the Analysis of Security Protocols
A Framework for the Analysis of Security Protocols
复制标题
安全协议分析框架
DOI：
--
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
M. Buscemi
中科院分区：
文献类型：
--
作者：
Michele Boreale;M. Buscemi
安全协议的属性（例如身份验证和保密性）通常通过显式生成协议的操作模型然后寻找不安全状态来验证。然而，入侵者和诚实参与者之间的消息交换会引发一种状态爆炸，使模型原则上无限。基于之前关于符号语义的工作，我们提出了一个通用框架，用于自动分析使用各种加密功能的安全协议。我们从类似于 spi 演算的基本语言开始，配备了一组通用密码原语。我们提出了一种依赖于统一并提供有限且有效的协议模型的符号操作语义。接下来给出一种直接对符号模型进行迹分析的方法。在给定加密原语的某些条件下，我们的方法对于所考虑的属性类别被证明是完整的。
Properties of security protocols such as authentication and secrecy are often verified by explictly generating an operational model of the protocol and then seeking for insecure states. However, message exchange between the intruder and the honest participants induces a form of state explosion that makes the model infinite in principle. Building on previous work on symbolic semantics, we propose a general framework for automatic analysis of security protocols that make use of a variety of crypto-functions. We start from a base language akin to the spi-calculus, equipped with a set of generic cryptographic primitives. We propose a symbolic operational semantics that relies on unification and provides finite and effective protocol models. Next, we give a method to carry out trace analysis directly on the symbolic model. Under certain conditions on the given cryptographic primitives, our method is proven complete for the considered class of properties.