We present MetaCP, a tool to aid the cryptographer throughout the process of designing and modelling a communication protocol suitable for formal verification. The crucial innovative aspect of the tool is its data-centric approach, where protocol specification is stored in a structured way rather than in natural languages to facilitate its interpretation to multiple target languages. Previous work shows a single exporting plugin (for Tamarin) which required aftermath modifications. By improving the expressiveness of the specification data structure we extend the tool to export to an additional formal language, i.e. ProVerif, as well as a C++ implementation. Starting with its modern graphical interface, MetaCP allows us to model the Diffie-Hellman key exchange, traditionally referred to as a case study, in just a few minutes. Ultimately, we use the formal tools to verify the executability and correctness of the automatically exported models. The design core of MetaCP is freely available in an online demo that provides two further sample protocols, Needham-Schroeder and Needham-Schroeder-Lowe, along with instructions to use the tool to begin modelling from scratch and to export the model to desired external languages.
Download