电子学报
電子學報
전자학보
ACTA ELECTRONICA SINICA
2007年
8期
1516-1520
,共5页
协议分析%动态逻辑%类BAN逻辑
協議分析%動態邏輯%類BAN邏輯
협의분석%동태라집%류BAN라집
本文提出了一种新的逻辑方法分析安全协议的安全性.该方法给出了一种安全协议的动态分析模型,从而克服了类BAN逻辑"理想化协议"步骤的缺陷,提出了消息唯一起源的概念和判定规则,严格区分"可靠信任"和"不可靠信任",解决了"相信事情的发生"和"相信事情的真实性"两种不同信任的区别,并在此基础上建立了动态逻辑方法.通过实例分析,该方法可以发现类BAN逻辑不能发现的协议漏洞,从而证明了方法的有效性.
本文提齣瞭一種新的邏輯方法分析安全協議的安全性.該方法給齣瞭一種安全協議的動態分析模型,從而剋服瞭類BAN邏輯"理想化協議"步驟的缺陷,提齣瞭消息唯一起源的概唸和判定規則,嚴格區分"可靠信任"和"不可靠信任",解決瞭"相信事情的髮生"和"相信事情的真實性"兩種不同信任的區彆,併在此基礎上建立瞭動態邏輯方法.通過實例分析,該方法可以髮現類BAN邏輯不能髮現的協議漏洞,從而證明瞭方法的有效性.
본문제출료일충신적라집방법분석안전협의적안전성.해방법급출료일충안전협의적동태분석모형,종이극복료류BAN라집"이상화협의"보취적결함,제출료소식유일기원적개념화판정규칙,엄격구분"가고신임"화"불가고신임",해결료"상신사정적발생"화"상신사정적진실성"량충불동신임적구별,병재차기출상건립료동태라집방법.통과실례분석,해방법가이발현류BAN라집불능발현적협의루동,종이증명료방법적유효성.
