Effectively Checking or Disproving the Finite Variant Property

Escobar, Santiago; Meseguer, José; Sasse, Ralf

Permalink

https://hdl.handle.net/2142/11451 Copy

Description

Title

Effectively Checking or Disproving the Finite Variant Property

Author(s)

• Escobar, Santiago
• Meseguer, José
• Sasse, Ralf

Issue Date

2008-04

Keyword(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.

Type of Resource

text

Permalink

http://hdl.handle.net/2142/11451

Copyright and License 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).

Owning Collections