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

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

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

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