BTW, has CryptoVerif been proven sound? I.e. has it been shown that the game transformations CryptoVerif produces really only amount to negligible probability transformations?
[1] https://prosecco.gforge.inria.fr/personal/bblanche/publicati...
Interestingly, that paper uses a variant of pi-calculus, i.e. an idealised programming language for message passing, as 'games'.