The Only Human Factor: Formal and Statistical Methods for Secure Password Composition Policy Design and Deployment

Abstract

Authentication to digital systems using passwords—secret knowledge used by
a claimant to authenticate their identity to a second party (the verifier)—remains
dominant today despite decades of research into alternative authentication factors and repeated predictions that passwords will soon die out. While they exhibit a number of very desirable security properties, human-chosen passwords
remain vulnerable to guessing attacks, and a number of measures have been
designed to motivate users to create less predictable passwords as well as make
guessing attacks more difficult to carry out for attackers. These measures, known
as password policies, restrict different aspects of password creation, usage and
management with the goal of enhancing their security. In this work, we apply
statistical techniques and formal methods to the design, development and deployment of password policies, with a particular focus on policies governing
password composition and lockout measures designed to arrest the evolution
of password guessing attacks against live systems. In doing this, we present
an end-to-end workflow beginning with sourcing and cleansing human-chosen
password data upon which to experiment, employing this data in the design of
password policies, and finally developing formally verified software capable of
enforcing these policies on real-world digital systems.

Date of Award	21 Jun 2024
Original language	English
Awarding Institution	Teesside University
Supervisor	Julien Cordry (Supervisor), João Ferreira (Supervisor), Alexandra Mendes (Supervisor) & Phillip Brooke (Supervisor)