I will describe how games (especially, but not exclusively, model-checking games) can be used in the verification of protocols which have an unbounded number of participants and/or which involve data from an infinite set. To solve such a problem one needs a sound abstraction; that is, one which retains all information which is important to the problem. I will give examples to show how the notion of abstract game provides a conceptually clean (and potentially efficient) way to generate sound abstractions automatically.