Automating Cryptographic Protocol Language Generation from Structured Specifications

TL;DR

This paper introduces a tool that automates the generation of cryptographic protocol models and code from structured specifications, supporting multiple formal languages and verifying correctness.

Contribution

It extends previous data-centric approaches to support multiple target languages and verification tools, enhancing automation and expressiveness in protocol modeling.

Findings

Successfully modeled Diffie-Hellman key exchange

Demo includes Needham-Schroeder protocols

Supports verification and correctness checks

Abstract

Security of cryptographic protocols can be analysed by creating a model in a formal language and verifying the model in a tool. All such tools focus on the last part of the analysis, verification, and the interpretation of the specification is only explained in papers. Rather, we focus on the interpretation and modelling part by presenting a tool to aid the cryptographer throughout the process and automatically generating code in a target language. We adopt a data-centric approach where the protocol design is stored in a structured way rather than as textual specifications. Previous work shows how this approach facilitates the interpretation to a single language (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, ProVerif, as well as a C++ fully running implementation. Furthermore, we extend the plugins to verify correctness in ProVerif and executability lemmas in Tamarin. In this paper we model the Diffie-Hellman key exchange, which is traditionally used as a case study; a demo is also provided for other commonly studied protocols, Needham- Schroeder and Needham-Schroeder-Lowe.