Modern software systems today have increasingly complex security requirements – such as supporting privacy-preserving computations, or resistance against quantum attackers – that are fulfilled by advanced forms of cryptography. At the same time, these advanced forms of cryptography often have subtle security proofs that require careful auditing. To ensure security, it is thus crucial to formally verify the security of the underlying cryptography, and to do so in a manner that is approachable to cryptographers. This thesis explores the use of equational reasoning to conduct machine-checked security proofs. Equational reasoning is pervasive in cryptography, as it underlies the concepts of game-hopping hybrids and the simulation paradigm; thus, optimizing formal tools for equational reasoning delivers machine-checked proofs closer to their on-paper counterparts.We first present AutoLWE, a prover for cryptographic primitives that sup- ports reasoning about lattices. AutoLWE is built around deducibility, which (semi-) automatically applies hardness assumptions by partitioning the security game into an application of the hardness assumption with a context. Using AutoLWE, we deliver very short proofs of several representative constructions, including Public-Key Encryption, Identity-Based Encryption, and Inner Product Encryption. We then present IPDL, a simple calculus and equational logic for distributed, interactive cryptographic protocols in the computational model. The purpose of IPDL is to prove simulation results between real and idealized protocols in the style of Universal Composability (UC) [Can01]. IPDL does so by restricting its attention to straight-line protocols, a particularly simple but expressive subset of protocols. Using IPDL, we deliver short proofs of multiple case studies, including a semi-honest multiparty computation protocol over general circuits [GMW87], and an n-party coin toss protocol [Blu83].