In game-based cryptographic proofs, the security of cryptographic algorithms is reduced to problems which are assumed to be hard (e.g. the DDH). This requires reasoning about and transforming probabilistic programs. In this presentation a probabilistic Hoare-style logic is given and it is shown how this logic can be used in formalizing cryptographic proofs. This technique is illustrated by proving semantic security of ElGamal. Joint work with Ricardo Corin.