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 NEXPTIME.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Anantharaman, S., Narendran, P., Rusinowitch, M.: Intruders with Caps. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 20–35. Springer, Heidelberg (2007)
Anantharaman, S., Lin, H., Lynch, C., Narendran, P., Rusinowitch, M.: Equational and Cap Unification for Intrusion Analysis. LIFO-Research Report, http://www.univ-orleans.fr/lifo/prodsci/rapports/RR/RR2008/RR-2008-03.pdf
Baudet, M.: Deciding security of protocols against off-line guessing attacks. In: Proc. of ACM Conf. on Computer and Communications Security, pp. 16–25 (2005)
Comon-Lundh, H., Shmatikov, V.: Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive-Or. In: Proc. of the Logic In Computer Science Conference, LICS 2003, pp. 271–280 (2003)
Cortier, V., Delaune, S., Lafourcade, P.: A Survey of Algebraic Properties Used in Cryptographic Protocols. Journal of Computer Security 14(1), 1–43 (2006)
Cortier, V., Rusinowitch, M., Zalinescu, E.: A resolution strategy for verifying cryptographic protocols with CBC encryption and blind signatures. In: Proc. of the 7th ACM SIGPLAN Symposium PPDP 2005, pp. 12–22 (2005)
Delaune, S., Jacquemard, F.: A decision procedure for the verification of security protocols with explicit destructors. In: Proc. of the 11th ACM Conference on Computer and Communications Security (CCS’04), Washington, D.C., USA, pp. 278–287. ACM Press, New York (2004)
Fujioka, A., Okamoto, T., Kazuo, O.: A Practical Secret Voting Scheme for Large Scale Elections. In: Zheng, Y., Seberry, J. (eds.) AUSCRYPT 1992. LNCS, vol. 718, pp. 244–251. Springer, Heidelberg (1993)
Lafourcade, P., Lugiez, D., Treinen, R.: Intruder deduction for the equational theory of Abelian groups with distributive encryption. Inf. Comput. 205(4), 581–623 (2007)
Narendran, P., Pfenning, F., Statman, R.: On the unification problem for Cartesian Closed Categories. In: Proc. of the Logic in Computer Science Conference LICS 1993, pp. 57–63 (1993)
Schaefer, T.J.: The complexity of satisfiability problems. In: Proc. of the 10th Annual ACM Symposium on Theory of Computing, pp. 216–226 (1978)
Tiden, E., Arnborg, S.: Unification Problems with One-sided Distributivity. Journal of Symbolic Computation 3(1-2), 183–202 (1987)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Anantharaman, S., Lin, H., Lynch, C., Narendran, P., Rusinowitch, M. (2009). Unification Modulo Homomorphic Encryption. In: Ghilardi, S., Sebastiani, R. (eds) Frontiers of Combining Systems. FroCoS 2009. Lecture Notes in Computer Science(), vol 5749. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04222-5_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-04222-5_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04221-8
Online ISBN: 978-3-642-04222-5
eBook Packages: Computer ScienceComputer Science (R0)