We show how the Tamarin tool can be used to model and reason about security protocols using identity-based cryptography, in- cluding identity-based encryption and signatures. Although such proto- cols involve rather different primitives than conventional public-key cryp- tography, we illustrate how suitable abstractions and Tamarin’s support for equational theories can be used to model and analyze realistic indus- try protocols, either finding flaws or gaining confidence in their security with respect to different classes of adversaries. Technically, we propose two models of identity-based cryptography. First, we formalize an abstract model, based on simple equations, in which verification of realistic protocols is feasible. Second, we formalize a more precise model, leveraging Tamarin’s support for bilinear pairing and exclusive-or. This model is much closer to practical realizations of identity- based cryptography, but deduction is substantially more complex. Along the way, we point out the limits of precise modeling and highlight chal- lenges in providing support for equational reasoning. We also evaluate our models on an industrial protocol where we find and fix flaws.