Tamarin’s standard usage is to analyze the design of a given security protocol or perhaps accompany the evolution of that design, checking the protocol after each modification. But Tamarin can also be used to compare protocols and even analyze families of related protocols. This can be used to determine the differences in the protocols’ strengths with respect to the properties they meet, the adversaries they resist, or even where in the protocol run particular properties are established. Such an analysis supports protocol implementers in choosing the protocol variant that best matches the guarantees they need for their specific use case. For example, for resource-constrained devices one might be willing to sacrifice some security guarantees for less computation or communication. Alternatively one might trade off privacy for security or vice versa.