计算机工程与应用
計算機工程與應用
계산궤공정여응용
COMPUTER ENGINEERING AND APPLICATIONS
2012年
36期
116-120
,共5页
形式化分析%有色Petri网(CPN)%时间戳%安全协议
形式化分析%有色Petri網(CPN)%時間戳%安全協議
형식화분석%유색Petri망(CPN)%시간착%안전협의
提出了一种适用于带有时间戳的安全协议的有色Petri (CPN)形式化分析方法,利用一个非自动时钟来描述协议中涉及的时间因素.对著名的WMF协议建模,利用CPN Tools,采用CPN ML语言编写查询函数验证协议的新鲜性,从而发现协议的漏洞.应用分析结果表明该方法有效,且操作简单容易理解.
提齣瞭一種適用于帶有時間戳的安全協議的有色Petri (CPN)形式化分析方法,利用一箇非自動時鐘來描述協議中涉及的時間因素.對著名的WMF協議建模,利用CPN Tools,採用CPN ML語言編寫查詢函數驗證協議的新鮮性,從而髮現協議的漏洞.應用分析結果錶明該方法有效,且操作簡單容易理解.
제출료일충괄용우대유시간착적안전협의적유색Petri (CPN)형식화분석방법,이용일개비자동시종래묘술협의중섭급적시간인소.대저명적WMF협의건모,이용CPN Tools,채용CPN ML어언편사사순함수험증협의적신선성,종이발현협의적루동.응용분석결과표명해방법유효,차조작간단용역리해.
