Skip navigation
Please use this identifier to cite or link to this item: http://repositorio.unb.br/handle/10482/4605
Files in This Item:
File Description SizeFormat 
2009_DanieleNantesSobrinho.pdf440,53 kBAdobe PDFView/Open
Title: O problema da dedução do intruso para um protocolo criptográfico especificado via reescrita módulo AC
Authors: Nantes Sobrinho, Daniele
Orientador(es):: Ayala-Rincón, Mauricio
Assunto:: Redes de computação - protocolos
Criptografia de dados (Computação)
Computadores - medidas de segurança
Matemática aplicada
Issue Date: 2009
Citation: NANTES SOBRINHO, Daniele. O problema da dedução do intruso para um protocolo criptográfico especificado via reescrita módulo AC. 2009. 94 f. Dissertação (Mestrado em Matemática)-Universidade de Brasília, Brasília, 2009.
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.
Description: Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Matemática, 2009.
Appears in Collections:MAT - Mestrado em Matemática (Dissertações)

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



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