In the symbolic model of cryptography, and in the examples we have seen until now in this book (notably in Chapter 7 ), there was exactly one symbolic model for each type of cryptographic primitive, such as symmetric encryption or signing. Most of these models originated in the early days of model checking for security protocols, and have been the de-facto standard for decades. Around 2019, due to advances in Tamarin’s support for equational reasoning, property specification, and restrictions, it became feasible to reconsider the precision of these models and develop more fine-grained symbolic models for primitives such as signatures [74], Diffie-Hellman [47], Hash functions [33], Authenticated Encryption [31], and Key Encapsulation Mechanisms [39].