基于TLA的NS安全协议分析及检测

行为时序逻辑是一种组合了时序逻辑与行为逻辑来对并发系统进行描述与验证的逻辑,在描述并发转移系统中,行为时序逻辑通过引入行动和行为的概念,使得系统和属性可用同一种行为时序逻辑来表示。本文首先介绍行为时序逻辑的语法、语义及简单推理规则;然后以典型的NS公开密钥协议为例,对其进行形式化分析,建立了入侵者参加的简化模型。通过对模型进行FSM建模,转化为TLA+描述的规约系统,然后对其进行TLC检测,发现其存在中间人的重放攻击。

Analysis and Checking of the NS Security Protocol Based on the Temporal Logic of Action

TLA is a logic which combines the temporal logic and the logic of action,describing and validating the concurrent systems with TLA. TLA can express the system and the corresponding properties by adding actions and behaviors.First,this paper introduces the grammer,semantics and simple reasoning rules, and then formally analyzes the NS protocol, and sets up the FSM model, and specifies the model with TLA+, and then checks the corresponding properties with the tool of TLC. The results of checking shows there exists middle man’s replay attack.