A Logical Verification Method for Security Protocols Based on Linear Logic and BAN Logic
A Logical Verification Method for Security Protocols Based on Linear Logic and BAN Logic
复制标题
一种基于线性逻辑和BAN逻辑的安全协议逻辑验证方法
DOI：
10.1007/3-540-36532-x_24
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
M. Okada
中科院分区：
文献类型：
--
作者：
Koji Hasebe;M. Okada
遵循安全协议的进程由形式证明（基于多集重写模型的线性逻辑片段）表示，cervesatto - durgin - lincoln - mitchell - Scedrov[2]修改了该思想，而（修改的）BAN逻辑（首先由Burrows-Abadi-Needham[2]引入）被用作进程安全属性的评估语义。通过这种方法，我们可以摆脱BAN框架验证过程中所谓的“理想化”步骤。特别地，我们将ban风格的信念推理分为两类；一种推理只需要参与者观察到的过程的一些语法结构，另一种推理需要参与者对协议结构的了解和一定的诚实假设。我们称后者为诚实推论。我们将展示如何在安全性验证的评估语义中使用这种诚实推断。我们还指出，对随机数/键/消息的新鲜度的评估推断被归类为第一类，但由于缺乏特定的具体时间约束设置，其中一些推断缺乏如何评估的信息。我们在工艺/协议描述中引入了自然的时间约束设置，丰富了新鲜度评价的表现力。
A process following a security protocol is represented by a formal proof (of a fragment of linear logic based on the multiset rewriting model), modifying the idea by Cervesato-Durgin-Lincoln-Mitchell- Scedrov [4], while the (modified) BAN logic (which was first introduced by Burrows-Abadi-Needham [2]) is used as an evaluation semantics on security-properties for processes. By this method, we can get rid of the so called “idealization” step in the verification procedure of the BAN framework. In particular, we classify BAN-style belief-inferences into two categories; the inferences which only require some syntactic structure of a process observed by a participant on one hand, and the inferences which require a participant’s knowledge on the structure of a protocol and a certain honesty assumption.We call the latter the honesty inferences.We shall show how such honesty inferences are used in the evaluation semantics for the security verification. We also point out that the evaluation inferences on freshness of nonces/keys/messages are classified as in the first category but that some of such inferences lack the information how to evaluate due to the lack of a certain concrete time-constraint setting. We introduce a natural time-constraint setting in our process/protocol descriptions and enrich the expressive power of the freshness evaluation.