Unification modulo homomorphic encryption

Encryption 'distributing over pairs' is a techni'ue employed in several cryptographic protocols. We show that unification is decidable for an e'uational theory HE specifying such an encryption. The method consists in transforming any given problem in such a way, that the resulting problem can be solved by combining a graph-based reasoning on its e'uations involving the homomorphisms, with a syntactic reasoning on its pairings. We show HE-unification to be NP-hard and in EXPTIME. We also indicate, briefly, how to extend HE-unification to Cap unification modulo HE, that can be used as a tool for modeling and analyzing cryptographic protocols where encryption follows the ECB mode, i.e., is done blockwise on messages.