Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Matemática, 2009. / Submitted by Allan Wanick Motta (allan_wanick@hotmail.com) on 2010-03-10T17:47:59Z
No. of bitstreams: 1
2009_DanieleNantesSobrinho.pdf: 451105 bytes, checksum: 5dacc5d725d520ef70f60e8bb44d4ede (MD5) / Approved for entry into archive by Daniel Ribeiro(daniel@bce.unb.br) on 2010-05-13T20:19:47Z (GMT) No. of bitstreams: 1
2009_DanieleNantesSobrinho.pdf: 451105 bytes, checksum: 5dacc5d725d520ef70f60e8bb44d4ede (MD5) / Made available in DSpace on 2010-05-13T20:19:47Z (GMT). No. of bitstreams: 1
2009_DanieleNantesSobrinho.pdf: 451105 bytes, checksum: 5dacc5d725d520ef70f60e8bb44d4ede (MD5)
Previous issue date: 2009 / 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.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.unb.br:10482/4605 |
| Date | January 2009 |
| Creators | Nantes Sobrinho, Daniele |
| Contributors | Ayala-Rincón, Mauricio |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Source | reponame:Repositório Institucional da UnB, instname:Universidade de Brasília, instacron:UNB |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0019 seconds