Skip navigation
Please use this identifier to cite or link to this item: http://repositorio.unb.br/handle/10482/14781
Files in This Item:
File Description SizeFormat 
2013_DanieleNantesSobrinho.pdf855,6 kBAdobe PDFView/Open
Title: O problema da dedução do intruso para teorias AC-convergentes localmente estáveis
Authors: Nantes Sobrinho, Daniele
Orientador(es):: Ayala-Rincón, Mauricio
Coorientador(es):: Fernández, Maribel
Assunto:: Criptografia de dados (Computação)
Redes de computação - protocolos
Computadores - medidas de segurança
Issue Date: 9-Dec-2013
Citation: NANTES SOBRINHO, Daniele. O problema da dedução do intruso para teorias AC-convergentes localmente estáveis. 2013. 101 f. Tese (Doutorado em Matemática)—Universidade de Brasília, Brasília, 2013.
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.
Description: Tese (doutorado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Matemática, 2013.
Licença:: A concessão da licença deste item refere-se ao termo de autorização impresso assinado pelo autor com as seguintes condições: Na qualidade de titular dos direitos de autor da publicação, autorizo a Universidade de Brasília e o IBICT a disponibilizar por meio dos sites www.bce.unb.br, www.ibict.br, http://hercules.vtls.com/cgi-bin/ndltd/chameleon?lng=pt&skin=ndltd sem ressarcimento dos direitos autorais, de acordo com a Lei nº 9610/98, o texto integral da obra disponibilizada, conforme permissões assinaladas, para fins de leitura, impressão e/ou download, a título de divulgação da produção científica brasileira, a partir desta data.
Appears in Collections:MAT - Doutorado em Matemática (Teses)

Show full item record Recommend this item " class="statisticsLink btn btn-primary" href="/handle/10482/14781/statistics">



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.