2024/08/23 by Di Long Li, Li, Di Long, Jim de Groot +3
Computer Science · #Algorithms and Data Compression #Cryptography and Security (cs.CR) #FOS: Computer and information sciences #Natural Language Processing Techniques #Network Packet Processing and Optimization
paper · pdf · doi:10.48550/arxiv.2408.13138
openalex publication_date 2024/08/23 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.