We now present a large case study where we use many of the previously introduced features to model a complex real-world protocol. We chose the next generation mobile communication key agreement protocol 5G-AKA as our example. The following account is based on our published paper [14], co-authored by Basin, Dreier, Hirschi, Radomirović, Sasse, and Stettler. Here we focus on the modeling decisions taken for the core of the protocol, and how we wrote the Tamarin model for it. Along the way, we showcase this with Tamarin code, exemplifying many of the features previously introduced in this book. For interested readers, we refer to the above paper for the presentation of the standard and how the core of the protocol was extracted from the standard, as well as a comprehensive account of the protocol’s properties.