Submitted by Maria Cristina (library@lncc.br) on 2017-08-10T18:19:02Z
No. of bitstreams: 1
dissertacao Natasha.pdf: 915040 bytes, checksum: 8e2b079465523b98d5e66edeb28a679c (MD5) / Approved for entry into archive by Maria Cristina (library@lncc.br) on 2017-08-10T18:19:15Z (GMT) No. of bitstreams: 1
dissertacao Natasha.pdf: 915040 bytes, checksum: 8e2b079465523b98d5e66edeb28a679c (MD5) / Made available in DSpace on 2017-08-10T18:19:25Z (GMT). No. of bitstreams: 1
dissertacao Natasha.pdf: 915040 bytes, checksum: 8e2b079465523b98d5e66edeb28a679c (MD5)
Previous issue date: 2017-02-17 / Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq) / Nowadays, besides the growing popularity of cryptography, there is a big interest from
researchers in the development of strategies that study and analyze the current crypto-
graphic methods. This is due to the fact that current methods are based on mathematical
problems considered safe, however, researchs points to security flaws in the presence of a
quantum computer.
In this work we created and developed a method capable of translating symmetric cryp-
tographic algorithms into Conjunctive Normal Form and then we analyze the obtained
output. Initially, we studied the cryptographic algorithm model of interest and used the
software CBMC, a bounded model checker software. This software returns a SAT system
to be solved, i.e, we rewrite the problem as SAT. In addition, the system can be interpreted
as a graph, so we reduce it by implementing a depth-first-search before solving it, to make
the problem feasible for resolution. The method proposed is then submitted to a round of
tests, aiming to validate the developed tool. / Atualmente, além da popularidade da criptografia estar crescendo consideravelmente, existe grande interesse em realizar pesquisas para o desenvolvimento de estratégias que estudem e analisem os métodos criptográficos utilizados atualmente. Isto se dá pelo fato dos métodos atuais serem baseados em problemas matemáticos considerados seguros, entretanto, pesquisas atuais apontam para falhas de segurança na presença de um computador quântico.
Este trabalho consiste em traduzir os algoritmos criptográficos simétricos para o sistema SAT e analisar a saída obtida. Para isto, inicialmente estudamos o modelo do algoritmo criptográfico de interesse e inserimos ele em um software verificador de modelos (CBMC).
Este software nos retorna um sistema SAT a ser resolvido, ou seja, reescrevemos o problema como SAT. Além disto, o sistema pode ser interpretado como um grafo, então reduzimos o mesmo através de uma busca em profundidade antes de resolvê-lo, para tornar o problema factível de resolução. A técnica proposta é submetida a um conjunto de testes, utilizando meios propostos pela literatura e alguns meios originais do trabalho, para validar a ferramenta desenvolvida.
| Identifer | oai:union.ndltd.org:IBICT/oai:tede-server.lncc.br:tede/266 |
| Date | 17 February 2017 |
| Creators | Paiva, Natasha do Nascimento |
| Contributors | Portugal, Renato, Lara, Pedro Carlos da Silva, Portugal, Renato, Oliveira, Jauvane Cavalcante de, Nedjah, Nadia |
| Publisher | Laboratório Nacional de Computação Científica, Programa de Pós-Graduação de Modelagem Computacional, LNCC, Brasil, Coordenação de Pós-Graduação e Aperfeiçoamento |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Format | application/pdf |
| Source | reponame:Biblioteca Digital de Teses e Dissertações do LNCC, instname:Laboratório Nacional de Computação Científica, instacron:LNCC |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0128 seconds