Modeling Secure MAVLink Protocol in the Tamarin Prover

Abstract

We present an intermediate formalization of the MAVLink protocol in the Tamarin Prover as the initial phase of a broader Software-In-The-Loop (SITL) simulation pipeline. In the first step, we define four core multiset-rewriting rules: InitKey, GCS_Send, Drone_Recv, and Replay_Attack to model key establishment, encrypted command transmission with monotonically increasing sequence counters, command reception with replay protection, and adversarial replay capabilities. The Tamarin model will be integrated into an underdevelopment QEMU-based ArduPilot SITL environment. Ongoing work focuses on embedding authenticated telemetry into the formal model, automating proof strategies within Tamarin, and forging a seamless link between symbolic verification and the protocol’s runtime behavior.