Unification modulo Homomorphic Encryption

Siva Anantharaman 1 Hai Lin 2 Christopher Lynch 2 Paliath Narendran 3 Michael Rusinowitch 4
4 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Encryption 'distributing over pairs' is a technique employed in several cryptographic protocols. We show that unification is decidable for an equational 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 equations 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 block-wise on messages.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2012, 48 (2), pp.135-158. 〈10.1007/s10817-010-9205-y〉
Liste complète des métadonnées

Contributeur : Siva Anantharaman <>
Soumis le : jeudi 1 septembre 2011 - 14:40:37
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10

Lien texte intégral



Siva Anantharaman, Hai Lin, Christopher Lynch, Paliath Narendran, Michael Rusinowitch. Unification modulo Homomorphic Encryption. Journal of Automated Reasoning, Springer Verlag, 2012, 48 (2), pp.135-158. 〈10.1007/s10817-010-9205-y〉. 〈inria-00618336〉



Consultations de la notice