形式化分析验证一种改进的NSSK协议

Formal Analysis and Verification of an Improved NSSK Protocol

认证协议是保证网络安全的基础,NSSK协议是最早最经典的一种认证密码协议.本文分析了NSSK协议的安全特性,提出了一种改进的NSSK协议,并利用形式化建模语言CSP和模型检测工具FDR分别对其建模和验证.实验结果表明改进的NSSK协议可以满足期望的安全目标,达到保障网络安全的目的.

Authentication protocols are the basis of network security. Needham-Schroeder Shared-Key （NS- SK） protocol is considered as one of the earliest and classical authentication protocol. This paper introduces NSSK protocol, analyzes its security, and proposes an improved NSSK protocol. It is also modeled and verified by the framework of CSP and its model-checking tool FDR. The analysis results show that the proposed protocol can achieve the expectative authentication goals and the purpose of ensuring network securi- ty.