一种安全协议分析算法研究  

Research on An Algorithm for Analyzing Security Protocol

作　　者：陈建熊[1] 孙乐昌[1] 揭摄[1] 

机构地区：[1]合肥电子工程学院网络工程系,合肥230037

出　　处：《微计算机信息》2009年第12期98-100,共3页Control & Automation

摘　　要：研究分析了Athena自动协议形式化分析算法的原理。该算法能够分析协议的各种安全属性,它基于扩展了的串空间模型,利用了消息间的因果关系,并且结合了定理证明和模型检测方法,能有效地分析安全协议的各种安全属性。在此基础上,完整地分析了ISO/IEC DIS11770-3中提出的Helsinki协议的认证属性,分析得出该协议是有安全缺陷的。To do some research about an automatic algorithm theory for analyzing security protocols. This algorithm can analyse verious security properties of security protocol. It bases on the theory of strand space which captures exact causal relation information and combines theory proving and model checking. So it is efficient to analyse properties of security protocols. Base on this theory, we analyse the authentication propertie of the Helsinki protocol which is brought forward in ISO/IEC DIS 11770-3 and we can conclude that this protocol can be flawed .

关 键 词：安全协议 串空间 Athena算法 模型检测 

分 类 号：TP309.2[自动化与计算机技术—计算机系统结构]