基于SPIN的SAS协议和NS公钥协议分析

Study on Analysis of SAS Protocol and NS Protocol Based on SPIN

给出SP IN模型检测协议的验证步骤,使用其分析验证SA S协议的安全属性和数据流行为属性,以及N S公钥协议的机密性和认证性。结果成功发现SA S协议数据流的缺陷和N S公钥协议的攻击路径。

Protocol verification procedures based on model checking technique using SPIN were provided,then these procedures were used to analyze and verify the salty and function property in the SAS protocol, and the security and authentication property in the NS protocol. The results show that the flaw in the data flow of SAS protocol and the attacking path of NS protocol are detected.