Cryptography provides the basic tools to guarantee confidentiality and integrity of data. It hence plays a pivotal role in securing our digital infrastructure, and in enforcing the right for privacy of individuals. The development of secure cryptographic techniques is however difficult and error-prone, as unknown attack strategies need to be taken into account. To overcome this, modern cryptography advocates the paradigm of provable security, where threat models are precisely formalized using the language of mathematics, and the security of cryptosystems is proved within these models. This project aims to develop a better quantitative approach to provable security. The research of this project yields a better understanding of in-use cryptography, therefore contributing to the safer deployment of existing cryptographic solutions, as well as the support of future standardization processes. The educational component of this project includes the development of a comprehensive program to educate undergraduate students in the proper use of cryptography, and to use cryptography as a vehicle for outreach. This project develops better theory to prove rigorous lower bounds on the combination of time and memory needed by the attacker. This allows us to better compare cryptographic solutions, and to favor those which, for equal time resources, require the largest amount of memory in order to be compromised. Concretely, this project contributes along two different fronts. The first direction extends the theory of memory-hard functions, which are functions that are moderately hard to compute with respect to some combination of time and memory resources. This project introduces better hardness metrics as well as new security targets for memory-hard functions, and analyze new constructions. The second direction revisits the security of various schemes in symmetric cryptography, and provides lower bounds on the complexity of adversaries breaking them both in terms of time and memory storage, in the setting where some underlying component of scheme is modeled as ideal.