Project Abstract

– Motivation and backgroundThere’s an increasing cyberattacks targeting security protocols due to weak configuration and verification. With an evolving landscape of information and communication systems, there’s a pressing need to continually refine and validate security protocols. – The proposition of this researchThis project gives the basic detailed exploration of the Tamarin Prover’s methodologies, emphasizing its distinctive position in the security verification domain.- Methods employedThis study revolves around a structured approach to investigate Tamarin Prover’s functionalities. It employs the Diffie-Hellman key exchange protocol as a case study, implementing and modelling it within the Tamarin Prover framework.- Main FindingsThe ability of Tamarin Prover to automatically generate proofs based on formal protocol definitions, proving or disproving security properties. Although the tool works well, handling complex protocols is difficult due to its partial automation, which necessitates manual interventions for thorough verification.- Conclusion / ContributionOur study explains our knowledge of the Tamarin Prover’s capabilities and limits in terms of guaranteeing the security of cryptographic systems and provides insightful information on the verification of security protocols.

Keywords: Verification, Protocol, Tamarin

 Conference Details

Session: Presentation Stream 22 at Presentation Slot 2

Location: CoFo 002 at Wednesday 8th 09:00 – 12:30

Markers: Deepak Sahoo, John Tucker

Course: MSc Cyber Security, Masters PG

Future Plans: I’m looking for an industry placement