Symmetric authentication in a simulatable Dolev–Yao-style cryptographic library

Tool-supported proofs of security protocols typically rely on abstractions from real cryptography by term algebras, so-called Dolev---Yao models. However, until recently it was not known whether a Dolev---Yao model could be implemented with real cryptography in a provably secure way under active attacks. For public-key encryption and signatures, this was recently shown, if one accepts a few additions to a typical Dolev---Yao model such as an operation that returns the length of a term. Here we extend this Dolev---Yao-style model, its realization, and the security proof to include a first symmetric primitive message authentication. This adds a major complication: we must deal with the exchange of secret keys. For symmetric authentication, we can allow this at any time, before or after the keys are first used for authentication, while working only with standard cryptographic assumptions.