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, Ralf Sasse

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 s =? t 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.

Original languageEnglish (US)
Title of host publicationCADE 2013 - 24th International Conference on Automated Deduction, Proceedings
Number of pages18
StatePublished - 2013
Event24th International Conference on Automated Deduction, CADE 2013 - Lake Placid, NY, United States
Duration: Jun 9 2013Jun 14 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7898 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other24th International Conference on Automated Deduction, CADE 2013
Country/TerritoryUnited States
CityLake Placid, NY

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Asymmetric unification: A new unification paradigm for cryptographic protocol analysis'. Together they form a unique fingerprint.

Cite this