基于Petri網(wǎng)的安全協(xié)議分析與驗證技術(shù).pdf

1、在一個分布式的網(wǎng)絡(luò)環(huán)境中，人們通過安全協(xié)議實現(xiàn)安全共享網(wǎng)絡(luò)資源的需求，因此安全協(xié)議的安全性逐漸成為網(wǎng)絡(luò)安全的關(guān)鍵。傳統(tǒng)的安全協(xié)議分析技術(shù)包括傳統(tǒng)的基于推理結(jié)構(gòu)性方法，基于攻擊結(jié)構(gòu)性方法以及基于證明結(jié)構(gòu)性方法三大類。 Petri網(wǎng)原本是用于并行系統(tǒng)分析的工具，但隨著關(guān)注安全協(xié)議的學(xué)者不斷實踐，使用Petri網(wǎng)方法實現(xiàn)對安全協(xié)議的分析驗證已經(jīng)初露端倪。繼[ALMU03]對STS協(xié)議的成功分析之后，[GULO05l和[DRES05]也

2、分別成功地對3GPPAKA協(xié)議和SAP無線協(xié)議進行分析，其中[GULO05]的工作是本文的重點內(nèi)容。 BAN邏輯是基于推理結(jié)構(gòu)性方法的經(jīng)典，但是它本身具有一定的缺陷，尤其是對重放攻擊的檢測能力十分弱。3GPPAKA協(xié)議設(shè)計者使用BAN邏輯進行分析，聲稱協(xié)議的安全目標(biāo)已經(jīng)達到[3GTS33]。然而，本文使用Petri網(wǎng)的分析將會得到不同的結(jié)果。 一個認(rèn)證協(xié)議可以看成在其執(zhí)行過程中通信實體信仰不斷變化的過程，因此對一個認(rèn)證協(xié)