10.3969/j.issn.1673-5692.2020.06.007
基于Event-B对存在网络攻击的安全协议的改进研究
设计对指定类型的网络攻击具有防御能力的安全协议,通常是一项重要且具有挑战性的任务.即使知道安全协议容易受到某种攻击,对其进行合理的改进也并不容易.本研究提出了一个基于Event-B方法的通用框架,用来指导安全协议的修改,并验证改进后的协议可以防御已知的网络攻击.首先用初始模型对攻击场景高度抽象,通过对抽象模型的精化,得到反映真实攻击过程的具体模型.然后将描述协议行为的事件从模型中分离出来,单独对其进行精化改进,如果改进后的协议事件重组的模型与具体模型不存在精化关系,则改进的合理性可以得到验证.最后通过NSPK协议被攻击的案例展示了本研究所提出方法的可用性.该框架可用于开发协议,以避免由逻辑漏洞引起的攻击,并验证协议补丁的正确性.
形式化方法、精化理论、模型检测、Event-B方法、安全协议设计、网络攻击
15
TP311(计算技术、计算机技术)
国家自然科学基金;上海市自然科学基金
2020-08-05(万方平台首次上网日期,不代表论文的发表时间)
共9页
530-538