计算机工程与应用
計算機工程與應用
계산궤공정여응용
COMPUTER ENGINEERING AND APPLICATIONS
2005年
30期
122-124
,共3页
身份鉴别协议%形式化分析
身份鑒彆協議%形式化分析
신빈감별협의%형식화분석
分别使用形式化分析工具Casper+FDR和OFMC模型检测器对文[1]提出的一个军网身份鉴别协议进行了分析,找到了一个相同的攻击实例.同时指出了文[1]和文[2]中存在的几个谬误.然后对协议进行了修正.形式化验证结果表明修正后的协议是安全的.
分彆使用形式化分析工具Casper+FDR和OFMC模型檢測器對文[1]提齣的一箇軍網身份鑒彆協議進行瞭分析,找到瞭一箇相同的攻擊實例.同時指齣瞭文[1]和文[2]中存在的幾箇謬誤.然後對協議進行瞭脩正.形式化驗證結果錶明脩正後的協議是安全的.
분별사용형식화분석공구Casper+FDR화OFMC모형검측기대문[1]제출적일개군망신빈감별협의진행료분석,조도료일개상동적공격실례.동시지출료문[1]화문[2]중존재적궤개류오.연후대협의진행료수정.형식화험증결과표명수정후적협의시안전적.
