微计算机信息
微計算機信息
미계산궤신식
CONTROL & AUTOMATION
2009年
12期
98-100
,共3页
安全协议%串空间%Athena算法%模型检测
安全協議%串空間%Athena算法%模型檢測
안전협의%천공간%Athena산법%모형검측
研究分析了Athena自动协议形式化分析算法的原理.该算法能够分析协议的各种安全属性,它基于扩展了的串空间模型,利用了消息间的因果关系,并且结合了定理证明和模型检测方法,能有效地分析安全协议的各种安全属性.在此基础上,完整地分析了ISO/IEC DIS 11770-3中提出的Helsinki协议的认证属性,分析得出该协议是有安全缺陷的.
研究分析瞭Athena自動協議形式化分析算法的原理.該算法能夠分析協議的各種安全屬性,它基于擴展瞭的串空間模型,利用瞭消息間的因果關繫,併且結閤瞭定理證明和模型檢測方法,能有效地分析安全協議的各種安全屬性.在此基礎上,完整地分析瞭ISO/IEC DIS 11770-3中提齣的Helsinki協議的認證屬性,分析得齣該協議是有安全缺陷的.
연구분석료Athena자동협의형식화분석산법적원리.해산법능구분석협의적각충안전속성,타기우확전료적천공간모형,이용료소식간적인과관계,병차결합료정리증명화모형검측방법,능유효지분석안전협의적각충안전속성.재차기출상,완정지분석료ISO/IEC DIS 11770-3중제출적Helsinki협의적인증속성,분석득출해협의시유안전결함적.
