计算机应用与软件
計算機應用與軟件
계산궤응용여연건
COMPUTER APPLICATIONS AND SOFTWARE
2013年
1期
315-318
,共4页
形式化分析%CPN%时间因素%安全协议
形式化分析%CPN%時間因素%安全協議
형식화분석%CPN%시간인소%안전협의
提出一种针对包含时间因素的安全协议的有色Petri (CPN)形式化分析方法,利用CPN Tools中的内置全局自动时钟标记,时间相关性质可通过仿真和生成状态图进行分析验证.基于这一方法,对著名的NS协议(简化版)建模,来分析验证与时间相关的安全属性.然后利用CPN Tools,采用CPN ML语言编写查询函数验证协议的AUT性质,从而发现协议的漏洞.应用分析结果表明方法有效,且操作简单容易理解.
提齣一種針對包含時間因素的安全協議的有色Petri (CPN)形式化分析方法,利用CPN Tools中的內置全跼自動時鐘標記,時間相關性質可通過倣真和生成狀態圖進行分析驗證.基于這一方法,對著名的NS協議(簡化版)建模,來分析驗證與時間相關的安全屬性.然後利用CPN Tools,採用CPN ML語言編寫查詢函數驗證協議的AUT性質,從而髮現協議的漏洞.應用分析結果錶明方法有效,且操作簡單容易理解.
제출일충침대포함시간인소적안전협의적유색Petri (CPN)형식화분석방법,이용CPN Tools중적내치전국자동시종표기,시간상관성질가통과방진화생성상태도진행분석험증.기우저일방법,대저명적NS협의(간화판)건모,래분석험증여시간상관적안전속성.연후이용CPN Tools,채용CPN ML어언편사사순함수험증협의적AUT성질,종이발현협의적루동.응용분석결과표명방법유효,차조작간단용역리해.
