基于GSPM的安全协议检验工具  

Verification Tool for Security Protocol Based on GSPM

作　　者：庄庆[1] 蔡小娟[1] 董笑菊[1] 戚正伟[1] 

机构地区：[1]上海交通大学计算机科学与工程系,上海200240

出　　处：《计算机工程》2008年第17期130-132,共3页Computer Engineering

基　　金：国家"973"计划基金资助项目(2003CB317005);国家自然科学基金资助项目(60473006;60573002);博士点基金资助项目(20010248033)

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

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

分 类 号：TP309[自动化与计算机技术—计算机系统结构]