Symbolic models for security are built around axioms that reflect appealing intuition regarding the security of basic primitives. The resulting adversaries however often seem unrealistically strong in some of their abilities and not sufficiently powerful in others. An interesting research direction pioneered by Abadi and Rogaway is to show that despite these apparent limitations symbolic models can be used to obtain results that are meaningful with respect to the more detailed and realistic models used in computational cryptography. This line of research is now known as computational soundness. This chapter describes in detail a computational soundness result that extends the original work of Abadi and Rogaway. We show that it is possible to reason about computational indistinguishability of distributions obtained by using symmetric encryption and exponentiation in finite groups with entirely symbolic methods. The result relies on standard notions of security for the encryption scheme and on a powerful generalization of the Diffie-Hellman assumption.