Variants of Variants and the Finite Variant Property

Cholewa, Andrew; Meseguer, José; Escobar, Santiago

Permalink

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

Description

Title

Variants of Variants and the Finite Variant Property

Author(s)

• Cholewa, Andrew
• Meseguer, José
• Escobar, Santiago

Issue Date

2014-02-11

Keyword(s)

• variants
• finite variant property
• rewriting
• equational rewriting
• equational theories

Abstract

Variants and the finite variant property were originally introduced about a decade ago by Hurbert Comon-Lundh and Stephanie Delaune to reason about equational theories that commonly appear in cryptographic protocol analysis. Since that time, two additional notions of variants have been developed: one by Santiago Escobar, Jose Meseguer, and Ralf Sasse, and one by Stefan Ciobaca. Though it seems intuitively clear that all three notions capture the same essential idea, their relationships to each other have never been rigorously analyzed. Therefore, we decided to do just that. In the process, we encountered an unexpected subtlety with respect to the finite variant property, the term signature of a theory, and the boundedness property. We also provide a simple semi-decision procedure for checking if an equational theory has the finite variant property, by analzying terms of the form f (x 1 : s 1 , . . . , x n : s n ) for all function symbols f : s 1 , . . . , s n → s in the signature, where x 1 , . . . , x n are distinct variables.

Type of Resource

text

Language

en

Permalink

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

Sponsor(s)/Grant Number(s)

• NSF Grant CCF 09-05584
• NSF Grant CNS 13-19109

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