Tamgram: A Frontend for Large-scale Protocol Modeling in Tamarin

TL;DR

Tamgram is a high-level modeling language designed to simplify the creation and maintenance of large-scale security protocol specifications in Tamarin, improving usability without sacrificing performance.

Contribution

Introduces Tamgram, a high-level language with formal semantics for large protocol modeling in Tamarin, including translation strategies and performance analysis.

Findings

Tamgram enables easier large protocol specification.

Translation strategies achieve performance comparable to manual Tamarin code.

Validated with multiple case studies, including large-scale protocols.

Abstract

Automated security protocol verifiers such as ProVerif and Tamarin have been increasingly applied to verify large scale complex real-world protocols. While their ability to automate difficult reasoning processes required to handle protocols at that scale is impressive, there remains a gap in the modeling languages used. In particular, providing support for writing and maintaining large protocol specifications. This work attempts to fill this gap by introducing a high-level protocol modeling language, called Tamgram, with a formal semantics that can be translated to the multiset rewriting semantics of Tamarin. Tamgram supports writing native Tamarin code directly, but also allows for easier structuring of large specifications through various high-level constructs, in particular those needed to manipulate states in protocols. We prove the soundness and the completeness of Tamgram with respect to the trace semantics of Tamarin, discuss different translation strategies, and identify an optimal strategy that yields performance comparable to manually coded Tamarin specifications. Finally we show the practicality of Tamgram with a set of small case studies and one large scale case study.