In this paper we study abstraction techniques for verification problems of the form C ⊨ ϕ, where C is a first-order structure and ϕ is a first-order formula (both w.r.t. a given signature ∑). This study is motivated by the need of such abstractions for the automatic verification of properties of cryptographic protocols, which in our approach are modeled by first-order structures. Our so-called algebraic abstractions will be correct by construction and optimal in some certain technical sense. Moreover, we provide guidelines to design specific algebraic abstractions suited for verification problems corresponding to cryptographic protocols.