Visible to the public Biblio

Filters: Author is Ralf Sasse, Institute of Information Security, ETH  [Clear All Filters]
2015-11-18
Serdar Erbatur, Università degli Studi di Verona, Santiago Escobar, Universidad Politécnica de Valencia, Spain, Deepak Kapur, University of New Mexico, Zhiqiang Liu, Clarkson University, Christopher A. Lynch, Clarkson University, Catherine Meadows, Naval Research Laboratory, Jose Meseguer, University of Illinois at Urbana-Champaign, Paliath Narendran, University at Albany-SUNY, Sonia Santiago, Universidad Politécnica de Valencia, Spain, Ralf Sasse, Institute of Information Security, ETH.  2013.  Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis. 24th International Conference on Automated Deduction (CADE 2013) .

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 unifi- cation 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.