Files in this item



application/pdfEffectively Che ... inite Variant Property.pdf (468kB)
(no description provided)PDF


Title:Effectively Checking or Disproving the Finite Variant Property
Author(s):Escobar, Santiago; Meseguer, José; Sasse, Ralf
Subject(s):computer science
Abstract:An equational theory decomposed into a set B of equational axioms and a set \Delta of rewrite rules has the \emph{finite variant} (FV) \emph{property} in the sense of Comon-Lundh and Delaune iff for each term t there is a finite set \{t_{1},\ldots,t_{n}\} of \rightarrow_{\Delta,B}-normalized instances of t so that any instance of t normalizes to an instance of some t_{i} modulo B. This is a very useful property for cryptographic protocol analysis, and for solving both unification and disunification problems. Yet, at present the property has to be established by hand, giving a separate mathematical proof for each given theory: no checking algorithms seem to be known. In this paper we give both a necessary and a sufficient condition for FV from which we derive, both an algorithm ensuring the sufficient condition, and thus FV, and another disproving the necessary condition, and thus disproving FV. These algorithms can check automatically a number of examples and counterexamples of FV known in the literature.
Issue Date:2008-04
Genre:Technical Report
Other Identifier(s):UIUCDCS-R-2008-2960
Rights Information:You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).
Date Available in IDEALS:2009-04-22

This item appears in the following Collection(s)

Item Statistics