Dissertação
Formal Verification of Password Generation Algorithms used in Password Managers EVALUATED
Gestores de Password são importantes ferramentas que nos permitem utilizar passwords fortes, libertando-nos do esforço cognitivo de as ter de memorizar. Apesar disto, ainda há muitos utilizadores que não confiam totalmente em gestores de passwords. Neste trabalho, focamo-nos numa feature que a maioria dos gestores de passwords oferece, que pode ter impacto na confiança dos mesmos, que é o processo de gerar passwords aleatórias. Pesquisamos quais os algoritmos e protocolos mais utilizados e propomos uma solução para uma implementação de referência de um algoritmo de geração de pass- words formalmente verificado. Finalmente, concretizamos a implementação de referência em Jasmin, e provamos que esta implementação preserva as propriedades verificadas. Utilizamos EasyCrypt como o ambiente de prova e Jasmin como linguagem de programação.
novembro 15, 2021, 18:0
Publicação
Obra sujeita a Direitos de Autor
Orientação
ORIENTADOR
João Fernando Peixoto Ferreira
Departamento de Engenharia Informática (DEI)
Professor Auxiliar
