Return to search

Análise e conversão de algoritmos criptográficos para forma normal conjuntiva

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.

Identiferoai:union.ndltd.org:IBICT/oai:tede-server.lncc.br:tede/266
Date17 February 2017
CreatorsPaiva, Natasha do Nascimento
ContributorsPortugal, Renato, Lara, Pedro Carlos da Silva, Portugal, Renato, Oliveira, Jauvane Cavalcante de, Nedjah, Nadia
PublisherLaborató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 SetsIBICT Brazilian ETDs
LanguagePortuguese
Detected LanguageEnglish
Typeinfo:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis
Formatapplication/pdf
Sourcereponame:Biblioteca Digital de Teses e Dissertações do LNCC, instname:Laboratório Nacional de Computação Científica, instacron:LNCC
Rightsinfo:eu-repo/semantics/openAccess

Page generated in 0.0023 seconds