AutoTam: Specifying Secure Protocol Implementations with Tamarin Model Generation

Computer Science > Cryptography and Security [Submitted on 18 Jun 2026] AutoTam: Specifying Secure Protocol Implementations with Tamarin Model Generation Johannes Wilson, Mikael Asplund, Niklas Johansson Formal verification is a challenging but important task for ensuring the security of cryptographic protocols. While modern protocol verification tools significantly reduce verification effort, modelling remains challenging to practitioners without a background in formal verification. In addition, transferring verification results to a concrete protocol implementation requires expert knowledge. In this paper, we present a novel language-first method for verification of trace properties using a domain-specific language for protocol implementations. We target the Tamarin prover for verification, and we prove that verified universal trace properties translate back to the implementation. We additionally integrate symbolic execution in order to analyse the memory safety of protocol implementations. We use our tool to implement and generate accurate models for a signed Diffie-Hellman protocol, and for the WireGuard VPN protocol. Our WireGuard implementation is interoperable with existing implementations when using our interpreter, and achieves acceptable performance. We formally prove our implementations secure using a combination of symbolic execution and verification of the generated Tamarin models. Comments: 19 pages, 5 figures Subjects: Cryptography and Security (cs.CR) Cite as: arXiv:2606.19937 [cs.CR]   (or arXiv:2606.19937v1 [cs.CR] for this version)   https://doi.org/10.48550/arXiv.2606.19937 Focus to learn more Submission history From: Johannes Wilson [view email] [v1] Thu, 18 Jun 2026 08:34:17 UTC (220 KB) Access Paper: HTML (experimental) view license Current browse context: cs.CR < prev   |   next > new | recent | 2026-06 Change to browse by: cs References & Citations NASA ADS Google Scholar Semantic Scholar Export BibTeX Citation Bookmark Bibliographic Tools Bibliographic and Citation Tools Bibliographic Explorer Toggle Bibliographic Explorer (What is the Explorer?) Connected Papers Toggle Connected Papers (What is Connected Papers?) Litmaps Toggle Litmaps (What is Litmaps?) scite.ai Toggle scite Smart Citations (What are Smart Citations?) Code, Data, Media Demos Related Papers About arXivLabs Which authors of this paper are endorsers? | Disable MathJax (What is MathJax?)