安全協(xié)議的形式化分析.pdf

1、隨著計(jì)算機(jī)網(wǎng)絡(luò)通信的迅猛發(fā)展，安全協(xié)議的重要性越來越得到重視。安全協(xié)議負(fù)責(zé)密鑰分發(fā)和身份認(rèn)證，一旦其自身出現(xiàn)漏洞，那么將會(huì)對(duì)通信的安全造成威脅?；谶@種迫在眉睫的需求，本文分別用基于BAN邏輯和基于符號(hào)化模型檢測的方法對(duì)安全協(xié)議進(jìn)行形式化分析。
　　本文的主要工作有:
　　(1)使用BAN邏輯對(duì)YAHALOM協(xié)議進(jìn)行協(xié)議理想化以及關(guān)于密鑰Kas、Kab、Kbs的有效性、服務(wù)器S的權(quán)威性、隨機(jī)數(shù)Na和Nb的新鮮性等初始狀態(tài)假設(shè)

2、以及在BAN邏輯規(guī)定的六條規(guī)則的基礎(chǔ)上進(jìn)行推理證明，來驗(yàn)證協(xié)議能否達(dá)到文中提出的協(xié)議一級(jí)目標(biāo)和二級(jí)目標(biāo)。同時(shí)對(duì)邏輯推理結(jié)果進(jìn)行分析，如果協(xié)議滿足部分安全目標(biāo)那就說明協(xié)議存在安全漏洞，那么我們就在分析結(jié)果的基礎(chǔ)上對(duì)YAHALOM協(xié)議的改進(jìn)提出建設(shè)性的意見;
　　(2) SMV是安全協(xié)議形式化進(jìn)行自動(dòng)化驗(yàn)證的工具。文中在闡述符號(hào)化模型檢測軟件SMV的語法語義并在小系統(tǒng)模型的基礎(chǔ)上，對(duì)YAHALOM協(xié)議中的三個(gè)通信實(shí)體建立有限狀態(tài)機(jī)模型

3、，同時(shí)在分析協(xié)議消息的基礎(chǔ)上創(chuàng)建初始者A、響應(yīng)者B和服務(wù)器S三個(gè)誠實(shí)通信實(shí)體的狀態(tài)轉(zhuǎn)換圖，當(dāng)然我們也會(huì)給出入侵者I冒充初始者、響應(yīng)者或者是服務(wù)器的狀態(tài)轉(zhuǎn)換圖。接著根據(jù)創(chuàng)建的狀態(tài)轉(zhuǎn)換圖給出三個(gè)誠實(shí)通信實(shí)體的狀態(tài)轉(zhuǎn)換的自然語言描述，并在此基礎(chǔ)上對(duì)YAHALOM協(xié)議進(jìn)行詳細(xì)的建模。然后根據(jù)SMV語法語義給出協(xié)議要驗(yàn)證的關(guān)于認(rèn)證性、保密性、安全性和完整性等性質(zhì)。最后用SMV執(zhí)行文中建立的模型，以此來驗(yàn)證YAHALOM協(xié)議是否符合文中提出的R1～