Equational Reasoning for Verified Cryptographic Security

Other Titles
Abstract

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
Description
150 pages
Sponsorship
Date Issued
2021-12
Publisher
Keywords
Cryptography; Equational Reasoning; Formal Methods; Protocols
Location
Effective Date
Expiration Date
Sector
Employer
Union
Union Local
NAICS
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)
References
Link(s) to Reference(s)
Previously Published As
Government Document
ISBN
ISMN
ISSN
Other Identifiers
Rights
Attribution 4.0 International
Types
dissertation or thesis
Accessibility Feature
Accessibility Hazard
Accessibility Summary
Link(s) to Catalog Record