Equational Reasoning for Verified Cryptographic Security

Other Titles


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].

Journal / Series

Volume & Issue


150 pages


Date Issued




Cryptography; Equational Reasoning; Formal Methods; Protocols


Effective Date

Expiration Date




Union Local


Number of Workers

Committee Chair

Shi, Runting

Committee Co-Chair

Committee Member

Rooth, Mats
Morrisett, Greg

Degree Discipline

Computer Science

Degree Name

Ph. D., Computer Science

Degree Level

Doctor of Philosophy

Related Version

Related DOI

Related To

Related Part

Based on Related Item

Has Other Format(s)

Part of Related Item

Related To

Related Publication(s)

Link(s) to Related Publication(s)


Link(s) to Reference(s)

Previously Published As

Government Document




Other Identifiers


Attribution 4.0 International


dissertation or thesis

Accessibility Feature

Accessibility Hazard

Accessibility Summary

Link(s) to Catalog Record