Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis^{* **}

Serdar Erbatur¹, Santiago Escobar³, Deepak Kapur⁴, Zhiqiang Liu⁵, Christopher A. Lynch⁵, Catherine Meadows⁶, José Meseguer⁷, Paliath Narendran², Sonia Santiago³, and Ralf Sasse⁸

¹Università degli Studi di Verona, Italy
serdar.erbatur@gmail.com

²University at Albany-SUNY, Albany, NY, USA
dran@cs.albany.edu

³DSIC-ELP, Universitat Politècnica de València, Spain
sescobar@dsic.upv.es
ssantiago@dsic.upv.es

⁴University of New Mexico, Albuquerque, NM, USA
kapur@cs.unm.edu

⁵Clarkson University, Potsdam, NY, USA
liuzh@clarkson.edu
clynch@clarkson.edu

⁶Naval Research Laboratory, Washington, DC, USA
meadows@itd.nrl.navy.mil

⁷University of Illinois, Urbana-Champaign, USA
meseguer@illinois.edu

⁸Institute of Information Security, ETH Zurich, Switzerland
ralf.sasse@inf.ethz.ch

Abstract. We present a new paradigm for unification arising out of a technique commonly used in cryptographic protocol analysis tools that employ unification modulo equational theories. This paradigm relies on: (i) a decomposition of an equational theory into (R,E) where R is confluent, terminating, and coherent modulo E, and (ii) on reducing unification problems to a set of problems under the constraint that t remains R/E-irreducible. We call this method asymmetric unification. We first present a general-purpose generic asymmetric unification algorithm. and then outline an approach for converting special-purpose conventional unification algorithms to asymmetric ones, demonstrating it for exclusive-or with uninterpreted function symbols. We demonstrate how asymmetric unification can improve performanceby running the algorithm on a set of benchmark problems. We also give results on the complexity and decidability of asymmetric unification.

^*S. Escobar and S. Santiago were partially supported by EU (FEDER) and the Spanish MEC/MICINN under grant TIN 2010-21062-C02-02, and by Generalitat Valenciana PROMETEO2011/052. The following authors were partially supported by NSF: S. Escobar, J. Meseguer, and R. Sasse under CNS 09-04749 and CCF 09-05584; D. Kapur under CNS 09-05222; C. Lynch, Z. Liu, and C. Meadows under CNS 09-05378, and P. Narendran and S. Erbatur under CNS 09-05286. Part of the S. Erbatur’s work was supported while with the Department of Computer Science, University at Albany, and part of R. Sasse’s work was supported while with the Department of Computer Science, University of Illinois at Urbana-Champaign. Portions of this paper appeared in an abstract in the informal proceedings of UNIF’11.

^**One of the authors is an employee of the US government, and the rights of this work are transferred to the extent transferable according to title 17 U.S.C. 105.

LNAI 7898, p. 231 ff.

Full article in PDF | BibTeX

lncs@springer.com
© Springer-Verlag Berlin Heidelberg 2013