Verified Password Generation from Password Composition Policies

• Tipo: Artigo em Livro de Atas de Conferência Internacional
• Data: 2022

Autores

Grilo, M (Autor) Outra; Campos, J (Autor) Outra; Ferreira, JF (Autor) Outra; Almeida, JB (Autor) Outra; Mendes, A (Autor) FEUP

Ata de Conferência Internacional

Título: INTEGRATED FORMAL METHODS, IFM 2022

Páginas: 271-288

17th International Conference on Integrated Formal Methods (IFM)

Univ Svizzera Italiana, Software Inst, Lugano, SWITZERLAND, JUN 07-10, 2022

Indexação

ISI Web of Knowledge - 0 Citações

Scopus - 1 Citação

Outras Informações

ID Authenticus: P-00W-NVT

DOI: 10.1007/978-3-031-07727-2_15

Abstract (EN): Password managers (PMs) are important tools that enable the use of stronger passwords, freeing users from the cognitive burden of remembering them. Despite this, there are still many users who do not fully trust PMs. In this paper, we focus on a feature that most PMs offer that might impact the user's trust, which is the process of generating a random password. We present three of the most commonly used algorithms and we propose a solution for a formally verified reference implementation of a password generation algorithm. We use EasyCrypt to specify and verify our reference implementation. In addition, we present a proof-of-concept prototype that extends Bitwarden to only generate compliant passwords, solving a frequent users' frustration with PMs. This demonstrates that our formally verified component can be integrated into an existing (and widely used) PM.

Idioma: Inglês

Tipo (Avaliação Docente): Científica

Nº de páginas: 18