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
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.
Accommodate diverse users
Ist Udy
Student
Finally, I can see the whole protocol and understand it better!
Jo Bd. One
Engineer
I do not need to understand the cryptography in depth to implement solutions.
Bur Densome
Security expert
I can prototype solutions and quickly verify subtle mistakes.
Lamb Dax
Formal modeller
I can reason in multiple models and tools to gain trust in my claims.
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
-
How can I trust the interpretation of the plugins?
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).
-
Can you import tool models to MetaCP?
You might, but the result would unlikely be complete, because the PSV usually captures more information than the model in the target language.
-
Can I visualise attacks on MetaCP?
It is currently not possible, but future extensions may include it!
-
Why else should I use this tool?
- 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!
-
Where can I find the source code?
We plan to provide the source code of MetaCP and example plugins, but we need more time to work on a presentable release.