Return to search

Verification of MAKE, a security protocol for LDACS : Modeling 'Mutual Authentication and Key Exchange' protocol in Tamarin Prover / Verifiering av säkerhetsprotokollet MAKE i Tamarin Prover

This report presents an approach to reinforce the security of the L-band Digital Aeronautical Communications System (LDACS) by developing and testing an enhanced protocol model. We have created a protocol model of MAKE, Mutual authentication and Key Exchange, based on the paper "Enhancing Cybersecurity for LDACS: a Secure and Lightweight Mutual Authentication and Key Agreement Protocol" by Suleman Khan, Gurjot Singh Gaba, Andrei Gurtov, in which the research paper addresses the security challenges inherent in LDACS. Using the open-source tool Tamarin Prover, we analysed and simulated the protocol to evaluate its effectiveness against posing threats. In this paper, our methodology involves an understanding of the MAKE protocol's architecture, identifying vulnerabilities and modeling in Tamarin Prover, to strengthen the security of LDACS. We developed two models of the protocol. The test consisted of four different lemmas and revealed partial verification of the two models, but with different outcomes. Some aspects of the model were proven to be true. Therefore, further research needs to be done to successfully validate these lemmas to ensure the robustness and reliability of the analyzed security protocol, MAKE.

Identiferoai:union.ndltd.org:UPSALLA1/oai:DiVA.org:liu-204848
Date January 2024
CreatorsStyfberg, Max, Odermalm, Josefin
PublisherLinköpings universitet, Institutionen för datavetenskap
Source SetsDiVA Archive at Upsalla University
LanguageEnglish
Detected LanguageEnglish
TypeStudent thesis, info:eu-repo/semantics/bachelorThesis, text
Formatapplication/pdf
Rightsinfo:eu-repo/semantics/openAccess

Page generated in 0.0021 seconds