[en] FORMALIZATION OF CRYPTOGRAPHY ALGORITHMS IN AN INTERACTIVE THEOREM PROVER

Detalhes bibliográficos
Ano de defesa: 2018
Autor(a) principal: GUILHERME GOMES FELIX DA SILVA
Orientador(a): Não Informado pela instituição
Banca de defesa: Não Informado pela instituição
Tipo de documento: Tese
Tipo de acesso: Acesso aberto
Idioma: por
Instituição de defesa: MAXWELL
Programa de Pós-Graduação: Não Informado pela instituição
Departamento: Não Informado pela instituição
País: Não Informado pela instituição
Palavras-chave em Português:
Link de acesso: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=35851&idi=1
https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=35851&idi=2
http://doi.org/10.17771/PUCRio.acad.35851
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.