分析和设计安全协议的新逻辑的语义

A Semantics for a New Logic of Analysis and Design Security Protocol

文献[1]中提出了一种分析和设计安全协议的新逻辑.协议分析者可以用该逻辑来对安全协议进行分析,而协议设计者可以使用该逻辑用一种系统的方法来构造安全协议.文献[1]没有给出该逻辑的形式化语义,因为串空间模型具有良好的语义,现将新逻辑和串空间模型结合起来,给出新逻辑的串空间语义,并运用该语义证明了新逻辑的推理规则是正确的.

We presented a new logic of analysis and design security protocol in paper [ 1 ]. Protocol analyser can analyse security protocol by the logic, and protocol designer can construct security protocol by the logic in a systematic way. In paper [ 1 ], we didn＇t present the formal semantics for the logic. In this paper, we give the strand space semantics for the logic by combining the logic with strand space model, then prove that inference rules of the logic are correct by strand space semantics.