EVALUATING FORMAL METHODS FOR VERIFYING SECURITY PROTOCOLS: A CASE STUDY OF TAMARIN, AVISPA, AND PROVERIF

Verifying security protocols using formal methods is crucial to ensure their robustness against cyber threats. Several verification tools, including Tamarin, AVISPA, and ProVerif, offer different methodologies for protocol analysis. However, a comprehensive comparative analysis of these tools under uniform conditions remains limited. This study systematically evaluates these three tools by assessing their verification mechanisms, supported programming languages, and usability. A standardized testing framework was employed to ensure a consistent comparison, focusing on two widely used security protocols: the Diffie-Hellman Key Exchange Protocol and the Needham-Schroeder Public Key Protocol. The findings highlight distinct strengths and weaknesses in each tool. Tamarin demonstrated superior capability in detecting active attacks such as Man-in-the-Middle (MitM) attacks, while ProVerif was more effective in identifying passive attacks like eavesdropping. AVISPA, on the other hand, provided a broader but less detailed security analysis. These insights help researchers and practitioners select the most appropriate tool based on protocol complexity and security requirements. Unlike prior research that focused on individual tools, this study offers a comprehensive empirical comparison, providing deeper insights into their practical effectiveness and limitations. The results contribute to enhancing security protocol verification methodologies and informing future improvements in formal verification tools.