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