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

关键词: 逻辑语义；认证协议设计；串空间

Abstract: 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.

Key words: Logic semantics; Authentication protocol design; Strand space