电子学报
電子學報
전자학보
ACTA ELECTRONICA SINICA
2002年
z1期
2099-2101
,共3页
邵晨曦%胡香冬%熊焰%蒋凡
邵晨晞%鬍香鼕%熊燄%蔣凡
소신희%호향동%웅염%장범
模型检测%BAN-Yahalom协议%SPIN
模型檢測%BAN-Yahalom協議%SPIN
모형검측%BAN-Yahalom협의%SPIN
为了将模型检测这种强有力的系统验证技术应用于网络协议的安全分析,形式化建模仍然是目前的关键问题和难点所在.本文提出了一种基于高级过程描述语言的建模方法.根据入侵者角色和攻击目标的不同,从入侵者的角度分析协议的运行模式,为每个主体建立过程模型,用模型检测工具进行分析验证.对BAN-Yahalom协议的SPIN分析验证了这种方法的可行性.该方法具有一定的通用性,对其它网络协议的分析有很好的参考价值.
為瞭將模型檢測這種彊有力的繫統驗證技術應用于網絡協議的安全分析,形式化建模仍然是目前的關鍵問題和難點所在.本文提齣瞭一種基于高級過程描述語言的建模方法.根據入侵者角色和攻擊目標的不同,從入侵者的角度分析協議的運行模式,為每箇主體建立過程模型,用模型檢測工具進行分析驗證.對BAN-Yahalom協議的SPIN分析驗證瞭這種方法的可行性.該方法具有一定的通用性,對其它網絡協議的分析有很好的參攷價值.
위료장모형검측저충강유력적계통험증기술응용우망락협의적안전분석,형식화건모잉연시목전적관건문제화난점소재.본문제출료일충기우고급과정묘술어언적건모방법.근거입침자각색화공격목표적불동,종입침자적각도분석협의적운행모식,위매개주체건립과정모형,용모형검측공구진행분석험증.대BAN-Yahalom협의적SPIN분석험증료저충방법적가행성.해방법구유일정적통용성,대기타망락협의적분석유흔호적삼고개치.
