Universally Composable Symbolic Analysis for Two-Party Protocols Based on Homomorphic Encryption

Abstract

We consider a class of two-party function evaluation protocols in which the parties are allowed to<br/>use ideal functionalities as well as a set of powerful primitives, namely commitments, homomorphic<br/>encryption, and certain zero-knowledge proofs. We illustrate that with these it is possible to capture<br/>protocols for oblivious transfer, coin- ipping, and generation of multiplication-triple.<br/>We show how any protocol in our class can be compiled to a symbolic representation expressed<br/>as a process in an abstract process calculus, and prove a general computational soundness theorem<br/>implying that if the protocol realises a given ideal functionality in the symbolic setting, then the<br/>original version also realises the ideal functionality in the standard computational UC setting. In<br/>other words, the theorem allows us to transfer a proof in the abstract symbolic setting to a proof in<br/>the standard UC model.<br/>Finally, we show that the symbolic interpretation is simple enough in a number of cases for the<br/>symbolic proof to be partly automated using ProVerif