In previous sections, we examined the foundations of modeling security protocols and how Tamarin reasons about these models. We now turn to tradeoffs in modeling, that is choosing between different options when modeling protocols or formalizing their properties. We also consider some pitfalls that newcomers to Tamarin should avoid. We note in this regard that there is often no one, specific, best modeling approach. However, there are certain standard patterns that have proven useful in practice, which we present in this section.