通信学报
通信學報
통신학보
JOURNAL OF CHINA INSTITUTE OF COMMUNICATIONS
2014年
11期
117-125
,共9页
顾纯祥%王焕孝%郑永辉%辛丹%刘楠
顧純祥%王煥孝%鄭永輝%辛丹%劉楠
고순상%왕환효%정영휘%신단%류남
安全协议%形式化分析%布尔可满足性%惰性分析%类型缺陷攻击
安全協議%形式化分析%佈爾可滿足性%惰性分析%類型缺陷攻擊
안전협의%형식화분석%포이가만족성%타성분석%류형결함공격
security protocols%formalization analysis%Boolean satisfiability problem%lazy analyze%type flaw attack
提出了一种基于布尔可满足性问题的安全协议形式化分析方法SAT-LMC,通过引入惰性分析的思想优化初始状态与转换规则,提高了安全性的检测效率.另一方面,通过在消息类型上定义偏序关系,SAT-LMC能够检测出更丰富的类型缺陷攻击.基于此方法实现了一个安全协议分析工具,针对Otway-Rees协议检测出了一种类型缺陷攻击;针对OAuth2.0协议,检测结果显示对现实中存在的一些应用场景,存在一种利用授权码截取的中间人攻击.
提齣瞭一種基于佈爾可滿足性問題的安全協議形式化分析方法SAT-LMC,通過引入惰性分析的思想優化初始狀態與轉換規則,提高瞭安全性的檢測效率.另一方麵,通過在消息類型上定義偏序關繫,SAT-LMC能夠檢測齣更豐富的類型缺陷攻擊.基于此方法實現瞭一箇安全協議分析工具,針對Otway-Rees協議檢測齣瞭一種類型缺陷攻擊;針對OAuth2.0協議,檢測結果顯示對現實中存在的一些應用場景,存在一種利用授權碼截取的中間人攻擊.
제출료일충기우포이가만족성문제적안전협의형식화분석방법SAT-LMC,통과인입타성분석적사상우화초시상태여전환규칙,제고료안전성적검측효솔.령일방면,통과재소식류형상정의편서관계,SAT-LMC능구검측출경봉부적류형결함공격.기우차방법실현료일개안전협의분석공구,침대Otway-Rees협의검측출료일충류형결함공격;침대OAuth2.0협의,검측결과현시대현실중존재적일사응용장경,존재일충이용수권마절취적중간인공격.
