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

A Framework for Revising Security Protocols Against Network Attacks Based on Event-B

作　　者：朱俊翔 张翔[1] ZHU Jun-xiang;ZHANG Xiang(East China Normal University,Shanghai 200062,China)

机构地区：[1]华东师范大学,上海200062

出　　处：《中国电子科学研究院学报》2020年第6期530-538,共9页Journal of China Academy of Electronics and Information Technology

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

摘　　要：设计对指定类型的网络攻击具有防御能力的安全协议,通常是一项重要且具有挑战性的任务。即使知道安全协议容易受到某种攻击,对其进行合理的改进也并不容易。本研究提出了一个基于Event-B方法的通用框架,用来指导安全协议的修改,并验证改进后的协议可以防御已知的网络攻击。首先用初始模型对攻击场景高度抽象,通过对抽象模型的精化,得到反映真实攻击过程的具体模型。然后将描述协议行为的事件从模型中分离出来,单独对其进行精化改进,如果改进后的协议事件重组的模型与具体模型不存在精化关系,则改进的合理性可以得到验证。最后通过NSPK协议被攻击的案例展示了本研究所提出方法的可用性。该框架可用于开发协议,以避免由逻辑漏洞引起的攻击,并验证协议补丁的正确性。Designing a security protocol is immune to a given kind of network attacks is usually an important but challenging task,even we know the security protocol is vulnerable to some kind of attacks,revising it is not an easy work. This paper proposes a generic framework based on Event-B method to guide the revising of a security protocol so that the known successful attack can no longer take places upon the revised protocol. The attack scenario is reflected with an abstract model and is refined to the concrete model which can capture the behaviors from both the protocol and the attacker. Then the revision of the protocol can be modeled by first separating the protocol behavior from the model and refine it solely. The security of the revised protocol can be verified by showing that the composed model with the attack is no longer a refinement of the concrete model. Finally,we demonstrate the feasibility of this approach on a case study about an insecure protocol. The framework can be used to develop protocols to avoid attacks caused by logical vulnerabilities,and to verify the correctness of patches to protocol improvement.

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]