There are two main frameworks for analyzing cryptographic systems; the symbolic frame-work, originating from the work of Dolev and Yao, and the computational approach, growing out of the work of Goldwasser and Micali. A significant amount of effort has been made in order to link both approaches and profit from the advantages of each of them. Indeed, while the symbolic approach is more amenable to automated proof methods, the computation approach can be more realistic. Abadi and Rogaway were the first to prove a formal link between these two models. More precisely, they introduced an equivalence relation on terms and prove that equivalent terms correspond to indistinguishable distributions ensembles, when interpreted in the computational model. The work of Abadi and Rogaway has been extended to active adversaries and various cryptographic primitives. Related works. A recently emerging branch of relating symbolic and computational mod-els for passive adversaries is based on static equivalence from π-calculus, induced by an equa-tional theory. Equational theories provide a framework to specify algebraic properties of the underlying signature, and hence, symbolic computations in a similar way as for abstract data types. That is, for a fixed equational theory, a term describes a computation in the symbolic model. Thus, an adversary can distinguish two frames (which roughly speaking are tuples of terms), if he is able to come up with two computations that yield the same result when applied to one frame, but different results when applied to the other frame. Such a pair of terms is called a test. Thus, a static equivalence relation is fully determined by the underlying equational theory, as two frames are statically equivalent, if there is no test that separates them. Baudet, Cortier and Kremer studied soundness and faithfulness of static equivalence for general equa-tional theories and used their framework to prove soundness of exclusive or as well as certain symmetric encryptions.