UC San Diego

Formalization and modeling are important topics in cryptography. They are crucial for precisely defining cryptographic problems and for rigorously deriving security analysis. In this dissertation, we study some computational and symbolic models in secure computation, namely:

Passive computational security model for homomorphic approximate encryptions. In this part, we study homomorphic encryption schemes, as they can be used to construct secure computation protocols. We identify the shortcomings of the classical passive security model \emph{indistinguishability under chosen plaintext attacks} when applied to approximate encryption, and we propose and study new security definitions in a model that captures the special properties of approximate encryption. As a concrete example showing the gap between these two models, we present a passive key recovery attack against the popular CKKS homomorphic approximate encryption scheme (Cheon et. al., Asiacrypt 2017) that is IND-CPA secure. We implement our attack against several open-source libraries, and we briefly discuss countermeasures to our attack.

Symbolic security model for garbled circuits. In this part, we present the first computationally sound symbolic security analysis of Yao's garbled circuits. We extend the symbolic framework of Micciancio (Eurocrypt 2010), and we prove Yao's garbled circuit scheme is (simulation-based) secure in a purely syntactic fashion, which implies concrete computational security statements by the computational soundness theorem of the symbolic model. We also implement our symbolic analysis in Haskell that can prove the security of garbling large circuits within several seconds.

Equational security model of oblivious transfer (OT) protocols. In this part, we analyze some concrete OT protocols in the equational security framework (Micciancio and Tessaro, ITCS 2013). Our analysis uncovers subtle timing issues in these protocols that are partly caused by shortcomings in the typical OT definitions. We show that the OT length extension protocol can be proved secure using a revised OT definition that adds an acknowledgment bit to the sender output. Our analysis on the ``simplest'' OT protocol of Chou and Orlandi (Latincrypt 2015) shows that this protocol cannot be proven secure in the equational framework, even using the revised OT definition.