Automating Cryptographic Protocol Language Generation from Structured Specifications

Roberto Metere, Luca Arnaboldi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish
Title of host publicationProceedings - IEEE/ACM 10th International Conference on Formal Methods in Software Engineering, FormaliSE 2022
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages91-101
Number of pages11
ISBN (Electronic)9781450392877
DOIs
Publication statusPublished - 21 Jul 2022
Event10th IEEE/ACM International Conference on Formal Methods in Software Engineering, FormaliSE 2022 - Pittsburgh, United States
Duration: 18 May 202219 May 2022

Publication series

NameProceedings - IEEE/ACM 10th International Conference on Formal Methods in Software Engineering, FormaliSE 2022

Conference

Conference10th IEEE/ACM International Conference on Formal Methods in Software Engineering, FormaliSE 2022
Country/TerritoryUnited States
CityPittsburgh
Period18/05/2219/05/22

Bibliographical note

Funding Information:
This research was partly funded by The Alan Turing Institute through the Lloyd’s Register Foundation (G0095), an Innovate UK e4Future grant (104227), and EPSRC grants EP/S016627/1, Active Building Centre, and EP/T027037/1 AISEC.

Publisher Copyright:
© 2022 ACM.

Keywords

  • Automated Software Development
  • Formal Security Models
  • Protocol Design

Cite this