基于事件邏輯的可證明網(wǎng)絡(luò)安全協(xié)議形式化分析.pdf

1、形式化方法是分析網(wǎng)絡(luò)安全協(xié)議的一種重要方法，也是信息安全領(lǐng)域的研究熱點。形式化方法基于嚴格的數(shù)學(xué)概念和邏輯方法，對協(xié)議進行描述，在描述過程中可發(fā)現(xiàn)協(xié)議安全屬性的不明確或不完整，有效地降低分析過程復(fù)雜度，使協(xié)議的安全分析簡單、規(guī)范、實用。定理證明是形式化方法的一種，目的是證明無窮并發(fā)狀態(tài)下網(wǎng)絡(luò)安全協(xié)議是安全的。事件邏輯是在并發(fā)與分布式系統(tǒng)下描述協(xié)議和算法的邏輯，是定理證明中一種非常重要的邏輯方法。
　　本文以事件邏輯為基礎(chǔ)，對其進行

2、擴展，提出強認證理論。針對Needham-Schroeder（NS）協(xié)議和Neuman-Stubblebine協(xié)議進行形式化描述及認證性證明。論文主要工作包括：
　　1、基于事件邏輯，對安全協(xié)議的七種動作（生成挑戰(zhàn)數(shù)、發(fā)送消息、接收消息、加密、解密、簽名和驗證）進行形式化描述，同時給出協(xié)議中密鑰、挑戰(zhàn)數(shù)和協(xié)議消息的形式化描述。定義強匹配及匹配會話，結(jié)合事件邏輯公理和推理規(guī)則，提出強認證理論。
　　2、對兩個主體的NS協(xié)議進行

3、研究，針對協(xié)議漏洞，對其增加時間戳，避免了重放攻擊，運用事件邏輯對改進后的協(xié)議進行形式化描述，通過對發(fā)送者和接收者的認證證明，說明強認證理論適用于兩方的網(wǎng)絡(luò)安全協(xié)議；對三個主體的Neuman-Stubblebine協(xié)議進行研究，運用事件邏輯對協(xié)議基本序列進行合法定義，證明發(fā)送者是安全的而接收者是不安全的，不能達到雙向身份認證，說明強認證理論也適用于三方的網(wǎng)絡(luò)安全協(xié)議。
　　3、通過以上分析，認證協(xié)議可以通過只對協(xié)議誠實主體動作的推