Return to search

[en] FORMALIZATION OF CRYPTOGRAPHY ALGORITHMS IN AN INTERACTIVE THEOREM PROVER / [pt] FORMALIZAÇÃO DE ALGORITMOS DE CRIPTOGRAFIA EM UM ASSISTENTE DE PROVAS INTERATIVO

[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. / [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.

Identiferoai:union.ndltd.org:puc-rio.br/oai:MAXWELL.puc-rio.br:35851
Date13 December 2018
CreatorsGUILHERME GOMES FELIX DA SILVA
ContributorsEDWARD HERMANN HAEUSLER
PublisherMAXWELL
Source SetsPUC Rio
LanguagePortuguese
Detected LanguagePortuguese
TypeTEXTO

Page generated in 0.0025 seconds