Guilherme Gomes Felix da Silva Formalização de Algoritmos de Criptografia em um Assistente de Provas Interativo Dissertação de Mestrado Dissertação apresentada como requisito parcial para obtenção do grau de Mestre em Informática pelo Programa de Pós-Graduação da PUC-Rio. Orientador: Prof. Edward Hermann Haeusler Rio de Janeiro agosto de 2018 Guilherme Gomes Felix da Silva Formalização de Algoritmos de Criptografia em um Assistente de Provas Interativo Dissertação apresentada como requisito parcial para a obtenção do grau de Mestre pelo Programa de Pós- graduação em Informática da PUC-Rio. Aprovada pela Comissão Examinadora abaixo assinada. Edward Hermann Haeusler Orientador Departamento de Informática – PUC-Rio Markus Endler Departamento de Informática – PUC-Rio Christiano de Oliveira Braga UFF Jefferson de Barros Santos FGV Prof. Márcio da Silveira Carvalho Coordenador Setorial do Centro Técnico Científico – PUC-Rio Rio de Janeiro, 28 de agosto de 2018 Todos os direitos reservados. É proibida a reprodução total ou parcial do trabalho sem autorização da universidade, do autor e do orientador. Guilherme Gomes Felix da Silva Formou-se em Engenharia da Computação pela Pontifícia Universidade Católica do Rio de Janeiro em 2015. Ficha Catalográfica Silva, Guilherme Gomes Felix da Formalização de algoritmos de criptografia em um assistente de provas interativo / Guilherme Gomes Felix da Silva ; orientador: Edward Hermann Haeusler. – 2018. 70 f. : il. ; 30 cm Dissertação (mestrado)–Pontifícia Universidade Católica do Rio de Janeiro, Departamento de Informática, 2018. Inclui bibliografia 1. Informática – Teses. 2. Criptografia. 3. Assistente de provas. I. Haeusler, Edward Hermann. II. Pontifícia Universidade Católica do Rio de Janeiro. Departamento de Informática. III. Título. CDD: 004 Agradecimentos Ao meu orientador, Edward Hermann Haeusler, pela constante ajuda e orientação nas pesquisas feitas durante a realização deste trabalho. À CAPES e à PUC-Rio pelo auxílio financeiro sem o qual este trabalho não poderia ter sido realizado. À minha família, pelo apoio dado todos os dias. Resumo Silva, Guilherme Gomes Felix da; Haeusler, Edward Hermann. Formalização de Algoritmos de Criptografia em um Assistente de Provas Interativo. Rio de Janeiro, 2018. 70p. Dissertação de Mestrado – Departamento de Informática, Pontifícia Universidade Católica do Rio de Janeiro. Ao descrever-se a prova de um teorema, é fundamental que haja cautela para que esta não contenha erros ou inconsistências. Para provas muito longas, no entanto, a detecção de erros pode tornar-se uma tarefa humanamente inviável. Um assistente de provas é um programa cuja finalidade é realizar esta detecção de erros para um usuário de forma eficiente, bem como facilitar a construção e compreensão de provas complexas a partir de outras já existentes. O Lean Theorem Prover, desenvolvido em 2012 por Leonardo de Moura, é um assistente de provas que trabalha com descrição de provas através de uma linguagem computacional compilável. Propomos aqui uma descrição no Lean Theorem Prover das provas de funcionamento de diversos algoritmos pertinentes à área de criptografia. Palavras-chave Criptografia; assistente de provas. Abstract Silva, Guilherme Gomes Felix da; Haeusler, Edward Hermann (Advisor). Formalization of Cryptography Algorithms in an Interactive Theorem Prover. Rio de Janeiro, 2018. 70p. Dissertação de Mestrado – Departamento de Informática, Pontifícia Universidade Católica do Rio de Janeiro. When describing a proof of a theorem, one must be cautious to ensure said proof does not contain errors or inconsistencies. For very long proofs, however, error detection can become humanly infeasible. A proof assistant is a program whose purpose is to perform said error detection efficiently, as well as to assist in the creation and comprehension of complex proofs out of simpler, existing proofs. The Lean Theorem Prover, developed in 2012 by Leonardo de Moura, is a proof assistant which functions via description of proofs in a compilable computer language. We present a description of proofs of correctness of various algorithms pertaining to cryptography in the Lean Theorem Prover. Keywords Cryptography; proof assistant. Sumário 1 Introdução..........................................................................................10 1.1 Contribuições.....................................................................................................10 2 Conceitos Fundamentais de Criptografia.......................................11 2.1 Criptografia com Chave Simétrica.....................................................................12 2.2 Criptografia com Chave Pública (ou Chave Assimétrica).................................14 3 Algoritmos de Criptografia...............................................................16 3.1 O Data Encryption Standard (DES)..................................................................16 3.1.1 Estrutura do Algoritmo......................................................................16 3.1.1.1 Etapas de Codificação........................................................17 3.1.1.2 Permutação Inicial e Final...................................................17 3.1.2 Função f...........................................................................................19 3.1.3 Key Schedule...................................................................................20 3.2 O Algoritmo RSA (Rivest, Shamir & Adleman).................................................21 3.2.1 Conceitos de Aritmética Modular.....................................................22 3.2.2 Utilização de Aritmética Modular pelo RSA......................................23 3.2.3 A Função Totiente de Euler..............................................................23 3.2.4 Geração de Parâmetros e Codificação de Mensagens....................24 3.3 Blowfish.............................................................................................................25 4 Prova Interativa de Teoremas...........................................................27 4.1 O Lean Theorem Prover....................................................................................27 5 Provas de Corretude e Consistência de Algoritmos de Criptografia no Lean Theorem Prover.............................................30 5.1 Provas de Corretude do Data Encryption Standard..........................................30 5.1.1 Permutações Inicial e Final...............................................................33 5.1.2 Passo de Codificação.......................................................................34 5.1.3 Sequência de Codificação................................................................40 5.2 Provas de Corretude do RSA............................................................................42 5.2.1 Prova.................................................................................................42 5.2.2 Prova no Lean Theorem Prover.......................................................44 5.3 Provas de Corretude do Blowfish......................................................................55 5.3.1 Prova.................................................................................................55 5.3.2 Prova no Lean Theorem Prover.......................................................56 6 Conclusão..........................................................................................69 7 Referências bibliográficas................................................................70 Lista de figuras 2.1: Representação genérica do funcionamento de um algoritmo de criptografia com chave simétrica..................................................................................12 2.2: Representação genérica do funcionamento de um algoritmo de criptografia com chave pública....................................................................................14 3.1: Estrutura do Data Encryption Standard................................................................17 3.2: Estrutura de uma etapa de codificação do Data Encryption Standard...................17 3.3: Estrutura da função f do Data Encryption Standard..............................................20 3.4: Estrutura da função Key Schedule do Data Encryption Standard........................21 3.5: Estrutura do algoritmo Blowfish...........................................................................26 5.1: Último passo de uma sequência de codificação do DES, seguido do primeiro passo da sequência de decodificação......................................................35 Lista de tabelas 3.1: Permutação inicial do Data Encryption Standard................................................18 3.2: Permutação final do Data Encryption Standard...................................................18 3.3: Exemplo de funcionamento da operação de permutação inicial do Data Encryption Standard.....................................................................................18 5.1: Prova de corretude da metade esquerda de um passo de codificação do DES, ou 𝐿𝑑 = 𝑅 ..................................................................................................38 1 15 5.2: Prova de corretude da metade direita de um passo de codificação do DES, ou 𝐿 = 𝑅𝑑.................................................................................................39 15 1 5.3: Prova de 𝐿𝑑 = 𝑅 para o algoritmo DES............................................................41 16 0 5.4: Definição no Lean de premissas sobre as variáveis one, x, n, p, q, d, e e para a prova de corretude do algoritmo RSA........................45 5.5: Definição no Lean de propriedades do número 1 para a prova de corretude do algoritmo RSA........................................................................................45 5.6: Definição no Lean de propriedades da exponenciação para a prova de corretude do algoritmo RSA..................................................................................46 5.7: Definição no Lean do operador de módulo e suas propriedades para a prova de corretude do algoritmo RSA.............................................................46 5.8: Definição no Lean das propriedades de escalabilidade e distributividade da multiplicação para a prova de corretude do algoritmo RSA..................................47 5.9: Definição no Lean do teorema de Euler e de uma propriedade do máximo divisor comum necessária para a prova de corretude do algoritmo RSA...................47 5.10: Prova de corretude do funcionamento do algoritmo RSA no Lean Theorem Prover, para o caso em que 𝑚𝑑𝑐(𝑥,𝑛) = 1...................................48-49 5.11: Primeira parte da prova de corretude do funcionamento do algoritmo RSA no Lean Theorem Prover, para o caso em que 𝑚𝑑𝑐(𝑥,𝑛) ≠ 1.............................................................................................................50 5.12: Segunda parte da prova de corretude do funcionamento do algoritmo RSA no Lean Theorem Prover, para o caso em que 𝑚𝑑𝑐(𝑥,𝑛) ≠ 1........................................................................................................51-54 5.13: Parte final da prova de corretude do funcionamento do algoritmo RSA no Lean Theorem Prover....................................................................55 5.14: Definição no Lean das propriedades da operação de ou-exclusivo para a prova de corretude do algoritmo Blowfish......................................................57 5.15: Prova de corretude do funcionamento do algoritmo Blowfish.....................59-65 5.16: Prova de corretude do funcionamento do algoritmo Blowfish.....................65-68 5.17: Listas de equações definidas nos comentários da prova de corretude do algoritmo Blowfish.................................................................................68 1 Introdução Ao descrever-se uma prova de um teorema, em particular provas de tamanho extenso, a detecção de erros torna-se uma questão crucial, pois um único erro pode implicar em uma conclusão errônea sobre a veracidade ou falsidade de um teorema. De modo a compensar a imperfeição humana no que se diz respeito à detecção de erros em provas de teoremas, foram desenvolvidos programas que visam auxiliar nesta prática, denominados assistentes de provas. O trabalho aqui apresentado tem a intenção de explorar o uso de assistentes de provas interativos, utilizando um destes programas para demonstrar a corretude de provas relacionadas a algoritmos da área de criptografia. Este trabalho encontra-se dividido em diversas partes. A seção 2 deste documento tem a finalidade de apresentar os conceitos básicos de criptografia que são necessários para a compreensão do trabalho desenvolvido, como a diferença entre criptografia com chave simétrica e assimétrica e o conceito de chaves públicas e privadas. Na seção 3, são apresentados em maior detalhe os algoritmos de criptografia explorados neste trabalho (Data Encryption Standard, RSA e Blowfish). Aqui também são descritos em maior detalhe alguns dos conceitos apresentados na seção 2, conforme estes tornam-se relevantes para a compreensão dos algoritmos. Como o algoritmo RSA utiliza aritmética modular amplamente, está incluída uma seção que visa apresentar o leitor que não possua familiaridade a esta área da matemática. A seção 4 visa descrever o Lean Theorem Prover, que é o assistente de provas interativo utilizado para o desenvolvimento das provas formais aqui apresentadas. Por fim, a seção 5 descreve o trabalho desenvolvido propriamente dito – isto é, como as provas de corretude dos algoritmos previamente descritos foram traduzidas para a linguagem do Lean Theorem Prover. 1.1 Contribuições Como contribuição para a comunidade científica, visa-se explorar aqui o conceito de prova interativa de teoremas e aplicar estas provas à área de criptografia, por tratar-se de uma área na qual foram realizados relativamente poucos trabalhos envolvendo provas formais e interativas, e por não ser conhecido, até o fechamento deste trabalho, nenhum que houvesse utilizado o Lean Theorem Prover para tal fim.