Secure protocol design is tricky – to say the least. There are seemingly unlimited possibilities for a motivated attacker to ruin your day: by forging messages, replaying packet captures, or interleaving sessions. The same, of course, is true for the cryptographic algorithms themselves which underlie these protocols. Thankfully, cryptographers have an exciting solution to such challenges: formal methods. In a perfect world, all protocols would be subject to the same rigorous approach, currently found in few places outside academia and avionics. But if yours isn’t, you can probably be forgiven (assuming you don’t have a postgraduate degree, three months of spare time, and a pathological devotion to pedantry). Even so, certain formal techniques do lend themselves particularly well to practical protocol analysis by engineers and defenders of all stripes. In this talk, we will give a whirlwind introduction to formal methods for security protocols. Our focus will be on those aspects which you can apply day to day, for example, to nail down a concrete threat model and challenge your trust assumptions. And we’ll show how our back-of-the-napkin approach can be used to discover flaws in a real-world protocol. All without giving a single mathematical proof (probably).