认证协议设计逻辑的语义

Semantics for a Simple Logic for Authentication Protocol Design

Levente Buttyan等人提出了一种认证协议设计的简单逻辑,协议设计者可以使用该逻辑,用一种系统的方法来构造认证协议。该文把简单逻辑和串空间(Strand Space)模型结合起来,给出了简单逻辑的串空间语义,然后运用该语义证明了简单逻辑的推理规则是正确的。

Levente Buttyan et al put forward a simple logic for authentication protocol design. Protocol designer can construct authentication protocol by the logic in a systematic way. This paper gives the strand space semantics for the logic by combining the logic and strand space,then proves that inference rules of the logic are correct by it.