發(fā)布時(shí)間：2022-10-05 14:40

　　設(shè)計(jì)對(duì)指定類型的網(wǎng)絡(luò)攻擊具有防御能力的安全協(xié)議,通常是一項(xiàng)重要且具有挑戰(zhàn)性的任務(wù)。即使知道安全協(xié)議容易受到某種攻擊,對(duì)其進(jìn)行合理的改進(jìn)也并不容易。本研究提出了一個(gè)基于Event-B方法的通用框架,用來(lái)指導(dǎo)安全協(xié)議的修改,并驗(yàn)證改進(jìn)后的協(xié)議可以防御已知的網(wǎng)絡(luò)攻擊。首先用初始模型對(duì)攻擊場(chǎng)景高度抽象,通過(guò)對(duì)抽象模型的精化,得到反映真實(shí)攻擊過(guò)程的具體模型。然后將描述協(xié)議行為的事件從模型中分離出來(lái),單獨(dú)對(duì)其進(jìn)行精化改進(jìn),如果改進(jìn)后的協(xié)議事件重組的模型與具體模型不存在精化關(guān)系,則改進(jìn)的合理性可以得到驗(yàn)證。最后通過(guò)NSPK協(xié)議被攻擊的案例展示了本研究所提出方法的可用性。該框架可用于開(kāi)發(fā)協(xié)議,以避免由邏輯漏洞引起的攻擊,并驗(yàn)證協(xié)議補(bǔ)丁的正確性。 

【文章頁(yè)數(shù)】：9 頁(yè)

【文章目錄】：
0 引言
1 Event-B方法
    1.1 Event-B模型
    1.2 模型的精化關(guān)系
    1.3 Rodin平臺(tái)
2 對(duì)存在網(wǎng)絡(luò)攻擊的協(xié)議建模方法和分離規(guī)則
    2.1 基本概念
    2.2 建模過(guò)程
    2.3 分離規(guī)則
3 對(duì)存在網(wǎng)絡(luò)攻擊的協(xié)議進(jìn)行改進(jìn)并驗(yàn)證改進(jìn)的合理性
    3.1 對(duì)協(xié)議進(jìn)行改進(jìn)
        3.1.1 對(duì)協(xié)議部分進(jìn)行精化
        3.1.2 改變協(xié)議事件
    3.2 對(duì)改進(jìn)的合理性進(jìn)行驗(yàn)證
        3.2.1 用模型間的精化關(guān)系驗(yàn)證改進(jìn)
        3.2.2 用模型檢測(cè)方法驗(yàn)證改進(jìn)
4 案例分析
    4.1 案例介紹
    4.2 建模過(guò)程
        4.2.1 初始模型
        4.2.2 具體模型
        4.2.3 精化改進(jìn)協(xié)議
    4.3 驗(yàn)證改進(jìn)的合理性
5 結(jié)語(yǔ)


【參考文獻(xiàn)】：
博士論文
[1]基于Event-B的ad hoc路由協(xié)議及任務(wù)級(jí)時(shí)間約束的形式化建模與驗(yàn)證[D]. 付春艷.浙江大學(xué) 2019



本文編號(hào)：3685965