Formal security verification of the Drone Remote Identification Protocol using Tamarin

Sammanfattning: The current standard for remote identification of unmanned aircraft does not contain anyform of security considerations, opening up possibilities for impersonation attacks. Thenewly proposed Drone Remote Identification Protocol aims to change this. To fully ensurethat the protocol is secure before real world implementation, we conduct a formal verification using the Tamarin Prover tool, with the goal of detecting possible vulnerabilities. Theunderlying technologies of the protocol are studied and important aspects are identified.The main contribution of this thesis is the formal verification of session key secrecy andmessage authenticity within the proposed protocol. Certain aspects of protocol securityare still missing from the scripts, but the protocol is deemed secure to the extent of themodel. Many features of both the protocol and Tamarin Prover are presented in detail,serving as a potential base for the continued work toward a complete formal verificationof the protocol in the future.