Web GUI for Automating the Formal Verification of Security Protocols using Casper FDR4

摘要

Over the last two decades, Casper & FDR have proved to be two very important tools in the domain of formal verification of security protocols. Both their creators and the formal verification community have used these tools to find attacks on proposed security protocols and to also design fixes for them. This paper presents a web application developed with the purpose of automating the use of Casper & FDR in order to ease the model checking process and to provide some extra functionality for the analysis of the obtained results (e.g. graphical representation of the verified protocols and of the reported attacks). The mentioned ongoing importance of these tools has motivated the work described in this paper and also indicates its potential importance.