安全協(xié)議保障信息資源在交互過程中的機(jī)密性、完整性及可用性。形式化方法規(guī)范密碼協(xié)議的安全特性,擁有較完善的理論體系及模型。定理證明是形式化方法的一種,基于嚴(yán)格數(shù)學(xué)理論知識和邏輯推導(dǎo),確定協(xié)議是否在合理假設(shè)下滿足要驗(yàn)證的安全屬性。事件邏輯理論是一種描述并發(fā)與分布式系統(tǒng)中狀態(tài)遷移和算法的定理證明方法,可用于證明網(wǎng)絡(luò)協(xié)議的安全性。本文運(yùn)用事件邏輯理論分析無線Mesh網(wǎng)絡(luò)客戶端認(rèn)證協(xié)議安全性,降低協(xié)議分析過程中的冗余度及復(fù)雜度,提高協(xié)議分析效率。論文主要工作如下:（1）基于事件邏輯理論,結(jié)合事件結(jié)構(gòu)、事件類、公理簇以及隨機(jī)數(shù)引理等,提出置換規(guī)則保證協(xié)議交互用戶在置換中性質(zhì)的等價轉(zhuǎn)換,推導(dǎo)出多組合信息交互、不疊加、事件匹配、去重復(fù)、去未來等性質(zhì),擴(kuò)展事件邏輯理論在協(xié)議分析中的應(yīng)用。（2）通過事件邏輯描述客戶端與LTCA間交互協(xié)議的基本序列,對協(xié)議交互動作形式化描述。證明協(xié)議強(qiáng)認(rèn)證性質(zhì),得出無線Mesh網(wǎng)絡(luò)客戶端與LTCA間認(rèn)證協(xié)議在合理假設(shè)下是安全的。表明事件邏輯理論可以對安全協(xié)議不同身份主體間的認(rèn)證性進(jìn)行證明。（3）在客戶端用戶已得到LCA頒發(fā)的認(rèn)證證書條件下,通過事件邏輯理論證明無線Mesh網(wǎng)... 

【文章來源】：華東交通大學(xué)江西省

【文章頁數(shù)】：57 頁

【學(xué)位級別】：碩士

【文章目錄】：
摘要
abstract
符號說明
第一章 緒論
    1.1 研究背景及意義
    1.2 發(fā)展歷史及研究現(xiàn)狀
    1.3 本文主要內(nèi)容
    1.4 論文結(jié)構(gòu)安排
第二章 無線Mesh網(wǎng)絡(luò)協(xié)議及形式化方法概述
    2.1 無線Mesh網(wǎng)絡(luò)
        2.1.1 無線Mesh網(wǎng)絡(luò)概述
        2.1.2 無線Mesh網(wǎng)絡(luò)的安全威脅
        2.1.3 無線Mesh網(wǎng)絡(luò)認(rèn)證協(xié)議的安全需求
    2.2 無線Mesh網(wǎng)絡(luò)客戶端協(xié)議分析
        2.2.1 WMN客戶端與LTCA間認(rèn)證協(xié)議
        2.2.2 WMN客戶端間認(rèn)證協(xié)議
    2.3 形式化方法概述
        2.3.1 模型檢測
        2.3.2 定理證明
第三章 事件邏輯理論
    3.1 事件邏輯理論
        3.1.1 基本定義
        3.1.2 加密系統(tǒng)建模
    3.2 事件邏輯理論公理、推論及性質(zhì)
        3.2.1 事件邏輯理論公理
        3.2.2 事件邏輯理論推論及性質(zhì)
    3.3 形式化方法描述協(xié)議
        3.3.1 線程和基本序列
        3.3.2 匹配會話及協(xié)議動作
        3.3.3 事件邏輯方法描述協(xié)議
    3.4 安全協(xié)議證明過程
        3.4.1 事件邏輯理論方法證明流程詳述
        3.4.2 事件邏輯理論方法證明流程
    3.5 本章小結(jié)
第四章 無線Mesh網(wǎng)協(xié)議形式化分析
    4.1 WMN客戶端與LTCA間雙向認(rèn)證協(xié)議證明
        4.1.1 協(xié)議的形式化分析
        4.1.2 協(xié)議證明過程
    4.2 WMN客戶端間雙向協(xié)議認(rèn)證性證明
        4.2.1 協(xié)議的形式化分析
        4.2.2 協(xié)議證明過程
    4.3 本章小結(jié)
第五章 形式化方法對比分析
    5.1 事件邏輯理論與模態(tài)邏輯比較
    5.2 事件邏輯理論與PCL比較
    5.3 事件邏輯理論通用性
第六章 總結(jié)與展望
    6.1 總結(jié)
    6.2 展望
參考文獻(xiàn)
個人簡歷在讀期間發(fā)表的學(xué)術(shù)論文
致謝



本文編號：3107803