One
Cryptographic Design
multiple interpretations!

About MetaCP

MetaCP is an automated tool simplifying the design of security protocols through a graphical interface.

  • Draw your protocol with Graphical Design Editor.
  • Save to format PSV (Protocol Specifications and Verification).
  • Interpret and export to some target language.
  • Do whatever with the export.

The graphical interface can be seen as a modern editor of a non-relational database whose data are protocols.The information of protocols is stored in XML, enjoying a fixed format and syntax aiming to contain all required information to specify any kind of protocol. This XML can be seen as an almost semanticless language, where different plugins confer strict semantics modelling the protocol into a variety of back-end verification languages.In the paper, we showcase the effectiveness of this novel approach by demonstrating how easy MetaCP makes it to design and verify a protocol going from the graphical design to formally verified protocol using a Tamarin prover plugin and a ProVerif plugin.
This is the first tool that allows to design and formally verify a security protocol in minutes!

Ready to design?

The quality of the demo is slightly less powerful (no delete, no undo capabilities) than the current development stage. We update the demo as soon as we have stable releases; we plan to make the designer an open-source project.

go to demobeta

Workflow

Step 1 – Design

The MetaCP Graphical Design Editor (GDE) aids the design of the protocol.

Drag and drop sets, variables, messages, cryptographic and mathematical constructions to shape the protocol you need.

Tools are currently available but many more are still required to be included and implemented.

Step 2 – Save your specs

The protocol is then saved as a PSV file, which is a structured XML, validated against a DTD specification.

We are enriching the PSV description (DTD) to let it be expressive enough to replace natural language specification.
(Multiple) natural languages would then be target languages in MetaCP.

Step 3 – Export

We written a rudimental plugin that interprets the PSV with Tamarin semantics: the result is coherent code. To appreciate the benefit, we just remark that typos, e.g. on variable names, are not detected by Tamarin and may lie in the code undetected.
In particular, we export executability only. Executability proves that the protocol can run between honest parties from the beginning to the end.

Our plugin is not the plugin for Tamarin in MetaCP, is just one plugin for Tamarin. New plugins targeting the same languages are supported!

Step 4 – Verify (or whatever)

This final step is actually outside of MetaCP.
The Tamarin prover is able to formally verify the code automatically generated from the graphical design.

This can be done in ten minutes. Let's assume one day. Don't push it! Even if you find MetaCP not easy to use as it could be, nobody would believe that for dragging and dropping a couple of items you can spend more than one day to reproduce the Diffie-Hellman key exchange.
Now, find any formal language that you learn in one day and get a protocol correct and formally verified.

Examples of protocols

Diffie-Hellman key exchange

key exchange

Needham-Schroeder

key exchange

Needham-Schroeder-Lowe

key exchange

Accommodate diverse users

Research material

Poster

Towards a Data Centric Approach for the Design and Verification of Cryptographic Protocols
(Presented at CCS'19)

Paper

Towards a Data Centric Approach for the Design and Verification of Cryptographic Protocols
(Proceedings of ACM CCS'19 - poster section)

Paper

Automating Cryptographic Protocol Language Generation from Structured Specifications
(preprint of accepted paper at FormaliSE'22)

Frequently Asked Questions

  • You need to show how the semantics of your plugin captures the aspects you model by interpreting the structure of the PSV. It should suffice to be as formal as you would do in security papers while interpreting to a formal language from specifications written in a natural language (e.g. English).

  • You might, but the result would unlikely be complete, because the PSV usually captures more information than the model in the target language.

  • It is currently not possible, but future extensions may include it!

    • Gives you a kick-start to formalisation in your favourite language.
    • You can export to many languages.
    • No syntax errors, no spelling mistakes.
    • Need more? Ask us!
  • We plan to provide the source code of MetaCP and example plugins, but we need more time to work on a presentable release.