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

摘要：

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

关键词：形式化方法、精化理论、模型检测、Event-B方法、安全协议设计、网络攻击

所属期刊栏目：15

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金;上海市自然科学基金

在线出版日期：2020-08-05（万方平台首次上网日期，不代表论文的发表时间）

页数：共9页

页码：530-538