Bridging Theory and Practice in Password-Based Cryptography

Online authentication is most often password-based. While a full understanding of the security bounds on password-based encryption systems is a precondition for designing robust instances, there exist systems which have yet to be subjected to advanced methods of analysis. Analytical frameworks like multi-instance security [1] allow for deriving security bounds relevant to password-based encryption. This multi-instance example formalises the security from a higher abstraction - instead of focusing of the security of a single instance, the system as a whole in analysed. This broadens the approach, allowing for analysis of second lines of defence. The example application from Bellare et. al. [1] is a formal security proof for the common practice of password salting. Public salting doesn't impact the adversary's advantage for recovering a single password, but greatly effects the advantage for recovering them all. Bellare et. al. formalised a conception of indifferentiability for a multi-instance case to prove this. By building systems without the fuller understanding of security conceptions, which these frameworks allow us, we run the risk of missing simple security improvements (like salting).
A modern attack scenario could entail preprocessed dictionaries of iterated, memory-hard hashes in a multi-instance environment. Future scenarios could feasibly involve quantum based attacks, with the capability of searching n length lists in (square root) n time [2]. Future proofing password-based cryptographic systems will involve considering the union of these situations.

Aims
The aims of this project are intended to bridge the theory of provable security for the context of password based cryptography, with the instances of new password-based protocols used in the wild. This means three goals, to be approached linearly:
-Conduct research into the current landscape of password-based cryptography. Which means investigating the generation and distribution of passwords in real life, in order to produce a model based on empirical results. Assess bounds for the model with formal security analysis.
- Consider the memory-hard, preprocessed scenario - constructing a tight security bound for the multi-instance case.
-Push bounds to levels which remain comfortable in the quantum attacker case, where the parties attempting to maintain security are non-quantum.