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

摘要:

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

Abstract: