Two distinct views of cryptography have been developed over the years, in two mostly separate communities, Formal Methods and Computational/Probabilistic Communities. The relation between these two approaches was previously explored in a paper by Abadi and Rogaway in 2000 where they proved the computational soundness of formal encryption with respect to a special type of cryptosystems. We present expansions of the Abadi-Rogaway logic and establish their soundness and completeness for a variety of interpretations. Two such interpretations are discussed in detail: a purely probabilistic one that interprets formal expressions in the One-Time Pad cryptosystem, and another one in the so-called type-2 (which-key revealing) cryptosystems based on computational complexity.