Project Abstract

Automated verification of security protocol has been an active research domain since the 1990s. The security of a protocol is challenging in the presence of an adversary and this mandates formal verification of the protocol. This project tries to demonstrate the formal verification of one of the security protocols using the tool Tamarin Prover. The project also tries to analyze the competency of the tool Tamarin. The security protocol is expected to be modeled in the symbolic model, in the presence of an external threat actor, and will be verified and validated for the security properties claimed by the protocol. Overall, the project presents the significance of the Tamarin tool in automatically proving security protocols. The security properties of a protocol viz secrecy, trace properties, equivalence properties, and authentication are to be tested to determine the correctness and error freeness of the protocol. Besides these, the protocol?��s existing implementation shall be subjected to alterations, and points of failure shall be observed.

Keywords: AUTOMATED VERIFICATION, SECURITY PROTOCOLS, TAMARIN PROVER

 Conference Details

Session: Presentation Stream 28 at Presentation Slot 9

Location: GH001 at Wednesday 8th 13:30 – 17:00

Markers: Neil Carter, Gary Tam

Course: MSc Cyber Security, Masters PG

Future Plans: I’m looking for an industry placement