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

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

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

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