Título
[en] FORMALIZATION OF CRYPTOGRAPHY ALGORITHMS IN AN INTERACTIVE THEOREM PROVER
Título
[pt] FORMALIZAÇÃO DE ALGORITMOS DE CRIPTOGRAFIA EM UM ASSISTENTE DE PROVAS INTERATIVO
Autor
[pt] GUILHERME GOMES FELIX DA SILVA
Vocabulário
[pt] CRIPTOGRAFIA
Vocabulário
[pt] ASSISTENTE DE PROVAS
Vocabulário
[en] CRYPTOGRAPHY
Vocabulário
[en] PROOF ASSISTANT
Resumo
[pt] 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.
Resumo
[en] 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.
Orientador(es)
EDWARD HERMANN HAEUSLER
Banca
MARKUS ENDLER
Banca
CHRISTIANO DE OLIVEIRA BRAGA
Banca
EDWARD HERMANN HAEUSLER
Banca
JEFFERSON DE BARROS SANTOS
Catalogação
2018-12-13
Apresentação
2018-08-28
Tipo
[pt] TEXTO
Formato
application/pdf
Idioma(s)
PORTUGUÊS
Referência [pt]
https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=35851@1
Referência [en]
https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=35851@2
Referência DOI
https://doi.org/10.17771/PUCRio.acad.35851
Arquivos do conteúdo
NA ÍNTEGRA PDF