1、在一個(gè)分布式的網(wǎng)絡(luò)環(huán)境中，人們通過(guò)安全協(xié)議實(shí)現(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é)者不斷實(shí)踐，使用Petri網(wǎng)方法實(shí)現(xiàn)對(duì)安全協(xié)議的分析驗(yàn)證已經(jīng)初露端倪。繼[ALMU03]對(duì)STS協(xié)議的成功分析之后，[GULO05l和[DRES05]也

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