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

来源：计算机测量与控制杂志2021年第4期北京时间：

作者：刘栋,连晓峰,王宇龙,谭励,赵宇琦,李林

单位：北京工商大学

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

关键词：无人机无线通信协议;形式化表示与建模;模型检测工具SPIN;攻击者知识项获取

基金资助：装备发展部项目(170341402020)