基于TLA的NS安全协议分析及检测
【出 处】:《
计算机工程与科学
》
CSCD
2010年第32卷第7期 38-41页,共4页
【作 者】:
黄贻望
[1,2] ;
万良
[1] ;
李祥
[1]
【摘 要】
行为时序逻辑是一种组合了时序逻辑与行为逻辑来对并发系统进行描述与验证的逻辑,在描述并发转移系统中,行为时序逻辑通过引入行动和行为的概念,使得系统和属性可用同一种行为时序逻辑来表示。本文首先介绍行为时序逻辑的语法、语义及简单推理规则;然后以典型的NS公开密钥协议为例,对其进行形式化分析,建立了入侵者参加的简化模型。通过对模型进行FSM建模,转化为TLA+描述的规约系统,然后对其进行TLC检测,发现其存在中间人的重放攻击。
相关热词搜索:
上一篇:基于AES的ZigBee标准安全机制分析
下一篇:应用层异常检测模型