O problema da dedução do intruso para um protocolo criptográfico especificado via reescrita módulo AC

Abstract

O ponto inicial deste trabalho é um caso de estudo de um protocolo de carteira eletrônica modelado por uma teoria equacional de um fragmento da aritmética, que inclui exponenciação. Foi estudado um procedimento de decisão para o problema da dedução do intruso, proposto recentemente por Bursuc, Comon-Lundh e Delaune. O intruso tem as mesmas capacidades algébricas de dedução que a teoria equacional que modela o protocolo. Associa-se a essa teoria equacional um sistema de reescrita equivalente, que é convergente módulo associatividade e comutatividade. Formula-se a capacidade de dedução do intruso através de um sistema de regras de inferência. Além de mostrar que o problema em questão pode ser decidido em tempo limitado polinomialmente, será mostrado que esse sistema de dedução tem uma propriedade de localidade e que a deducibilidade em um passo é decidida em tempo limitado polinomialmente ______________________________________________________________________________________ ABSTRACT

The starting point of this work is a case study of an electronic purse protocol modeled by an equational theory of a fragment of arithmetic including exponentiation. A decision procedure for the intruder deduction problem was studied, which was proposed recently by Bursuc, Comon-Lundh and Delaune. The intruder algebraic deduction capabilities are the same as the ones of the equational theory that model the protocol. This equational theory is associated with an equivalent term rewriting system which is convergent modulo associativity and commutativity. The intruder deduction capabilities are formalized by a system of inference rules. In order to show that this problem can be decided in polynomial time, it is proved that this deduction system has a locality property and that the one-step deducibility property is decidable in polynomial time.