Verified Password Generation from Password Composition Policies

• Type: Article in International Conference Proceedings Book
• Date: 2022

Authors

Grilo, M (Author) Other; Campos, J (Author) Other; Ferreira, JF (Author) Other; Almeida, JB (Author) Other; Mendes, A (Author) FEUP

Conference proceedings International

Title: INTEGRATED FORMAL METHODS, IFM 2022

Pages: 271-288

17th International Conference on Integrated Formal Methods (IFM)

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

Indexing

ISI Web of Knowledge - 0 Citations

Scopus - 1 Citation

Other information

Authenticus ID: 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.

Language: English

Type (Professor's evaluation): Scientific

No. of pages: 18