Intruder deduction problem for locally stable theories with normal forms and inverses

Mauricio Ayala-Rincón; Maribel Fernández; Daniele Nantes-Sobrinho

doi:10.1016/j.tcs.2017.01.027

Intruder deduction problem for locally stable theories with normal forms and inverses

Mauricio Ayala-Rincón
, Maribel Fernández
, Daniele Nantes-Sobrinho

Research output: Contribution to journal › Article › peer-review

7 Citations (Scopus)

235 Downloads (Pure)

Abstract

We present an algorithm to decide the intruder deduction problem (IDP) for a class of equational theories that include associative and commutative (AC) operators. The algorithm is based on the analysis of reductions in the head of terms built from normal contexts using the initial knowledge of the intruder. It relies on a new and efficient algorithm to solve a restricted case of higher-order AC-matching. For the subclass of theories for which AC operators have inverses, our algorithm runs in polynomial time on the size of a saturated set built from the initial knowledge of the intruder. To illustrate, we apply the results to Pure AC theories, Abelian Groups, Abelian Groups extended with exponentiation, and XOR. Although specific algorithms have already been defined to deal with each of these theories, we provide a modular approach that can deal with all of them in a uniform way.

Original language	English
Article number	TCS-D-14-00678R4
Pages (from-to)	64-100
Journal	Theoretical Computer Science
Volume	672
Early online date	24 Feb 2017
DOIs	https://doi.org/10.1016/j.tcs.2017.01.027
Publication status	Published - 11 Apr 2017

Keywords

Intruder deduction problem
Associativity and commutativity
Locally stable theories
Term rewrite systems
AC-matching

Access to Document

10.1016/j.tcs.2017.01.027

Intruder deduction for locally stable_AYALA-RINCON_Firstonline24February2017_GREEN AAMAccepted author manuscript, 656 KBLicence: CC BY-NC-ND

Cite this

@article{ae64aacc3f5d49cf9674e5f36cf0247d,

title = "Intruder deduction problem for locally stable theories with normal forms and inverses",

abstract = "We present an algorithm to decide the intruder deduction problem (IDP) for a class of equational theories that include associative and commutative (AC) operators. The algorithm is based on the analysis of reductions in the head of terms built from normal contexts using the initial knowledge of the intruder. It relies on a new and efficient algorithm to solve a restricted case of higher-order AC-matching. For the subclass of theories for which AC operators have inverses, our algorithm runs in polynomial time on the size of a saturated set built from the initial knowledge of the intruder. To illustrate, we apply the results to Pure AC theories, Abelian Groups, Abelian Groups extended with exponentiation, and XOR. Although specific algorithms have already been defined to deal with each of these theories, we provide a modular approach that can deal with all of them in a uniform way.",

keywords = "Intruder deduction problem, Associativity and commutativity, Locally stable theories, Term rewrite systems, AC-matching",

author = "Mauricio Ayala-Rinc{\'o}n and Maribel Fern{\'a}ndez and Daniele Nantes-Sobrinho",

year = "2017",

month = apr,

day = "11",

doi = "10.1016/j.tcs.2017.01.027",

language = "English",

volume = "672",

pages = "64--100",

journal = "Theoretical Computer Science",

issn = "0304-3975",

publisher = "Elsevier BV",

}

TY - JOUR

T1 - Intruder deduction problem for locally stable theories with normal forms and inverses

AU - Ayala-Rincón, Mauricio

AU - Fernández, Maribel

AU - Nantes-Sobrinho, Daniele

PY - 2017/4/11

Y1 - 2017/4/11

N2 - We present an algorithm to decide the intruder deduction problem (IDP) for a class of equational theories that include associative and commutative (AC) operators. The algorithm is based on the analysis of reductions in the head of terms built from normal contexts using the initial knowledge of the intruder. It relies on a new and efficient algorithm to solve a restricted case of higher-order AC-matching. For the subclass of theories for which AC operators have inverses, our algorithm runs in polynomial time on the size of a saturated set built from the initial knowledge of the intruder. To illustrate, we apply the results to Pure AC theories, Abelian Groups, Abelian Groups extended with exponentiation, and XOR. Although specific algorithms have already been defined to deal with each of these theories, we provide a modular approach that can deal with all of them in a uniform way.

AB - We present an algorithm to decide the intruder deduction problem (IDP) for a class of equational theories that include associative and commutative (AC) operators. The algorithm is based on the analysis of reductions in the head of terms built from normal contexts using the initial knowledge of the intruder. It relies on a new and efficient algorithm to solve a restricted case of higher-order AC-matching. For the subclass of theories for which AC operators have inverses, our algorithm runs in polynomial time on the size of a saturated set built from the initial knowledge of the intruder. To illustrate, we apply the results to Pure AC theories, Abelian Groups, Abelian Groups extended with exponentiation, and XOR. Although specific algorithms have already been defined to deal with each of these theories, we provide a modular approach that can deal with all of them in a uniform way.

KW - Intruder deduction problem

KW - Associativity and commutativity

KW - Locally stable theories

KW - Term rewrite systems

KW - AC-matching

U2 - 10.1016/j.tcs.2017.01.027

DO - 10.1016/j.tcs.2017.01.027

M3 - Article

SN - 0304-3975

VL - 672

SP - 64

EP - 100

JO - Theoretical Computer Science

JF - Theoretical Computer Science

M1 - TCS-D-14-00678R4

ER -

Intruder deduction problem for locally stable theories with normal forms and inverses

Abstract

Keywords

Access to Document

Fingerprint

Cite this