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

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 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
Pages231-248
Number of pages18
DOIs
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

Other

Other24th International Conference on Automated Deduction, CADE 2013
CountryUnited States
CityLake Placid, NY
Period6/9/136/14/13

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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

  • Cite this

    Erbatur, S., Escobar, S., Kapur, D., Liu, Z., Lynch, C. A., Meadows, C., Meseguer, J., Narendran, P., Santiago, S., & Sasse, R. (2013). Asymmetric unification: A new unification paradigm for cryptographic protocol analysis. In CADE 2013 - 24th International Conference on Automated Deduction, Proceedings (pp. 231-248). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7898 LNAI). https://doi.org/10.1007/978-3-642-38574-2_16