随着无人机技术的快速发展，MAVlink 协议已成为无人机与地面站通信的事实标准，但其安全性设计相对薄弱。本文采用基于 pi 演算的形式化方法，利用 ProVerif 工具对 MAVlink 协议进行系统性安全分析。通过建立协议进程模型、定义安全属性查询、模拟 Dolev-Yao 攻击者行为，全面评估了 MAVlink 1.0 与 2.0 版本在机密性、完整性、认证性、防重放和可用性等方面的安全表现。研究发现，MAVlink 在非签名模式下存在消息伪造、重放、中间人攻击等多重漏洞；签名机制虽能显著提升认证与完整性，但仍受制于静态密钥管理、序列号空间有限等潜在风险。基于分析结果，本文提出一种分层安全增强架构，涵盖动态密钥协商、选择性加密、异常检测与响应机制，并通过扩展 ProVerif 模型验证了其有效性。