| 基于GSPM的安全协议检验工具 |
| |
| 引用本文： | 庄庆,蔡小娟,董笑菊,戚正伟.基于GSPM的安全协议检验工具[J].计算机工程,2008,34(17):130-132. |
| |
| 作者姓名： | 庄庆 蔡小娟 董笑菊 戚正伟 |
| |
| 作者单位： | 上海交通大学计算机科学与工程系,上海,200240 |
| |
| 基金项目： | 国家重点基础研究发展计划(973计划)，国家自然科学基金，教育部高等学校博士学科点专项科研基金 |
| |
| 摘 要： | 介绍一个基于GSPM的安全协议验证的图形化工具。验证工具以GSPM模型为基础形式化地描述了安全协议，并引进线性时序逻辑刻画了安全协议的性质，用基于状态搜索的模型检测方法在安全协议的验证过程中找出漏洞。以简化的NSPK协议为例，描述了该工具如何验证安全协议，表明GSPM模型和验证算法的有效性和正确性。
|
| 关 键 词： | 线性时序逻辑 安全协议 保密性 认证性 |
| 修稿时间： | |
Verification Tool for Security Protocol Based on GSPM |
| |
| ZHUANG Qing,CAI Xiao-juan,DONG Xiao-ju,QI Zheng-wei.Verification Tool for Security Protocol Based on GSPM[J].Computer Engineering,2008,34(17):130-132. |
| |
| Authors: | ZHUANG Qing CAI Xiao-juan DONG Xiao-ju QI Zheng-wei |
| |
| Affiliation: | (Dept. of Computer Science and Engineering, Shanghai Jiaotong University, Shanghai 200240) |
| |
| 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. |
| |
| Keywords: | Linear Temporal Logic(LTL) security protocol confidentiality authentication |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程》浏览原始摘要信息 |
|
点击此处可从《计算机工程》下载全文 |
