“Games” are a ...

I think the terminology of games is a bit misleading. A better term would be program but in a (probabilistic) programming language that specifies interaction by message passing (such as process calculi).

CryptoVerif outputs what might be seen as program transformations:

   P = Q

such that the probability that a polynomially bounded adversary can 'crack' P is only negligibly different from the probability for Q. This can be seen as a probabilistic generalisation of e.g. the program transformations that an optimising compiler does, except that in compilation you need that P and Q have exactly the same (observable) behaviour.

Verifying crypto protocols is essentially the production of a chain

   P1 = P2 = ... = Pn

where P1 is the protocol in question, and Pn is some "obviously secure" protocol (e.g. existence of one-way functions). Note that Pn might be doing something different from P1. What's important is that the probabilities remain 'similar' (this can be made precise). This proves that P1 is as secure as Pn, so we can break the latter if we can break the former.

The reason for the "game" terminology is historical. Von Neumann's theory of economic games [1] preceeds the development of programming languages for interactive behaviour [2] by many decades.

[1] https://en.wikipedia.org/wiki/Theory_of_Games_and_Economic_B...

[2] https://en.wikipedia.org/wiki/Process_calculus