基于時延Petri網(wǎng)的密碼協(xié)議分析和評估.pdf

1、密碼協(xié)議安全性分析是網(wǎng)絡(luò)安全的一個難題,運用形式化方法對密碼協(xié)議進行分析一直是該領(lǐng)域的研究熱點.形式化分析由于其精煉、簡潔和無二義性逐步成為分析密碼協(xié)議的一條可靠和準確的途徑,但是密碼協(xié)議的形式化分析研究目前還不夠深入,該文主要研究了基于時延Petri網(wǎng)的密碼協(xié)議分析和評估方法.作者所取得的主要研究結(jié)果如下:(1)對四類常見的密碼協(xié)議形式化分析方法作了一些比較,闡述了各自的特點.(2)首次提出用時延Petri網(wǎng)作為工具來分析和評估密碼協(xié)

2、議,并且給出了用它分析和評估密碼協(xié)議的具體方法和步驟.該方法不但能夠反映協(xié)議的結(jié)構(gòu)特性和動態(tài)特性,而且能夠?qū)γ艽a協(xié)議進行時間、空間上的性能評估.(3)給出了時延Petri網(wǎng)的引發(fā)規(guī)則、時間可達圖定義和構(gòu)造算法,并且介紹了時延Petri網(wǎng)的兩個基本分析方法:時間可達圖(或可覆蓋圖)和狀態(tài)方程.(4)用時延Petri網(wǎng)對MSR協(xié)議、Aziz-Diffle協(xié)議和TMN協(xié)議進行了具體和詳細的分析,給出了這三種協(xié)議的發(fā)生序列(執(zhí)行劇情)和攻擊者對