Paper 2013/296
Universally Composable Symbolic Analysis for Two-Party Protocols based on Homomorphic Encryption
Morten Dahl and Ivan Damgård
Abstract
We consider a class of two-party function evaluation protocols in which the parties are allowed to use ideal functionalities as well as a set of powerful primitives, namely commitments, homomorphic encryption, and certain zero-knowledge proofs. We illustrate that with these it is possible to capture protocols for oblivious transfer, coin-flipping, and generation of multiplication-triple. We show how any protocol in our class can be compiled to a symbolic representation expressed as a process in an abstract process calculus, and prove a general computational soundness theorem implying that if the protocol realises a given ideal functionality in the symbolic setting, then the original version also realises the ideal functionality in the standard computational UC setting. In other words, the theorem allows us to transfer a proof in the abstract symbolic setting to a proof in the standard UC model. Finally, we show that the symbolic interpretation is simple enough in a number of cases for the symbolic proof to be partly automated using the ProVerif tool.
Metadata
- Available format(s)
-
PDF
- Category
- Foundations
- Publication info
- Published elsewhere. Unknown where it was published
- Keywords
- Cryptographic protocolsSecurity analysisSymbolic analysisAutomated analysisComputational soundnessUniversal compositionHomomorphic encryption
- Contact author(s)
- mdahl @ cs au dk
- History
- 2013-05-25: received
- Short URL
- https://ia.cr/2013/296
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2013/296,
author = {Morten Dahl and Ivan Damgård},
title = {Universally Composable Symbolic Analysis for Two-Party Protocols based on Homomorphic Encryption},
howpublished = {Cryptology {ePrint} Archive, Paper 2013/296},
year = {2013},
url = {https://eprint.iacr.org/2013/296}
}
