Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Di Long Li, Jim de Groot, Alwen Tiu

TL;DR

Tamgram provides a high-level, modular frontend for the Tamarin prover, designed to address the scalability and maintainability challenges of large-scale security protocol specifications. It marries an ML-style module system, hygienic macros, and process-local memory to capture complex stateful interactions, while remaining faithful to Tamarin through a formal, trace-preserving translation. The authors develop a CFG-based intermediate representation and analyze multiple translation strategies, concluding that a hybrid forward/backward approach yields performance close to manually coded Tamarin models and improves readability. Empirical results on EMVerify and CSF18 XOR demonstrate practical viability and the potential for significant usability gains in real-world protocol modeling. The work lays groundwork for future optimizations, heuristic-guided proof strategies, and back-translation tools to bridge compiled proofs with source Tamgram models.

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.

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

TL;DR

Tamgram provides a high-level, modular frontend for the Tamarin prover, designed to address the scalability and maintainability challenges of large-scale security protocol specifications. It marries an ML-style module system, hygienic macros, and process-local memory to capture complex stateful interactions, while remaining faithful to Tamarin through a formal, trace-preserving translation. The authors develop a CFG-based intermediate representation and analyze multiple translation strategies, concluding that a hybrid forward/backward approach yields performance close to manually coded Tamarin models and improves readability. Empirical results on EMVerify and CSF18 XOR demonstrate practical viability and the potential for significant usability gains in real-world protocol modeling. The work lays groundwork for future optimizations, heuristic-guided proof strategies, and back-translation tools to bridge compiled proofs with source Tamgram models.

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.
Paper Structure (30 sections, 12 theorems, 71 equations, 15 figures)

This paper contains 30 sections, 12 theorems, 71 equations, 15 figures.

Table of Contents

  1. Introduction
  2. Our contributions
  3. Related work
  4. Background
  5. Overview of Tamarin
  6. Labeled operational semantics of Tamarin
  7. Problems in combining MSR rules and the applied-pi calculus
  8. Common modeling techniques and problems
  9. EMVerify
  10. WPA2
  11. Basic components of a Tamgram process
  12. Syntax
  13. Control flow graph representation
  14. Labeled operational semantics of Tamgram
  15. Revisiting EMVerify and WPA2 in Tamgram
  16. ...and 15 more sections

Key Result

Lemma 21

For any trace $\tau = S_0, tr(S_0, [k_0, \dots, k_n]) = S_0, k_0, S_1, \dots, S_n, k_n, S_{n+1}$, any cell $a$, if$a \not \in S_{n+1}$, then

Figures (15)

  • Figure 1: Example toy CFG.
  • Figure 2: Inference rules for the labeled transition relation of a Tamgram system.
  • Figure 3: Basic CFG.
  • Figure 4: CSF18 XOR benchmark summary (seconds)
  • Figure 5: EMVerify Contactless Mastercard CDA NoPIN Low benchmark (seconds)
  • ...and 10 more figures

Theorems & Definitions (52)

  • Definition 1
  • Definition 2
  • Definition 3
  • Example 4
  • Definition 5
  • Definition 6
  • Definition 7
  • Example 8
  • Definition 9
  • Definition 10
  • ...and 42 more