Análise e conversão de algoritmos criptográficos para forma normal conjuntiva - Paiva, Natasha do Nascimento (2017)
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.