无人机无线通信协议的形式化认证分析与验证

Formal Authentication Analysis and Verification of UAV Wireless Communication Protocol

针对无人机组与地面控制站之间进行无线通信时的身份认证问题,首先分析无线通信协议的工作流程及其形式化表示,然后对网络系统中的诚实主体和攻击者进行形式化建模,其中推导了协议安全属性的LTL公式,通过建立密钥机制,实现控制站与无人机节点以及各个无人机节点之间的身份认证;运用模型检测工具SPIN验证无线通信协议的一致性,其中提出一种改进的知识项获取方法,加快攻击者需掌握知识集的求取过程;验证结果表明该无人机无线通信协议具有中间人攻击漏洞。

In order to solve the issue of identity authentication in wireless communication between UAV and control station,the workflow of wireless communication protocol as well as formal representation are analyzed firstly.Then the honest agent and attacker agent in the network system are formal modeled,in which the LTL formula of the security attribute of the protocol are derived.The identity authentication between the control station and UAV nodes as well as are implemented by establishing the key mechanism.The consistency of wireless communication protocol is verified by using SPIN,which is a model checking tool.An improved method of acquiring knowledge items is proposed to speed up the process of acquiring knowledge sets for attackers.The verification results show that the UAV wireless communication protocol has intermediary attack vulnerability.