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

作     者：朱俊翔 张翔 ZHU Jun-xiang;ZHANG Xiang

作者机构：华东师范大学上海200062 

基　　金：国家自然科学基金(61602177) 上海市自然科学基金(18ZR1411600) 

出 版 物：《中国电子科学研究院学报》 (Journal of China Academy of Electronics and Information Technology)

年 卷 期：2020年第15卷第6期

页      码：530-538页

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

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

学科分类：08[工学] 0835[0835] 081202[081202] 0812[工学-测绘类] 

D　O　I：10.3969/j.issn.1673-5692.2020.06.007

馆 藏 号：203953636...