刘 栋，连晓峰，王宇龙，谭 励，赵宇琦，李 林

(1.北京工商大学 人工智能学院，北京 100048；2.中国兵器工业信息中心，北京 100089；3.北京工商大学 计算机学院，北京 100048)

0 引言

随着科学技术的不断发展，生产力不断进步，无人机的技术越来越成熟，无人机已经走进人们的日常生产和生活中。由于无人机具有成本较低，操作简单，灵活度高，适用于多种复杂环境等优点，故无人机广泛应用于环境探测[1]、货物运输[2]、应急救援[3]及个人航拍等领域。然而无人机在给我们的日常生产生活带来便利的同时，无人机通信方面可能会受到攻击者的攻击[4]，使无人机通讯信息遭到泄露，从而产生严重的安全问题[5]。

形式化方法[6]是一种以数学为基础，使系统设计各个步骤实现可靠性和正确性的方法，在协议设计方面的应用极大地提高了安全协议的可靠性。形式化方法主要分为逻辑推理[7]，模型检测[8]和定理证明[9]。模型检测可以自动检测要验证的系统是否满足要验证的属性，如果不满足要验证的属性，则会给出攻击流程图。模型检测具有完全自动化，检测速度快，自动显示攻击流程图等优点。

2002年Maggi等人[10]以N-S公钥协议为例，提出一种基于模型检测工具SPIN(Simple Promela Interpreter)的安全协议建模分析方法。2006年M.H.Xiao等人[11]提出了一种Promela建模的方法，并对Helsinki协议进行建模，发现了对此协议的攻击。2015年程道雷等人[12]对OAuth2.0协议进行分析，拓展了Maggi的方法，实现了多主体建模分析。2017年梅映天等人[13]对Maggi的方法进行改进，实现了四通道并行建模法，优化了模型复杂度。……