Formal analysis of security protocols is becoming increasingly relevant. In formal analysis, a model is created of a protocol or system, and propositions about the security of the model are written. A program is then used to verify that the propositions hold, or find examples of where they do not. This report uses formal methods to analyse the authentication aspect of a protocol that allows private individuals, enterprises, and systems to securely and asynchronously share sensitive data. Unpublished, early drafts of the protocol were studied and algorithms described in it were verified with the help of the formal verification tool Tamarin Prover. The analysis revealed two replay attacks. Improvements to the protocol were suggested based on this analysis. In later versions of the protocol, the improvements have been implemented by the protocol developers. / Det blir alltmer relevant med formell analys av säkerhetsprotokoll. I formell analys så skapas en modell av ett protokoll eller ett system, och påståenden om modellens säkerhet skrivs. Ett program används sedan för att verifiera att påståendena gäller, eller för att hitta exempel där de inte gäller. Den här rapporten avänder formella metoder för att analysera autentiseringsaspekten av ett protokoll som tillåter privatpersoner, företag och system att asynkront dela känslig information på ett säkert sätt. Opublicerade och tidiga utkast av protokollet studerades och de algoritmer som beskrivs i protokollet verifierades med hjälp av Tamarin Prover. Analysen avslöjade två återspelningsattacker. Förbättringar till protokollet föreslogs baserat på denna analys. I senare versioner har protokollutvecklarna implementerat förslagen.

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.