基于Event-B对存在网络攻击的安全协议的改进研究

发布时间：2022-10-05 14:40

　　设计对指定类型的网络攻击具有防御能力的安全协议,通常是一项重要且具有挑战性的任务。即使知道安全协议容易受到某种攻击,对其进行合理的改进也并不容易。本研究提出了一个基于Event-B方法的通用框架,用来指导安全协议的修改,并验证改进后的协议可以防御已知的网络攻击。首先用初始模型对攻击场景高度抽象,通过对抽象模型的精化,得到反映真实攻击过程的具体模型。然后将描述协议行为的事件从模型中分离出来,单独对其进行精化改进,如果改进后的协议事件重组的模型与具体模型不存在精化关系,则改进的合理性可以得到验证。最后通过NSPK协议被攻击的案例展示了本研究所提出方法的可用性。该框架可用于开发协议,以避免由逻辑漏洞引起的攻击,并验证协议补丁的正确性。 

【文章页数】：9 页

【文章目录】：
0 引言
1 Event-B方法
    1.1 Event-B模型
    1.2 模型的精化关系
    1.3 Rodin平台
2 对存在网络攻击的协议建模方法和分离规则
    2.1 基本概念
    2.2 建模过程
    2.3 分离规则
3 对存在网络攻击的协议进行改进并验证改进的合理性
    3.1 对协议进行改进
        3.1.1 对协议部分进行精化
        3.1.2 改变协议事件
    3.2 对改进的合理性进行验证
        3.2.1 用模型间的精化关系验证改进
        3.2.2 用模型检测方法验证改进
4 案例分析
    4.1 案例介绍
    4.2 建模过程
        4.2.1 初始模型
        4.2.2 具体模型
        4.2.3 精化改进协议
    4.3 验证改进的合理性
5 结语


【参考文献】：
博士论文
[1]基于Event-B的ad hoc路由协议及任务级时间约束的形式化建模与验证[D]. 付春艳.浙江大学 2019



本文编号：3685965