O problema da dedução do intruso para teorias AC-convergentes localmente estáveis

Abstract

Apresenta-se um algoritmo para decidir o problema da dedução do intruso (PDI) para a classe de teorias localmente estáveis normais, que incluem operadores associativos e comutativos (AC). A decidibilidade é baseada na análise de reduções de reescrita aplicadas na cabeça de termos que são construídos a partir de contextos normais e o conhecimento inicial de um intruso. Este algoritmo se baseia em um algoritmo eficiente para resolver um caso restrito de casamento módulo AC de ordem superior, obtido pela combinação de um algoritmo para Casamento AC com Ocorrências Distintas, e um algoritmo padrão para resolver sistemas de equações Diofantinas lineares. O algoritmo roda em tempo polinomial no tamanho de um conjunto saturado construído a partir do conhecimento inicial do intruso para a subclasse de teorias para a qual operadores AC possuem inversos. Os resultados são aplicados para teoria AC pura e a teoria de grupos Abelianos de ordem n dada. Uma tradução entre dedução natural e o cálculo de sequentes permite usar a mesma abordagem para decidir o problema da dedução elementar para teorias localmente estáveis com inversos. Como uma aplicação, a teoria de assinaturas cegas pode ser modelada e então, deriva-se um algoritmo para decidir o PDI neste contexto, estendendo resultados de decidibilidade prévios. ______________________________________________________________________________ ABSTRACT

We present an algorithm to decide the intruder deduction problem (IDP) for the class of normal locally stable theories, which include associative and commutative (AC) opera- tors. The decidability is based on the analysis of rewriting reductions applied in the head of terms built from normal contexts and the initial knowledge of the intruder. It relies on a new and efficient algorithm to solve a restricted case of higher-order AC-matching, obtained by combining the Distinct Occurrences of AC-matching algorithm and a stan- dard algorithm to solve systems of linear Diophantine equations. Our algorithm runs in polynomial time on the size of a saturation set built from the initial knowledge of the intruder for the subclass of theories for which AC operators have inverses. We apply the results to the Pure AC equational theory and Abelian Groups with a given order n. A translation between natural deduction and sequent calculus allows us to use the same approach to decide the elementary deduction problem for locally stable theories with inverses. As an application, we model the theory of blind signatures and derive an algorithm to decide IDP in this context, extending previous decidability results.