Formal Verification and Security Assessment of the Drone Remote Identification Protocol

The worldwide implementation of Remote Identification (RID) regulations mandates unmanned aircraft systems (UAS), or drones, to openly transmit their identity and realtime location as plain text on the wireless channel. This mandate serves the purpose of accounting for and monitoring drone operations effectively. However, the current RID standard's plain-text transmission exposes it to cyberattacks, including eavesdropping, injection, and impersonation. The Drone Remote Identification Protocol (DRIP) has been proposed to enhance the security of RID. The DRIP ensures information secrecy and confidentiality by using unique session keys while guaranteeing the authenticity of messages and entities through digital signatures. These security features of DRIP make it a preferable alternative to the existing RID standard. However, the lack of verification regarding its security claims raises concerns about its performance in hostile conditions. This paper comprehensively analyzes the DRIP protocol's security features using Tamarin Prover, a formal security verification tool. With its automated reasoning capabilities, Tamarin Prover accurately identifies potential security vulnerabilities within the DRIP protocol while thoroughly verifying its conformance to security properties. Our investigation demonstrates that the DRIP protocol is susceptible to replay attacks. We strongly recommend the inclusion of message freshness components, reducing the lifespan of DET broadcasts, and incorporating a not-after timestamp that is set only a few minutes ahead of the current time. These measures enhance the protocol's defence against replay attacks and ensure message authenticity and integrity.