The computational soundness of formal indistinguishability and static equivalence

1 Introduction In the past few years, significant effort has been made to link formal and compu-tational methods of cryptography. These directions had largely been developing independently; the first based on the seminal work of Dolev and Yao [15], and thesecond growing out of the work of Goldwasser and Micali [16]. While the computational method gives a more realistic and detailed description of an actualprotocol, using probability theory and taking limited computational power into account, security proofs in this model are done by hand and are often notoriouslyhard to verify. The formal method is a high-level treatment, amenable to automatization,but its reliability is sometimes questionable; namely, a protocol that is formally secure may not be so computationally, and, therefore, may be insecure in reality.It is therefore important how to translate one model into the other, and to characterize which security proofs in the simpler formal framework carry over tothe computational setting