计算机工程
計算機工程
계산궤공정
COMPUTER ENGINEERING
2006年
5期
164-166,246
,共4页
陈大伟%董荣胜%郭云川%古天龙
陳大偉%董榮勝%郭雲川%古天龍
진대위%동영성%곽운천%고천룡
IKE协议%模型检测%SPIN%Promela
IKE協議%模型檢測%SPIN%Promela
IKE협의%모형검측%SPIN%Promela
基于模型检测技术,使用SPIN对IKEv2协议进行了建模和分析.应用Promela语言描述了协议模型,并用LTL规约了该协议需要满足的认证性和秘密性,最后对检测结果进行了分析.
基于模型檢測技術,使用SPIN對IKEv2協議進行瞭建模和分析.應用Promela語言描述瞭協議模型,併用LTL規約瞭該協議需要滿足的認證性和祕密性,最後對檢測結果進行瞭分析.
기우모형검측기술,사용SPIN대IKEv2협의진행료건모화분석.응용Promela어언묘술료협의모형,병용LTL규약료해협의수요만족적인증성화비밀성,최후대검측결과진행료분석.
