@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@inproceedings{ComDel-rta2005,
abstract = {We consider the following problem: Given a term
\(t\), a rewrite system \(\mathcal{R}\), a finite set
of equations \(E'\) such that \(\mathcal{R}\) is
convergent modulo~\(E'\), compute finitely many
instances of~\(t\): \(t_1,\ldots,t_n\) such that, for
every substitution~\(\sigma\), there is an index
\(i\) and a substitution~\(\theta\) such that \(
t\sigma\mathord{\downarrow}=_{E'} t_i\theta\) (where
\(t\sigma\mathord{\downarrow}\) is the normal form of
\(t\sigma\) w.r.t.~\(\mathcal{R}/E'\)). \par The goal
of this paper is to give equivalent (resp.
sufficient) conditions for the finite variant
property and to systematically investigate this
property for equational theories, which are relevant
to security protocols verification. For instance, we
prove that the finite variant property holds for
Abelian Groups, and a theory of modular
exponentiation and does not hold for the
theory~\textit{ACUNh} (Associativity, Commutativity,
Unit, Nilpotence, homomorphism).},
address = {Nara, Japan},
author = {Comon{-}Lundh, Hubert and Delaune, St{\'e}phanie},
booktitle = {{P}roceedings of the 16th {I}nternational
{C}onference on {R}ewriting {T}echniques and
{A}pplications ({RTA}'05)},
OPTDOI = {10.1007/b135673},
editor = {Giesl, J{\"u}rgen},
month = apr,
pages = {294-307},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {The finite variant property: {H}ow to get rid of some
algebraic properties},
volume = {3467},
year = {2005},
acceptrate = {31/79},
acronym = {{RTA}'05},
nmonth = {4},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}