Cryptographic standards published by organizations like NIST, ISO, and the IETF provide guidance for developers choosing and implementing cryptographic algorithms for their applications. In recent years, formal proofs of security have become an important part of validation for standardized algorithms; however, these proofs rely on abstractions which sometimes differ significantly from the schemes and protocols used in practice.

In this work, I will begin with a study of the ongoing NIST standardization process of post-quantum key-encapsulation mechanisms and highlight vulnerabilities in several (former) candidate algorithms which arise from a systematic mismatch between abstract primitives used in cryptographic models and their actual instantiation in implementations. I will then present a library of secure instantiation techniques and a way to extend schemes' existing proofs to their instantiations. Next, I will address the Transport Layer Security (TLS 1.3) Handshake Protocol and demonstrate by a concrete evaluation that prior work fails to prove practical security levels for many of the standardized parameter sets. I will then show tighter proofs that do justify these parameter sets and which additionally give the first fully justified abstraction of the TLS 1.3 key schedule in the random oracle model, and I will explain how certain parts of the TLS 1.3 design hinder the application of useful abstractions. I will also explain how inaccurate portrayals of hash functions in the random oracle model impact the security analysis of the standardized EdDSA signature scheme and present an improved proof of security with better tightness and modularity. I conclude by introducing my work on the proposed standard for privacy-preserving measurement, including a new security model for Verifiable Distributed Aggregation Functions. Within this model, I discuss results for Prio3, an optimized version of the massively scalable, widely used Prio construction for private data collection, and Doplar, a new construction for private histogram generation.