AutoTam: Specifying Secure Protocol Implementations with Tamarin Model Generation
For developers without formal verification expertise, this work reduces the gap between protocol implementation and verification by automating model generation and ensuring security properties translate to code.
The paper presents a language-first method for verifying trace properties of cryptographic protocol implementations using a domain-specific language that generates Tamarin models. The approach is applied to a signed Diffie-Hellman protocol and WireGuard, achieving interoperability and acceptable performance while formally proving security.
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.