Verification Tool for Security Protocol Based on GSPM
QI Zheng-wei · Jisuanji gongcheng · 2008
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.