Abstract: This paper describes a graphic verification tool for security protocol based on GSPM with formal methods. Linear Temporal Logic(LTL) is introduced to show the property of security protocol. This tool can find out the bug of security protocol using the model-checking method based on searching states. The simplified needham-schroeder public-key authentication protocol is used to exemplify the automatic verification process of security protocol with this tool, and results show the validity and correctness of the verification algorithm.

Key words: Linear Temporal Logic(LTL), security protocol, confidentiality, authentication

摘要： 介绍一个基于GSPM的安全协议验证的图形化工具。验证工具以GSPM模型为基础形式化地描述了安全协议，并引进线性时序逻辑刻画了安全协议的性质，用基于状态搜索的模型检测方法在安全协议的验证过程中找出漏洞。以简化的NSPK协议为例，描述了该工具如何验证安全协议，表明GSPM模型和验证算法的有效性和正确性。

关键词: 线性时序逻辑, 安全协议, 保密性, 认证性

CLC Number: 

• TP309