Using first-order theorem provers for security protocol verification

In today’s computer-dominated world, cryptographic security protocols are exceptionally important in ensuring secure communication over an insecure network. Hence, this has led to much research in this field, leading to security protocols being developed and deployed. However, a majority of these existing protocols have been found to contain vulnerabilities after deployment. Even with the knowledge of such vulnerabilities, insecure protocols are still being created. This could be due to the difficulty faced by developers in checking for flaws in the protocols. It remains a difficult task to analyze cryptographic security protocols manually. This project aims to tackle this problem by running security protocols modeled in First-Order Logic through dedicated theorem provers such as Proverif, and fullfledged theorem provers like Vampire. Proverif makes use of a weak attacker model, Dolev-Yao model, which leads to attacks undetected. Although a richer attacker model is used for Vampire, it may not necessary be more efficient than Proverif. Hence, the theorem provers’ efficiencies are analyzed and compared. The outcome of the project shows that both Proverif and Vampire are almost as capable in analyzing security protocols, since there remain protocols that Proverif can detect while Vampire could not, and vice versa. Thus, it can be concluded that there is no clear winner in terms of performance, and the best result is only achieved when the provers are used in parallel.Bachelor of Engineering (Computer Science